在确保终止的同时键入级别固定点

Question

可以表示unFix 的总和？可能通过限制f 是什么？

record Fix (f : Type -> Type) where
    constructor MkFix
    unFix : f (Fix f)

> :total unFix
Fix.unFix is possibly not total due to:
    MkFix, which is not strictly positive

Answer 1

这里的问题是 Idris 无法知道您用于数据类型的基本函子是严格正数的。如果它接受你的定义，那么你可以将它与一个具体的负函子一起使用，并从中证明Void。

有两种方法可以表示严格的正函子：定义一个 Universe 或使用容器。我已经把所有东西都放在了two self-contained gists（但是那里没有 cmets）。

严格正函子的宇宙

您可以从基本表示开始：我们可以将函子分解为 sigma 类型 (Sig)、递归子结构的（严格正数）位置 (Rec) 或什么都没有 (@987654325 @)。这给了我们这个描述和它作为Type -> Type函数的解码：

-- A universe of positive functor
data Desc : Type where
  Sig : (a : Type) -> (a -> Desc) -> Desc
  Rec : Desc -> Desc
  End : Desc


-- The decoding function
desc : Desc -> Type -> Type
desc (Sig a d) x = (v : a ** desc (d v) x)
desc (Rec d)   x = (x, desc d x)
desc End       x = ()

一旦你拥有了这个保证严格正数的函子宇宙，你就可以取它们的最小固定点：

-- The least fixpoint of such a positive functor
data Mu : Desc -> Type where
  In : desc d (Mu d) -> Mu d

您现在可以定义自己喜欢的数据类型。

示例：自然

我们从每个构造函数的总和类型开始。

data NatC = ZERO | SUCC

然后，我们通过将构造函数标记存储在 sigma 中并根据标记值计算描述的其余部分来定义严格的正基函子。 ZERO 标记与End 相关联（在zero 构造函数中没有其他内容可存储），而SUCC 需要Rec End，也就是说一个与Nat 的前身相对应的递归子结构。

natD : Desc
natD = Sig NatC $ \ c => case c of
  ZERO => End
  SUCC => Rec End

我们的归纳类型然后通过取描述的固定点来获得：

nat : Type
nat = Mu natD

我们可以自然地恢复我们期望的构造函数：

zero : nat
zero = In (ZERO ** ())

succ : nat -> nat
succ n = In (SUCC ** (n, ()))

参考文献

这个特定的宇宙取自 McBride 的“Ornamental Algebras, Algebraic Ornaments”，但您可以在 Chapman、Dagand、McBride 和 Morris 的“The Gentle Art of Levitation”中找到更多细节。

严格正函子作为容器的扩展

第二种表示基于另一种分解：每个归纳类型都被视为一般形状（即其构造函数和它们存储的数据）加上许多递归位置（可能取决于形状的特定值）。

record Container where
  constructor MkContainer
  shape : Type
  position : shape -> Type

我们可以再次将其解释为Type -> Type 函数：

container : Container -> Type -> Type
container (MkContainer s p) x = (v : s ** p v -> x)

并取如此定义的严格正函子的不动点：

data W : Container -> Type where
  In : container c (W c) -> W c

您可以通过定义感兴趣的Containers 再次恢复您最喜欢的数据类型。

示例：自然

自然数有两个构造函数，每个构造函数都不存储任何内容。所以形状将是Bool。如果我们处于zero 的情况下，则没有递归位置（Void），而在succ 中，只有一个位置（()）。

natC : Container
natC = MkContainer Bool (\ b => if b then Void else ())

我们的类型是通过取容器的fixpoint得到的：

nat : Type
nat = W natC

我们可以恢复通常的构造函数：

zero : nat
zero = In (True ** \ v => absurd v)

succ : nat -> nat
succ n = In (False ** \ _ => n)

参考文献

这是基于 Abbott、Altenkirch 和 Ghani 的“容器：构造严格的正类型”。