4

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

4

1 回答 1

8 
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不是类型。_ 接受任何类型的参数并为您提供一个（重命名类型变量以与我们在实例中讨论的内容保持一致），type 也是如此。我们对类型没有约束，我们需要暗示，所以没有办法。Expr aCastExpr a1Expr aeExpr a1Showa1Show a1Show (Expr a1)show e

并且没有办法在Show实例中添加这样的约束，因为类型a1没有出现在Cast e. 这似乎是在这里使用 GADT 的重点；您故意丢弃了有关Cast所应用事物类型的所有信息（除了Castable a1 a成立的事实），并将结果简单地声明为Expr a.

于 2013-07-31T23:53:28.800 回答