递归类型代表使用广义代数数据类型（GADTs）

Question

递归类型代表使用广义代数数据类型（GADTs）

3

我有以下GADT，它可以表示基本的代数数据类型。

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}

data Type :: * -> * where
  TUnit   :: Type ()
  TInt    :: Type Int
  (:+)    :: Type a -> Type b -> Type (Either a b)
  (:*)    :: Type a -> Type b -> Type (a, b)
  (:>)    :: Type a -> Type b -> Type (a -> b)
deriving instance Show (Type a)

我可以与以下GADT一起使用，创建具有在运行时可用的类型的值。

data Value where
  MkVal :: a -> Type a -> Value

someVal = MkVal (+) (TInt :> (TInt :> TInt))

这对于非递归类型效果很好，但我还想包括其他类型，如列表和树，而不需要手动添加它们。类型构造器可以表示为一个函数，例如maybeConstr a = TUnit :+ a。然而，我无法将其转化为Nat的递归定义。使用fix不起作用，因为输入和输出类型不匹配。此外，将类型构造器表示为函数似乎可能会在编写类型的等式函数时出现问题。有什么好方法来完成这个任务吗？

- vigenary

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Jon Purdy · Accepted Answer

你可以使用一个固定点来表示递归类型，通过添加构造函数TMu来表示递归类型μx. t。这是一种类型，可以将其“展开”为类型t，其中x用μx的另一个副本替换。 t: t[μx. t/x]。例如，列表类型可以写成L(a) = μx. 1 + a × x；类型变量x表示整个类型L(a)。（严格来说，这是最大不动点ν，而μ是最小不动点，但如果我们不关心区别，则通常对两者都使用μ。）

为了使用这个，你需要一些类型变量的表示方法；一种通用的方法是在GADT的类型参数中包含“环境”的类型，并使用De Bruijn指数索引到该环境中。

data Type :: [*] -> * -> * where
  TUnit   :: Type c ()
  TInt    :: Type c Int
  (:+)    :: Type c a -> Type c b -> Type c (Either a b)
  (:*)    :: Type c a -> Type c b -> Type c (a, b)
  (:>)    :: Type c a -> Type c b -> Type c (a -> b)

  TMu     :: Type (a ': c) b -> Type c (Mu a b)
  TVarZ   :: Type (a ': c) a
  TVarS   :: Type c a -> Type (x ': c) a

TVarZ 引用环境栈顶的变量，TVarS 将上下文转移到环境的其他部分。如果您永远不需要嵌套递归类型，可以没有 TVarS，并将 TVarZ 称为 TSelf 或 TRec。

从正式方面来看，GADT 的每个构造函数对应于您正在表示的类型系统的一个规则：Type γ α → Type γ β → Type γ (α × β) 直接对应于序言 (Γ ⊢ α) ∧ (Γ ⊢ β) ⇒ (Γ ⊢ α × β)。

如果您想要在 Type 中表示类型构造函数，则过程类似： Maybe a ≅ 1 + a 也可以被视为 Maybe ≅ ∀a. 1 + a，其中此处的 ∀ 很像术语级别的 λ。因此，您需要向 Type 添加 TForall 和 TApp 构造函数，并使用 TVar 构造函数引用它们绑定的变量。

这带来了两个问题。首先，现在您需要考虑 kind，但如果您的类型参数都是基本类型（即不是类型构造函数），则不需要显式表示它们。其次，您当前正在直接使用 Haskell 类型索引 GADT，但是如果直接使用 TForall :: Type (a ': c) b -> Type c (forall a. b)，则会遇到问题；典型的解决方案是创建 AST 类型的基本“未标记”版本：

data UType where
  UTUnit   :: UType
  UTInt    :: UType
  UTSum    :: UType -> UType -> UType
  UTProd   :: UType -> UType -> UType
  UTFun    :: UType -> UType -> UType

使用 DataKinds，data Type :: * -> * 变成了 data Type :: UType -> *：

data Type :: * -> * where
  TUnit   :: Type 'UTUnit
  TInt    :: Type 'UTInt
  (:+)    :: Type a -> Type b -> Type ('UTSum a b)
  (:*)    :: Type a -> Type b -> Type ('UTProd a b)
  (:>)    :: Type a -> Type b -> Type ('UTFun a b)

（这基本上是“单例”形式的UType。）

然后，您可以为上述情况扩展它，并将其解释为Haskell类型。

德布鲁因表示法使得在Type上推导相等变得容易，但这里有几种可能的变量绑定表示方式，例如变量名称，“局部无名”，“高阶抽象语法”（HOAS），或仅使用点无类型组合器。