Нечетное сообщение об ошибке ghc: "Мой мозг просто взорвался"?

Когда я пытаюсь сопоставить образ GADT в синтаксисе proc (с Netwire и Vinyl):

sceneRoot = proc inputs -> do
            let (Identity camera :& Identity children) = inputs 
            returnA -< (<*>) (map (rGet draw) children) . pure

Я получаю (скорее нечетную) ошибку компилятора, из ghc-7.6.3

  My brain just exploded
    I can't handle pattern bindings for existential or GADT data constructors.
    Instead, use a case-expression, or do-notation, to unpack the constructor.
    In the pattern: Identity cam :& Identity childs

Я получаю аналогичную ошибку, когда я помещаю шаблон в шаблон proc (...). Почему это? Это необоснованно или просто не реализовано?

Ответы

Ответ 1

Рассмотрим GADT

data S a where
  S :: Show a => S a

и выполнение кода

foo :: S a -> a -> String
foo s x = case s of
            S -> show x

В реализации Haskell на основе словаря можно ожидать, что значение s будет содержать словарь классов и что case извлекает функцию show из указанного словаря, чтобы выполнить show x.

Если мы выполним

foo undefined (\x::Int -> 4::Int)

получаем исключение. Оперативно это ожидается, потому что мы не можем получить доступ к словарю. Более того, case (undefined :: T) of K -> ... будет вызывать ошибку, потому что он заставляет оценивать undefined (при условии, что T не является newtype).

Рассмотрим теперь код (допустим, что это компилируется)

bar :: S a -> a -> String
bar s x = let S = s in show x

и выполнение

bar undefined (\x::Int -> 4::Int)

Что это должно делать? Можно утверждать, что он должен генерировать то же исключение, что и с foo. Если бы это было так, ссылочная прозрачность означала бы, что

let S = undefined :: S (Int->Int) in show (\x::Int -> 4::Int)

также не работает с тем же исключением. Это означало бы, что let оценивает выражение undefined, в отличие от, например,

let [] = undefined :: [Int] in 5

который оценивается как 5.

Действительно, шаблоны в let ленивы: они не заставляют оценивать выражение, в отличие от case. Вот почему, например,

let (x,y) = undefined :: (Int,Char) in 5

успешно оценивает значение 5.

Можно было бы сделать let S = e in e' оценку e, если в e' требуется <<24 > , но это выглядит довольно странно. Кроме того, при оценке let S = e1 ; S = e2 in show ... было бы непонятно, следует ли оценивать e1, e2 или и то, и другое.

GHC на данный момент решает запретить все эти случаи с помощью простого правила: никаких ленивых шаблонов при устранении GADT.