将 GADT 与 DataKinds 结合使用以实现函数中的类型级数据构造函数约束

Question

我正在尝试将 GADT 与 DataKinds 结合使用，如下所示

\n

{-# LANGUAGE KindSignatures, DataKinds, GADTs #-}\nmodule NewGadt where\n\ndata ExprType = Var | Nest\n\ndata Expr (a :: ExprType) where\n  ExprVar :: String -> Expr Var\n  ExprNest :: Expr a -> Expr Nest\n\ndata BaseExpr\n  = BaseExprVar String\n  | BaseExprNest BaseExpr\n\ntranslate :: BaseExpr -> Expr a\ntranslate (BaseExprVar id) = ExprVar id\ntranslate (BaseExprNest expr) = ExprNest $ translate expr\n

\n

编译错误：

\n

/home/elijah/code/monty/src/NewGadt.hs:15:32: error:\n    \xe2\x80\xa2 Couldn\'t match type \xe2\x80\x98a\xe2\x80\x99 with \xe2\x80\x98\'Var\xe2\x80\x99\n      \xe2\x80\x98a\xe2\x80\x99 is a rigid type variable bound by\n        the type signature for:\n          bexprToExpr :: forall (a :: ExprType). BaseExpr -> Expr a\n        at src/NewGadt.hs:14:1-33\n      Expected type: Expr a\n        Actual type: Expr \'Var\n    \xe2\x80\xa2 In the expression: ExprVar id\n      In an equation for \xe2\x80\x98bexprToExpr\xe2\x80\x99:\n          bexprToExpr (BaseExprVar id) = ExprVar id\n    \xe2\x80\xa2 Relevant bindings include\n        bexprToExpr :: BaseExpr -> Expr a (bound at src/NewGadt.hs:15:1)\n   |\n15 | bexprToExpr (BaseExprVar id) = ExprVar id\n   |                                ^^^^^^^^^^\n

\n

我想这样做，以便某些函数只能对特定类型的 expr 起作用，例如：

\n

/home/elijah/code/monty/src/NewGadt.hs:15:32: error:\n    \xe2\x80\xa2 Couldn\'t match type \xe2\x80\x98a\xe2\x80\x99 with \xe2\x80\x98\'Var\xe2\x80\x99\n      \xe2\x80\x98a\xe2\x80\x99 is a rigid type variable bound by\n        the type signature for:\n          bexprToExpr :: forall (a :: ExprType). BaseExpr -> Expr a\n        at src/NewGadt.hs:14:1-33\n      Expected type: Expr a\n        Actual type: Expr \'Var\n    \xe2\x80\xa2 In the expression: ExprVar id\n      In an equation for \xe2\x80\x98bexprToExpr\xe2\x80\x99:\n          bexprToExpr (BaseExprVar id) = ExprVar id\n    \xe2\x80\xa2 Relevant bindings include\n        bexprToExpr :: BaseExpr -> Expr a (bound at src/NewGadt.hs:15:1)\n   |\n15 | bexprToExpr (BaseExprVar id) = ExprVar id\n   |                                ^^^^^^^^^^\n

\n

当然，printVariable用Expr Nest进行调用应该会导致编译失败。

\n

有没有办法让翻译函数返回Expr a像这样返回？或者这是 DataKinds 和 GADT 的不当使用？

\n

编辑：

\n

解决方案有效！但是，我必须升级到 ghc >=8.10 并启用StandaloneKindSignatures, PolyKinds

\n

Answer 1

您可以定义一个存在的包装器

{-# Language PolyKinds                #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications         #-}

import Data.Kind (Type)

--
--   Exists @ExprType :: (ExprType -> Type) -> Type
--
type Exists :: forall k. (k -> Type) -> Type
data Exists f where
  Exists :: f x -> Exists f

并返回Exists Expr

translate :: BaseExpr -> Exists @ExprType Expr
translate (BaseExprVar id)
  = Exists (ExprVar id)
translate (BaseExprNest expr)
  | Exists a <- translate expr
  = Exists (ExprNest a)

这使用模式保护来解压存在类型

模式保护的形式为p <- e，其中p是类型的模式（参见第 3.17 节）t，并且e是表达式类型t1。如果表达式e与模式匹配p，它们就会成功，并将模式的绑定引入到环境中。

哈斯克尔报告

并且相当于这些

translate (BaseExprNest expr) = case translate expr of
  Exists a -> Exists (ExprNest a)

{-# Language ViewPatterns #-}

translate (BaseExprNest (translate -> Expr a)) = Exists (ExprNest a)

let但用or尝试一下where，却行不通。

参考

• Stitch：声音类型索引类型检查器
• 生存危机已解决

Answer 2

之所以失败，是因为你做出了无法兑现的承诺。翻译的类型是BaseExpr -> Expr a，所以你实际上是在说“如果你给我一个BaseExpr，我会给你一个你想要的Expr a任何类型a”。GHC 抱怨，因为你实际上并没有这样做。如果你translate用 a调用BaseExprVar，你实际上不会得到Expr a任何类型 a 的 an ，但你会得到一个Expr Var.

为了解决这个问题，您可以创建一个存在包装器，如 @iceland_jack 的答案中所述。该类型的BaseExpr -> Exists @ExprType Expr真正含义是“如果你给我一个BaseExpr，我会给你一个我确定的某个aExpr a。”，这正是你的函数所做的。