伊德里斯向量与链表

Question

伊德里斯在向量下是否进行了任何优化？因为从外观上看，Idris 向量只是一个已知大小(编译时已知(的链表。事实上，一般来说，你似乎可以表达以下等效性(我在语法上有点猜测(：

Vector : Nat -> Type -> Type
Vector n t = (l: List t ** length l = n)

因此，虽然这在防止范围误差的意义上很好，但向量(在该术语的传统用法中(的真正优势在于性能;特别是O(1(随机访问。似乎 idris 向量不支持这一点(您将如何编写索引函数以获得这种性能？

• 假设引擎盖下没有魔法(就像Nat一样(来重新配置 Vector s，那么 Idris 中是否有随机访问数据类型？
在
• 代数类型系统中如何定义这样的东西？当然，似乎不可能归纳地定义它。
• 在像 Idris这样的类型系统中，是否有可能创建一个支持 O(1( 随机访问的数据类型，并知道其长度，以便所有访问都证明有效？(Haskell有数组风格的向量，但它们的具体实现对普通用户来说是不透明的，包括我(

Answer 1

它没有做任何事情来优化矢量查找(至少在撰写此答案时(。

这并不是因为这样做有任何困难，而是因为我宁愿有某种通用框架来编写这种优化，而不是硬编码很多。诚然，我们已经为Nat进行了硬编码优化，但我仍然不希望以临时方式添加更多负载。

根据你实际想要它的目的，实验性唯一性类型系统可能会有所帮助，因为你可以在引擎盖下有一个低级可变的东西，并且仍然可以安全有效地访问和更新在高级语言的纯风格中。我们拭目以待...

Answer 2

埃德温对伊德里斯目前的工作有明确的答案。 但是，如果您正在寻找在某些情况下优化为恒定时间查找的自然内容，那么以下内容可能是朝着正确方向迈出的一步。

对于编译时固定大小的向量(即，不在 lambda 下，不在顶级按长度参数化(，以下结构为您提供了向量和查找函数，对于任何固定的具体长度，可以在编译时规范化为应该可以直接优化为常量时间函数的函数。 (抱歉，代码在 Coq 中;我目前没有伊德里斯的工作版本，也不太了解它。 如果有人建议正确的语法，例如在评论中，我很乐意用 Idris 代码替换它。

Fixpoint vector (n : nat) (A : Type) :=
  match n return Type with
    | 0 => unit
    | S n' => (A * vector n' A)%type
  end.
Definition nil {A} : vector 0 A := tt.
Definition cons {n} {A : Prop} (x : A) (xs : vector n A) : vector (S n) A
  := (x, xs).
Fixpoint get {n} {A : Prop} (m : nat) (default : A) (v : vector n A) {struct n} : A
  := match n as n return vector n A -> A with
       | 0 => fun _ => default
       | S n' => match m with
                   | 0 => fun v => fst v
                   | S m' => fun v => @get n' A m' default (snd v)
                 end
     end v.

这个想法是，对于任何固定的 n，get的正常形式是非递归的，因此编译器可以假设地将其编译为一个函数，其运行时与 n 碰巧是什么无关。