coq - Coq 中的无限递归类型(用于 Bananas 和 Lenses)
问题描述
我希望看到香蕉、镜头等的 Coq 版本。它们是在sumtypeofway 递归方案简介的优秀系列博客文章中建立的
然而,博客文章是在 Haskell 中的,它允许无限的非终止递归,因此完全满足于Y
组合器。哪个 Coq 不是。
特别是,定义取决于类型
newtype Term f = In { out :: f (Term f) }
它构建了无限类型 f (f (f (f ...)))
。 Term f
允许使用 Term 类型族对 catamorphisms、paramorphisms、anamorphisms 等进行非常漂亮和简洁的定义。
尝试将此移植到 Coq
Inductive Term f : Type := {out:f (Term f)}.
给了我预期的
Error: Non strictly positive occurrence of "Term" in "f (Term f) -> Term f".
问:在 Coq 中形式化上述 Haskell Term 类型的好方法是什么?
上面f
是 type Type->Type
,但也许它太笼统了,可能有一些方法可以限制我们使用归纳类型,使得每个应用程序 都f
在减少?
也许有人已经在 Coq 中实现了Banans、Lenses、Envelopes的递归方案?
解决方案
我认为流行的解决方案是将函子编码为“容器”,这篇论文的介绍是一个很好的起点:https ://arxiv.org/pdf/1805.08059.pdf这个想法要老得多(论文的意思是给出一个自包含的解释),你可以从那篇论文中寻找参考资料,但如果你不熟悉类型论或范畴论,我在粗略的搜索中发现的内容可能很难理解。
简而言之,Type -> Type
我们使用以下类型来代替 :
Set Implicit Arguments.
Set Contextual Implicit.
Record container : Type := {
shape : Type;
pos : shape -> Type;
}.
F
粗略地,如果你想象一个递归类型的“基本函子” Fix F
,shape
描述 的构造函数F
,并且对于每个构造函数,pos
枚举其中的“孔”。所以基函子List
data ListF a x
= NilF -- no holes
| ConsF a x -- one hole x
由这个容器给出:
Inductive list_shape a :=
| NilF : list_shape a
| ConsF : a -> list_shape a.
Definition list_pos a (s : list_shape a) : Type :=
match s with
| NilF => False (* no holes *)
| ConsF _ => True (* one hole x *)
end.
Definition list_container a : container := {|
shape := list_shape a;
pos := fun s => list_pos s;
|}.
关键是这个容器描述了一个严格的正函子:
Inductive ext (c : container) (a : Type) : Type := {
this_shape : shape c;
this_rec : pos c this_shape -> a;
}.
Definition listF a : Type -> Type := ext (list_container a).
因此Fix f = f (Fix f)
,fixpoint 构造可以取一个容器,而不是 :
Inductive Fix (c : container) : Type := MkFix : ext c (Fix c) -> Fix c.
并非所有仿函数都可以编码为容器(延续仿函数就是一个典型的例子),但你不会经常看到它们与Fix
.
完整要点:https ://gist.github.com/Lysxia/21dd5fc7b79ced410b129f31ddf25c12
推荐阅读
- git - 是否可以对 git-for-each-ref 的“输入”和输出进行不同的排序?
- android - Program type already present: Google Services Auth
- javascript - 使用 JavaScript 在某些单词之间进行匹配
- python - Adding header/column to my .csv file
- javascript - 如何获得特定的在 android webview 中使用 js 的 id 数据?
- python-3.x - 使用 Imaplib 在 python 中访问电子邮件内容的不同方法是什么?
- r - 如何在 stringr 中的两个模式或 r 中的 stringi 之间应用 string_extract
- spring-boot - Spring Boot ConfigurationProperties 问题
- flask - Flask:从数据库内容动态填充的表单
- linux - 用另一个列表中的下一行替换列表中的字符串