Вывод типа с помощью GADT — a0 неприкосновенен

Допустим, у меня есть эта программа

{-# LANGUAGE GADTs #-}

data My a where
  A :: Int  -> My Int
  B :: Char -> My Char


main :: IO ()
main = do
  let x = undefined :: My a

  case x of
    A v -> print v

  -- print x

компилируется нормально.

Но когда я комментирую в print x, я получаю:

gadt.hs: line 13, column 12:
  Couldn't match type ‘a0’ with ‘()’
    ‘a0’ is untouchable
      inside the constraints (a1 ~ GHC.Types.Int)
      bound by a pattern with constructor
                 Main.A :: GHC.Types.Int -> Main.My GHC.Types.Int,
               in a case alternative
      at /home/niklas/src/hs/gadt-binary.hs:13:5-7
  Expected type: GHC.Types.IO a0
    Actual type: GHC.Types.IO ()
  In the expression: System.IO.print v
  In a case alternative: Main.A v -> System.IO.print v

Почему я получаю эту ошибку в строке 13 (A v -> print v), а не только в строке print x?

Я думал, что первое вхождение должно определять тип.

Пожалуйста, просветите меня :)


haskell gadt
person nh2    schedule 18.02.2015    source источник

Ответы (1)


arrow_upward
26
arrow_downward

Ну, во-первых, обратите внимание, что это не имеет ничего общего с конкретным print x: вы получаете ту же ошибку, когда заканчиваете main, например. putStrLn "done".

Таким образом, проблема действительно заключается в блоке case, а именно в том, что только последний оператор do должен иметь тип сигнатуры блока do. Остальные операторы просто должны быть в той же монаде, то есть IO a0, а не IO ().

Теперь обычно это a0 выводится из самого утверждения, поэтому, например, вы можете написать

do getLine
   putStrLn "discarded input"

хотя getLine :: IO String, а не IO (). Однако в вашем примере информация print :: ... -> IO () поступает из блока case из совпадения GADT. И такие совпадения GADT ведут себя иначе, чем другие операторы Haskell: в основном, они не позволяют какой-либо информации о типе выйти за пределы своей области действия, потому что, если информация получена из конструктора GADT, то она неверна за пределами case.

В этом конкретном примере кажется достаточно очевидным, что a0 ~ () не имеет никакого отношения к a1 ~ Int из совпадения GADT, но в целом такой факт может быть доказан только в том случае, если GHC проследит все сведения о типах. откуда оно взялось. Я не знаю, возможно ли это вообще, это определенно было бы сложнее, чем система Хиндли-Милнера в Haskell, которая сильно зависит от объединения информации о типах, которая, по сути, предполагает, что не имеет значения, где находится информация. пришли из.

Таким образом, совпадения GADT просто действуют как жесткий диод информации о типах: содержимое внутри никогда не может быть использовано для определения типов снаружи, например, блок case в целом должен быть IO ().

Однако вы можете вручную утверждать, что с довольно уродливым

  (case x of
     A v -> print v
    ) :: IO ()

или написав

  () <- case x of
          A v -> print v
person leftaroundabout    schedule 18.02.2015
comment
Отличный ответ! Техническая придирка: в то время как основной язык Haskell98 использует систему типов Hindley-Milner, GHC использует более мощную System F. - person Ari Fordsham; 16.03.2021