GADTs上的模式匹配

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)

我希望show实例基本上打印出像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.