haskell - 使用 GADT 的递归类型代表

Question

我有以下可以表示基本代数数据类型的 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))

这适用于非递归类型，但我也想包括其他类型，如列表和树，而无需手动添加它们。类型构造函数可以表示为函数 Type a -> Type b，例如，maybeConstr a = TUnit :+ a。但是，我不能把它变成 Nat 的递归定义。使用 fix 不起作用，因为输入和输出类型不匹配。此外，如果我想为类型编写相等函数，则将类型构造函数表示为函数似乎会出现问题。有什么好的方法可以做到这一点吗？

Answer 1

您可以使用不动点表示递归类型，方法是添加构造函数 TMu 来表示递归类型 μx。 t。这是一种可以“展开”为类型 t 的类型，其中 x 替换为 μx 的另一个副本。 t:t[μx。 t/x]。例如，列表类型可以写成 L(a) = μx。 1 + a × x；类型变量 x 表示整个类型 L(a)。 (从技术上讲，这是最大不动点 ν，而 μ 是最小不动点，但如果我们不关心两者的区别，通常将 μ 用于两者。)

为了使用它，您需要一些类型变量的表示；用类型化的 AST 表示这一点的通用方法是在 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，这里的∀很像术语级别的λ。因此，您需要将TForall 和TApp 构造函数添加到Type，并使用TVar 构造函数来引用它们绑定(bind)的变量。

这引发了两个问题。首先，您现在也需要考虑 种类，尽管如果您的类型参数都是基本类型(即不是类型构造函数)，则不需要显式表示它们。其次，您当前直接使用 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

然后data Type::* -> *变成data Type::UType -> *，使用DataKinds:

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 类型进行解释。

De Bruijn 表示使得在 Type 上推导相等变得容易，但是这里有几种可能的变量绑定(bind)表示，例如变量名、“本地无名”、“高阶抽象”语法”(HOAS)，或仅使用无点类型组合器。