haskell - GADT 上的模式匹配

Question

我为表达式创建了一个 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) 之类的内容.

Answer 1

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 .