将 GADT 与 DataKind 一起用于函数中的类型级数据构造函数约束

Question

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

{-# LANGUAGE KindSignatures, DataKinds, GADTs #-}
module NewGadt where

data ExprType = Var | Nest

data Expr (a :: ExprType) where
  ExprVar :: String -> Expr Var
  ExprNest :: Expr a -> Expr Nest

data BaseExpr
  = BaseExprVar String
  | BaseExprNest BaseExpr

translate :: BaseExpr -> Expr a
translate (BaseExprVar id) = ExprVar id
translate (BaseExprNest expr) = ExprNest $ translate expr

编译错误：

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

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

printVariable :: Expr Var -> IO ()
printVariable (ExprVar id) = putStrLn id

printNested :: Expr Nest -> IO ()
printNested (ExprNest inner) = putStrLn "nested expression"

printExpr :: Expr a -> IO ()
printExpr expr@ExprVar {} = printVariable expr
printExpr expr@ExprNest {} = printNested expr

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

有什么方法可以让翻译功能 return Expr a 像这样？或者这是对 DataKinds 和 GADTs 的不当使用？

编辑：

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

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

和returnExists Expr

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

这使用pattern guards解压存在类型

pattern guards are of the form p <- e, where p is a pattern (see Section 3.17) of type t and e is an expression type t1. They succeed if the expression e matches the pattern p, and introduce the bindings of the pattern to the environment.

Haskell Report

并且相当于这些

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

{-# Language ViewPatterns #-}

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

但是用 let 或 where 试一下，还是不行。

参考资料

Answer 2

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

要解决这个问题，您可以创建一个存在性包装器，如@iceland_jack 的回答中所述。类型 BaseExpr -> Exists @ExprType Expr 的真正意思是“如果你给我一个 BaseExpr，我会给你一个 Expr a，因为 一些我确定的 。” ，这正是您的函数所做的。

Answer 3

为什么您的原始代码不起作用？

此类型不可用：

translate :: BaseExpr -> Expr a

记住意味着在Haskell中的类型变量。 translate 的这种类型表示“对于 translate 的调用者选择的任何类型 a，它将采用 BaseExpr 并将其转换为 Expr a”。

因此，如果我想将 BaseExprVar "variableName" 传递给 translate 并接收 Expr Nest，我应该能够做到；我只选择 a 为 Nest。这个特定的 BaseExpr 只是一个变量，而不是嵌套表达式并不重要，并且没有 Expr Nest 类型的值忠实地表示这一点。将多态 GADT 作为 return 类型，这不是 my 的问题，而是 translate 的问题，因为 translate 的类型承诺是能够想出这样的价值。 translate 不能强迫我为 a 选择 Var。

这不是您想要的类型。您不希望 returned 的 Expr 类型被 translate 的 caller 选择，您希望它被选择通过translate的实现（因此它可以return适合BaseExpr内容的任何类型）。

要让函数的实现选择类型参数，您需要使用存在性包装器，或者使用更高级别的类型和延续传递。

存在包装器

data SomeExpr
  where SomeExpr :: Expr a -> SomeExpr

translate :: BaseExpr -> SomeExpr
translate (BaseExprVar id) = Some (ExprVar id)
translate (BaseExprNest expr)
  = case translate expr of
      Some e -> Some (ExprNest e)

请注意 Expr 的类型参数 而不是 出现在 translate 的类型中，因此 translate 的调用者不会'不需要指定它应该是什么。

要使用 translate 的输出，您需要在 Some 构造函数上进行模式匹配，这将为您提供一个 Expr a 类型的值，用于某些未知 [=14] =]（与 translate 的原始尝试相反，它为您选择的某些特定 a 提供类型 Expr a 的值）。因此，在模式匹配中，您必须处理 a 的任何可能值，并且结果值不能具有依赖于 a 的类型（我们只允许在模式中“看到”它匹配）。

你可以在递归调用中看到上面的例子； translate expr returned Some Expr，但是我们需要在 ExprNest 构造函数中包装的是 Expr a。通过Some上的模式匹配，我们得到包含的Expr a，然后我们可以将其放入ExprNest构造函数中以获得类型Expr Nest的值。然后我们将其隐藏在 Some 构造函数中，最后将正确的类型从 translate.

变为 return

您当然也可以概括存在性包装器，使其适用于更多类型，而不仅仅是 Expr，如@Iceland_jack 的回答所示。我在这里使用的表格没有什么特别之处；它本身只是 GADT 语法的另一种用法（嵌入一个带有未在整体类型中公开的类型参数的值）。一个通用的很好，但通常你会想要一些类型 class 对隐藏类型的约束，这样你就可以在模式匹配时用值做更多的事情在它上面，因此您需要变得更复杂才能使类型足够通用，以便在您需要存在性包装器时随时重用。

更高级别的类型

根据正在处理的数据处理 translate 到 return 不同类型的要求的另一种方法是使用更高级别的类型。为此，您需要 {-# LANGUAGE RankNTypes #-} 扩展名。

translate :: BaseExpr -> (forall a. Expr a -> r) -> r
translate (BaseExprVar id) handler = handler (ExprVar id)
translate (BaseExprNest expr) handler
  = handler (translate expr ExprNest)

在这里，我们没有使用额外的包装器类型来“隐藏”类型变量，而是重构 translate 以便它采用 Expr 的“处理函数”。现在 translate 根本没有 return 任何形式的 Expr，而是生成一个，将其传递给 handler，return 处理程序 returns.

为什么这样做？诀窍是handler需要作为多态函数传递给translate。 translate 参数之一的类型中嵌套的 forall a. 意味着调用者不会像通常那样选择 a，相反，调用者需要传递一个有效的函数任何可能 a。处理函数的代码类似于existential wrapper版本中的“inside of the pattern match”；它必须处理任何可能的 a 而不能 return 类型依赖于 a.

的任何东西
因为调用者必须传递适用于任何 a 的 handler，translate 的代码可以在任何它喜欢的类型上使用它，包括在不同的不同类型上分支机构。因此 translate 的第一种情况可以选择 Var 并将 handler 用作 Expr Var -> r，而第二种情况可以选择 Nest 并将处理程序用作 Expr Nest -> r ].

请注意第二种情况的微妙之处。现在translate需要递归调用自己的时候，需要传递一个“处理函数”。我们可以尝试传递从顶部接收到的处理程序，但这是不对的。我们应该只在 complete Expr 上调用该处理程序一次，而不是在 BaseExpr 的每个级别调用它。此外，这只会给我们一个 r，这不是我们需要在 ExprNest 构造函数中包装的内容。相反，我们需要意识到 ExprNest 是本身类型 forall a. Expr a -> Expr Nest 的函数，它符合我们需要的处理函数类型！使用 ExprNest 构造函数翻译嵌套表达式作为处理程序将翻译其中的任何内容，然后将其提供给构造函数，return 向我们提供我们需要提供的完整 Expr Nest 值顶级处理程序。

在这个特定的例子中，更高级别的版本最终使用的样板文件少于存在包装版本。通常是这种情况，但一个可能的缺点是它会让您将一些调用代码重组为连续传递形式；你不能只调用 translate 然后使用结果值，你必须构造一个函数来实现你会对翻译后的表达式所做的事情，如果你有的话，然后将该函数传递给 translate。有时这种编码风格更难 read/write.

将 GADT 与 DataKind 一起用于函数中的类型级数据构造函数约束

Using GADTs with DataKinds for type level data constructor constraints in functions

haskell

gadt

existential-type

data-kinds

为什么您的原始代码不起作用？

存在包装器

更高级别的类型