1

我刚刚开始学习 Idris，我想一个不错的小项目可以开始将有限序列实现为 2-3 个手指树。树中的每个内部节点都需要在运行时使用存储在其下方的元素总数进行注释，以支持快速拆分和索引。这个大小信息也需要在编译时进行管理，以便（最终）证明用适当的索引分割和用另一个序列压缩一个序列是全部操作。

我可以想到两种方法来解决这个问题：

  1. 我目前正在做的事情，只写了一小部分必要的代码：完全在类型中处理大小，然后使用类似的东西proof {intros; exact s;}来处理它们。我不知道这可能会产生什么可怕的效率后果（如果有的话）。在我心中的潜力中：a）不必要地为每个叶节点存储一个大小。b) 我认为这不太可能，但如果它坚持自下而上而不是懒惰地自上而下计算尺寸，那将是非常糟糕的。

  2. 在每个节点构造函数中包含显式大小字段，以及大小字段中的数字与类型系统所需大小匹配的证明。这种方法似乎非常尴尬。从好的方面来说，我应该能够非常确定类型级别的数字和相等性证明会被删除，在运行时每个内部节点只留下一个数字。

如果有的话，哪一个是正确的方法？

当前代码

请随时提供样式提示，并可能解释如何内联尺寸代码。我只能以交互方式弄清楚要做什么，但是在底部为如此简单的事情提供证明似乎有点奇怪。

data Tree23 : Nat -> Nat -> Type -> Type where
    Elem : a -> Tree23 0 1 a
    Node2 : Lazy (Tree23 d s1 a) -> Lazy (Tree23 d s2 a) ->
            Tree23 (S d) (s1 + s2) a
    Node3 : Lazy (Tree23 d s1 a) -> Lazy (Tree23 d s2 a) -> Lazy (Tree23 d s3 a) ->
              Tree23 (S d) (s1 + s2 + s3) a

size23 : Tree23 d s a -> Nat
size23 t = ?size23RHS

data Digit : Nat -> Nat -> Type -> Type where
  One : Lazy (Tree23 d s a) -> Digit d s a
  Two : Lazy (Tree23 d s1 a) -> Lazy (Tree23 d s2 a) -> Digit d (s1+s2) a
  Three : Lazy (Tree23 d s1 a) -> Lazy (Tree23 d s2 a) ->
          Lazy (Tree23 d s3 a) -> Digit d (s1+s2+s3) a
  Four : Lazy (Tree23 d s1 a) -> Lazy (Tree23 d s2 a) ->
          Lazy (Tree23 d s3 a) -> Lazy (Tree23 d s4 a) -> Digit d (s1+s2+s3+s4) a

sizeDig : Digit d s a -> Nat
sizeDig t = ?sizeDigRHS

data FingerTree : Nat -> Nat -> Type -> Type where
  Empty : FingerTree d 0 a
  Single : Tree23 d s a -> FingerTree d s a
  Deep : Digit d spr a -> Lazy (FingerTree (S d) sm a) -> Digit d ssf a ->
         FingerTree d (spr + sm + ssf) a

data Seq' : Nat -> Type -> Type where
  MkSeq' : FingerTree 0 n a -> Seq' n a

Seq : Type -> Type
Seq a = (n ** Seq' n a)

---------- Proofs ----------

try.sizeDigRHS = proof
  intros
  exact s

try.size23RHS = proof
  intros
  exact s

编辑

我探索过的另一个选择是尝试将数据结构与其有效性分开。这导致以下情况：

data Tree23 : Nat -> Type -> Type where
    Elem : a -> Tree23 0 a
    Node2 : Nat -> Lazy (Tree23 d a) -> Lazy (Tree23 d a) ->
            Tree23 (S d) a
    Node3 : Nat -> Lazy (Tree23 d a) -> Lazy (Tree23 d a) -> Lazy (Tree23 d a) ->
              Tree23 (S d) a

size23 : Tree23 d a -> Nat
size23 (Elem x) = 1
size23 (Node2 s _ _) = s
size23 (Node3 s _ _ _) = s

data Valid23 : Tree23 d a -> Type where
  ElemValid : Valid23 (Elem x)
  Node2Valid : Valid23 x -> Valid23 y -> Valid23 (Node2 (size23 x + size23 y) x y)
  Node3Valid : Valid23 x -> Valid23 y -> Valid23 z
    -> Valid23 (Node3 (size23 x + size23 y + size23 z) x y z)

data Digit : Nat -> Type -> Type where
  One : Lazy (Tree23 d a) -> Digit d a
  Two : Lazy (Tree23 d a) -> Lazy (Tree23 d a) -> Digit d a
  Three : Lazy (Tree23 d a) -> Lazy (Tree23 d a) ->
          Lazy (Tree23 d a) -> Digit d a
  Four : Lazy (Tree23 d a) -> Lazy (Tree23 d a) ->
          Lazy (Tree23 d a) -> Lazy (Tree23 d a) -> Digit d a

data ValidDig : Digit d a -> Type where
  OneValid : Valid23 x -> ValidDig (One x)
  TwoValid : Valid23 x -> Valid23 y -> ValidDig (Two x y)
  ThreeValid : Valid23 x -> Valid23 y -> Valid23 z -> ValidDig (Three x y z)
  FourValid : Valid23 x -> Valid23 y -> Valid23 z -> Valid23 w -> ValidDig (Four x y z w)

sizeDig : Digit d a -> Nat
sizeDig (One x) = size23 x
sizeDig (Two x y) = size23 x + size23 y
sizeDig (Three x y z) = size23 x + size23 y + size23 z
sizeDig (Four x y z w) = (size23 x + size23 y) + (size23 z + size23 w)

data FingerTree : Nat -> Type -> Type where
  Empty : FingerTree d a
  Single : Tree23 d a -> FingerTree d a
  Deep : Nat -> Digit d a -> Lazy (FingerTree (S d) a) -> Digit d a ->
         FingerTree d a

sizeFT : FingerTree d a -> Nat
sizeFT Empty = 0
sizeFT (Single x) = size23 x
sizeFT (Deep k x y z) = k

data ValidFT : FingerTree d a -> Type where
  ValidEmpty : ValidFT Empty
  ValidSingle : Valid23 x -> ValidFT (Single x)
  ValidDeep : ValidDig pr -> ValidFT m -> ValidDig sf ->
              ValidFT (Deep (sizeDig pr + sizeFT m + sizeDig sf) pr m sf)

record Seq : Type -> Type where
  MkSeq : FingerTree 0 a -> Seq a

data ValidSeq : Seq a -> Type where
  MkValidSeq : ValidFT t -> ValidSeq (MkSeq t)

然后每个函数都附有一个（单独的）其有效性证明。

我有点喜欢这种方法将“代码”与“证明”分开的方式，但我遇到了几个问题：

  1. 虽然“代码”变得更容易，但证明似乎更难构建。我想其中很大一部分可能是我不熟悉系统的结果。

  2. 我实际上还没有接近编写此代码的地步，但是索引、拆分和压缩功能都必须坚持获得其输入有效性的证明。有些函数只使用序列，而另一些函数坚持证明，这似乎有点奇怪，但也许这只是我。

4

1 回答 1

1

您的问题可以简化为具有类似的类型

data Steps : Nat -> Type where
  Nil : Steps 0
  Cons : Steps n -> Steps (S n)

并想写

size : Steps n -> Nat

这很容易做到，因为隐式量化的参数（n在这种情况下）作为隐式参数传递给size！所以上面的类型size是一样的

size : {n : _} -> Steps n -> Nat

这意味着它可以定义为

size {n} _ = n
于 2015-03-27T05:07:58.657 回答