使用GADT进行类型推断 - a0不可触摸 [英] Type inference with GADTs - a0 is untouchable
问题描述
可以说我有这个程序
{ - ＃LANGUAGE GADTs＃ - }
data My a where
A :: Int - >我的Int
B :: Char - > My Char
main :: IO（）
main = do
let x = undefined :: My a
case x of
A v - >打印v
- 打印x
编译正常。
但是，当我在 print x 中发表评论时，我得到：
gadt.hs：第13行，第12列：
无法将类型'a0'与'（）'相匹配
'a0'不可触及
约束内（a1〜GHC.Types.Int）
由具有构造函数的模式绑定
Main.A :: GHC.Types.Int - > Main.My GHC.Types.Int，
（可选）
at /home/niklas/src/hs/gadt-binary.hs:13:5-7
预期类型：GHC .Types.IO a0
实际类型：GHC.Types.IO（）
在表达式中：System.IO.print v
在另一种情况下：Main.A v - > System.IO.print v
为什么我在第13行（ A v - >打印v ），而不是仅在打印x 行中？
我认为第一次出现应该确定这种类型。
请赐教：）
好吧，首先请注意，这与特定的 print x 没有任何关系：在结束时出现同样的错误。主要与例如 putStrLndone。
所以在这种情况下，问题确实存在 do 的最后一条语句需要 c> 块的签名的类型。其他语句只需要在相同的monad中，即 IO a0 而不是 IO（）。
现在，通常这个 a0 是从语句本身推断出来的，例如，您可以写入
do getLine
putStrLn丢弃的输入
尽管 getLine :: IO String 而不是 IO（）。但是，在您的示例中，信息 print :: ... - > IO（）来自 case 块，来自GADT匹配。而且这样的GADT匹配与其他Haskell语句的行为不同：基本上，它们不会让任何类型信息溢出其范围，因为如果信息来自GADT构造函数，那么在 case 。
在这个特定的例子中，似乎很明显， a0〜（）完全与GADT匹配中的 a1〜Int 有关，但通常情况下，只有GHC追踪所有类型信息的 他们来自哪里。我不知道这是否有可能，它肯定比Haskell的Hindley-Milner系统更复杂，它很大程度上依赖于统一类型信息，它基本上假定信息的位置并不重要
因此，GADT匹配只是作为一个刚性的类型信息二极管：内部的东西永远不能用于确定外部类型，就像
case 块作为一个整体应该是 IO（）。 然而，你可以手动断言，用相当丑陋的
（case x of
A v - > print v
）:: IO（）
或书写
（）< - case x of
A v - >打印v
Lets say I have this program
{-# 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
compiles fine.
But when I comment in the print x, I get:
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
Why do I get this error in line 13 (A v -> print v) instead of only in the print x line?
I thought the first occurrence should determine the type.
Please enlighten me :)
Well, first note that this has nothing to do with the particular print x: you get the same error when ending main with e.g. putStrLn "done".
So the problem is indeed in the case block, namely in that only the last statement of a do is required to have the type of the do block's signature. The other statements merely have to be in the same monad, i.e. IO a0 rather than IO ().
Now, usually this a0 is inferred from the statement itself, so for instance you can write
do getLine
putStrLn "discarded input"
though getLine :: IO String rather than IO (). However, in your example the information print :: ... -> IO () comes from inside the case block, from a GADT match. And such GADT matches behave differently from other Haskell statements: basically, they don't let any type information escape its scope, because if the information came from the GADT constructor then it's not correct outside of the case.
In that particular example, it seems obvious enough that a0 ~ () has nothing at all to do with the a1 ~ Int from the GADT match, but in general, such a fact could only be proven if GHC traced for all type information where it came from. I don't know if that's even possible, it would certainly be more complicated than Haskell's Hindley-Milner system, which heavily relies on unifying type information, which essentially assumes that it doesn't matter where the information came from.
Therefore, GADT matches simply act as a rigid “type information diode”: the stuff inside can never be used to determine types on the outside, like that the case block as a whole should be IO ().
However, you can manually assert that, with the rather ugly
(case x of
A v -> print v
) :: IO ()
or by writing
() <- case x of
A v -> print v
这篇关于使用GADT进行类型推断 - a0不可触摸的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
