我一直在使用Pierce的《类型和编程语言》中的Rust实现System F-omega,想要添加iso-recursive的fold
/unfold
运算符来实现递归类型,并寻求指导。已经添加了和、积、记录、存在和全局类型。
在System F(没有类型操作符)中,我发现这相对简单,只需在解析后通过AST进行访问器遍历,在情况分析或类型构建期间执行折叠/展开同构即可。
而对于System F omega,由于类型层面存在lambda抽象,情况则较为复杂。例如(使用标准lambda-calc/haskell-ish语法),假设我想定义一个参数化的List
数据类型。
datatype List a = Cons a (List a) | Nil
这可以被编码在我们的演算中(省略*种类):
type List = μ ΛX::*=>*. ΛA. Cons A (X A) | Nil
substs to: ΛA. Cons A ((μ ΛX::*=>*. ΛA. Cons A (X A) | Nil) A) | Nil
但是,一旦我们试图展开值,就会遇到问题,因为引入了一个新的抽象来再次绑定A
。这似乎可能有效,只要我们在某个地方存储了具体类型A。
或者我们可以将其“lambda降级”为:
type ListF = ΛX. ΛA. Cons (A, X) | Nil
type List = ΛA. μ (ListF A)
lambda删除对于像这样简单的递归类型非常有效,并且也很容易实现,我可以设想一种自动生成ListF类型的方式。但是我有一种烦恼的感觉,似乎有什么不对劲。我一直在尝试阅读围绕此主题的文献(Mendler-style迭代、Andreas Abel、Ralph Matthes、Tarmo Uustalu,“Iteration and coiteration schemes for higher-order and nested datatypes”等),但说实话有些内容让我有点力不从心,而且我不知道如何以具体的方式实现它。任何建议都将不胜感激。
List
应该展开为Cons A ((μ ...) A) | Nil
,而不是Cons A (μ ...) | Nil
(即,μ应该应用于A)。这可能是混淆的源头吗?这确实使类型检查变得困难,但这似乎不是您关心的问题,是吗? - Li-yao Xia