确保终止时的类型级别修复点

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或使用容器.我把所有东西放在两个独立的要点(但那里没有评论).

一个严格积极乐趣的宇宙

您可以从一个基本表示开始:我们可以将一个仿函数分解为sigma类型(Sig),递归子结构(严格为正)位置(Rec或根本没有End)().这给了我们这个描述及其解码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

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

示例:Nat

我们从每个构造函数的标记类型开始.

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 Lentle 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

您可以通过定义Container感兴趣的内容再次恢复您喜欢的数据类型.

示例:Nat

自然数有两个构造函数,每个构造函数都没有存储.所以形状将是一个Bool.如果我们在这种zero情况下那么没有递归位置(Void),并且在那个succ中只有一个(()).

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

我们的类型是通过获取容器的固定点获得的:

nat : Type
nat = W natC

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

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

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

参考

这是基于Abbott,Altenkirch和Ghani的"容器:构建严格正面类型".