我为表达式创建了一个 GADT。当我对具有约束的构造函数进行模式匹配时,类型检查器无法推断构造函数约束中使用的类型变量的约束。我认为代码和错误消息更清楚。
{-# LANGUAGE GADTs, MultiParamTypeClasses #-}
import Data.Word
data Expr a where
Value :: a -> Expr a
Cast :: (Castable a b) => Expr a -> Expr b
class Castable a b where
cast :: a -> b
instance Castable Word64 Word32 where
cast = fromIntegral
instance (Show a) => Show (Expr a) where
show (Cast e) = "Cast " ++ show e -- ERROR
我得到的错误:
gadt.hs:16:30:
Could not deduce (Show a1) arising from a use of `show'
from the context (Show a)
bound by the instance declaration at gadt.hs:15:10-34
or from (Castable a1 a)
bound by a pattern with constructor
Cast :: forall b a. Castable a b => Expr a -> Expr b,
in an equation for `show'
at gadt.hs:16:9-14
Possible fix:
add (Show a1) to the context of
the data constructor `Cast'
or the instance declaration
In the second argument of `(++)', namely `show e'
In the expression: "Cast " ++ show e
In an equation for `show': show (Cast e) = "Cast " ++ show e
编辑:如果我注释掉
Show (Expr a)
实例并添加以下代码,它工作正常:eval :: Expr a -> a
eval (Value a) = a
eval (Cast e) = cast $ eval e
main = do
let bigvalue = maxBound `div` 2 + 5 :: Word64
e = Cast (Value bigvalue) :: Expr Word32
v = eval e
putStrLn "typechecks."
print (bigvalue, v)
我希望显示实例基本上打印
Cast (Value bigvalue)
之类的内容.
最佳答案
Cast :: (Castable a b) => Expr a -> Expr b
所以在这里:
instance (Show a) => Show (Expr a) where
show (Cast e) = "Cast " ++ show e -- ERROR
Cast e
是 Expr a
类型.我们有一个 Show a
约束,在这个例子中,这意味着 Show (Expr a)
,所以我们可以调用show
关于 Expr a
类型的东西.但是
e
是 不是 类型 Expr a
. Cast
接受任何类型的参数 Expr a1
并给你一个Expr a
(重命名类型变量以与我们在实例中讨论的内容保持一致),所以 e
是 Expr a1
类型.我们没有 Show
a1
类型的约束, 我们需要 Show a1
暗示Show (Expr a1)
, 所以没有办法 show e
.并且没有办法在
Show
中添加这样的约束。例如,因为类型 a1
没有出现在 Cast e
的类型中.这似乎是在这里使用 GADT 的重点;你故意丢弃了所有关于 Cast
的事物类型的信息。被应用于(除了 Castable a1 a
成立的事实),并声明结果只是 Expr a
.
关于haskell - GADT 上的模式匹配,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/17982477/