Haskell GADT和衍生节目

Question

如何使show用于Bind数据构造函数？前两个（Return和Put）似乎工作正常。由于Bind接受了一个函数作为参数，所以我认为它需要一些特殊的“处理”吗？

data Program a where
  Put    :: Char -> Program ()
  Get    :: Program (Maybe Char)
  Return :: a -> Program a
  Bind   :: Program a -> (a -> Program b) -> Program b

instance Show a => Show (Program a) where
    show (Return a) = show a
    show (Put a) = show a
    show (Bind pr f) = show pr   -- incorrect


• Could not deduce (Show a1) arising from a use of ‘show’
  from the context: Show a
    bound by the instance declaration at EDSL_Deep1.hs:18:10-35
  Possible fix:
    add (Show a1) to the context of the data constructor ‘Bind’
• In the expression: show pr
  In an equation for ‘show’: show (Bind pr f) = show pr
  In the instance declaration for ‘Show (Program a)’

Answer 1

我认为您可能正在混淆类型变量。 a中的Program a与构造函数类型中的a没有关系。仅在此处指定程序的类型。实际上，使用KindSignatures也可以说data Program :: Type -> Type。在此过程中，还可以在Bind中重命名vars，因为我们可以：

data Program :: Type -> Type where
  Put    :: Char -> Program ()
  Get    :: Program (Maybe Char)
  Return :: a -> Program a
  Bind   :: Program x -> (x -> Program y) -> Program y

这仍然是相同的定义。希望这可以清楚地表明您试图显示仅具有Program x的Show y，这就是为什么会出现错误的原因。正如评论中所说，我认为这里没有希望。