在编译时和运行时使用数字的最佳方法是什么？

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

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

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

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

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

当前代码

请随意提供样式提示，也许可以解释如何内联大小代码 . 我只能弄清楚交互式做什么，但是对于这些简单的事情，在底部有证据似乎有点奇怪 .

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)

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

我有点像这种方法将“代码”与“证据”分开的方式，但我遇到了一些问题：

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

• 我实际上并没有接近我将编写此代码的点，但索引，拆分和压缩函数都必须坚持获得其输入有效性的证明 . 对于某些函数来说，只使用序列似乎有点奇怪，而其他函数则坚持使用证据，但也许这只是我 .