Почему GHC считает, что эта переменная типа не является инъективной? - PullRequest
Новая
       7

Почему GHC считает, что эта переменная типа не является инъективной?

25 голосов
/ 23 октября 2011

У меня есть этот кусок кода: 

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, KindSignatures, GADTs, FlexibleInstances, FlexibleContexts #-}

class Monad m => Effect p e r m | p e m -> r where
  fin :: p e m -> e -> m r

data ErrorEff :: * -> (* -> *) -> * where 
  CatchError :: (e -> m a) -> ErrorEff ((e -> m a) -> m a) m

instance Monad m => Effect ErrorEff ((e -> m a) -> m a) a m where
  fin (CatchError h) = \f -> f h

Это не компилируется, с этой ошибкой типа в последней строке: 

Could not deduce (a1 ~ a)
from the context (Monad m)
[...]
or from (((e -> m a) -> m a) ~ ((e1 -> m a1) -> m a1))
[...]

Если я изменю m на[] он компилируется нормально, поэтому, очевидно, GHC считает, что m не является инъективным.(Хотя он не предупреждает об инъективности, как это происходит с семействами типов.)

Моя версия GHC - 7.2.1.

Редактировать: Если я изменю (e -> m a) на eэто работает, если я изменяю это на m a, это не делает, и ни для (m a -> e).

Ответы [ 2 ]

31 голосов
/ 31 октября 2011

Это не совсем ошибка, но это длинная история ...

История

В 7.0 раньше был конструктор приведения right, который работал так:

g : f a ~ f b
---------------
right g : a ~ b

То есть, если g является принуждением между f a и f b, то right g является принуждением между a и b.Это только звук, если f гарантированно будет инъективным: в противном случае мы могли бы на законных основаниях, скажем, f Int ~ f Char, и тогда мы могли бы заключить Int ~ Char, что было бы Плохо.Конечно, синонимы типов и семейства типов не обязательно являются инъективными;например: 

type T a = Int

type family F a :: *
type instance F Int  = Bool
type instance F Char = Bool

Так как же эта гарантия возможна?Что ж, это как раз та причина, по которой частичное применение синонимов и семейств типов не допускается.Частичные применения синонимов типов и семейств типов могут не быть инъективными, но насыщенные приложения (даже те, которые приводят к более высокому виду) всегда.

Конечно, ограничение на частичные применения раздражает.Таким образом, в 7.2, пытаясь двигаться в направлении разрешения частичного применения (и поскольку это упрощает теорию и реализацию языка принуждения), конструктор right был заменен конструктором nth с сопровождающим правилом 

g : T a1 .. an ~ T b1 .. bn
---------------------------
nth i g : ai ~ bi

То есть nth применяется только к принуждению g, которое относится к двум типам, которые известны как насыщенные приложения конструктора типа T.Теоретически, это допускает частичное применение синонимов и семейств типов, потому что мы не можем разложить равенства, пока не узнаем, что они находятся между приложениями (обязательно инъективного) конструктора типа.В частности, nth не применяется к принуждению f a ~ f b, потому что f является переменной типа, а не конструктором типа.

Во время изменения считалось, что никто на самом деле не заметит, но, очевидно, это было неправильно!

Интересно, что трюк Олега, изложенный в сообщении haskell-cafe от Daniel Schüssler , показывает, что реализация семейств типов не изменилась соответствующим образом!Проблема в том, что определение типа 

type family Arg fa
type instance Arg (f a) = a

не должно быть разрешено, если f может быть неинъективным;в этом случае определение даже не имеет смысла.

Следующие шаги

Я думаю, что правильное решение - восстановить right (или что-то эквивалентное), поскольку люди явно этого хотят!Надеемся, что это будет сделано в ближайшее время.

Тем временем было бы очень здорово разрешить частично примененные синонимы и семейства типов.Кажется, правильный путь (tm) сделать это - отслеживать инъективность в системе вида: то есть каждый вид стрелки будет аннотирован своей инъекцией.Таким образом, встречая равенство f a ~ f b, мы можем посмотреть на вид f, чтобы определить, безопасно ли его разложить на равенство a ~ b.Не случайно я сейчас пытаюсь разработать дизайн такой системы.=) * +1058 *

2 голосов
/ 31 октября 2011

Я не уверен в причине, но я уменьшил ваш тестовый пример до: 

{-# LANGUAGE GADTs #-}

data ErrorEff x where
  CatchError :: m a -> ErrorEff (m a)

fin :: ErrorEff (m a) -> m a
fin (CatchError h) = h

, который компилируется в GHC 7.0.3, но не 7.3.20111021.

Это определенноошибка компилятора.

Компилируется после изменения: 

data ErrorEff x where
  CatchError :: x -> ErrorEff x

И функцию "fin" можно восстановить с помощью синтаксиса записи: 

data ErrorEff x where
  CatchError :: { fin :: m a } -> ErrorEff (m a)
...