你可以使用一个固定点来表示递归类型,通过添加构造函数
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),或仅使用点无类型组合器。
(:+)
、(:*)
和(:>)
这些类型中,您指出输入具有相同的上下文,因此无法组合,例如 TInt 和 TVarZ。这是否需要一些类型级联接?其次,Mu a b
的定义是什么?我尝试适应定义Mu f = Mu (forall r. (f r -> r) -> r
,但没有成功,因为在我们的情况下,b
不是一个类型构造函数。 - vigenary'[]
应该是一个多态的c
,我没有理由使它线性化。但你是对的,如果你想要组合多个上下文,你需要例如type family (++) :: [k] -> [k] -> [k]
。我认为我过于复杂化了TMu
,它应该更像TMu :: Type (a ': c) a -> Type c a
(参见fix :: (a -> a) -> a
的类型)。这里的a
是整个类型,所以它是一个基本类型,而不是一个构造函数。我很确定我在一篇论文中看到过这个解释……会尽快找到参考资料或写一个更完整的例子。 - Jon Purdy