Idris向量 vs 链表

Question

Idris在向量的底层是否进行任何优化？因为从外表看，Idris向量只是一个已知大小（在编译时已知）的链表。实际上，一般情况下，您可以表示以下等式（我猜测一下语法）：

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

因此，虽然这种方法可以避免范围错误，但向量（在传统意义上）的真正优势在于性能，特别是O(1)的随机访问。似乎idris向量不支持这一点（你如何编写索引函数以实现这种性能？）。

假设没有任何巫术在底层运行（就像“Nat”一样），以重新配置向量，“Idris”中是否有随机访问数据类型？

在代数类型系统中，这样的事情将如何被定义？当然，似乎不可能在归纳上定义它。

在像Idris这样的类型系统中，是否可能创建一个数据类型，支持O(1)的随机访问，并且知道其长度，以便所有访问都可以得到证明是有效的？（Haskell有类似数组的向量，但它们的具体实现对于普通用户（包括我）来说是不透明的）

- limp_chimp

Answer 1

它并没有对向量查找进行任何优化（至少在撰写本回答时是如此）。

这并不是因为很难做到，而是因为我更喜欢有一种通用的框架来编写这种优化，而不是硬编码大量的优化。诚然，我们已经针对 Nat 进行了硬编码优化，但我仍然不愿意以临时方式添加更多的代码。

根据您实际想要的内容，实验性的唯一类型系统可能会有所帮助，在高级语言中你可以拥有一个底层可变的东西，并且在保持纯风格的同时进行安全和有效的访问和更新。我们拭目以待...

- Edwin Brady

Answer 2

Edwin对于Idris当前的功能有权威答案。不过，如果你正在寻找一些在某些情况下可能自然而然地优化为常数时间查找的东西，则以下内容可能是朝着正确方向迈出的一步。

对于编译时固定大小的向量（即，在 lambda 下没有，顶层不是长度参数化的），以下结构为您提供了向量和查找函数，对于任何固定的具体长度，都可以将它们规范化为编译时函数，应该可以相对简单地优化为常数时间函数。(抱歉，代码在 Coq 中；我现在没有可用的 Idris 版本，并且不太熟悉它。如果有人建议正确的语法（例如在注释中），我很乐意用 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无关。

- Jason Gross

---

原始问题涉及 O(1) 访问元素。很明显，如果你固定 n，那么访问时间将是恒定的。 - jch

我已经编辑了最后一句话，希望能更清楚地表达以下观点：在使用 n 的任何地方，都必须将其固定到一个值。它应该作为编译时固定 n 值的函数是 O(1)。也就是说，在一个假设的世界中，Idris可以将 A * B * ... * C 编译成一个数组，当你插入 n = 5 时，绝对运行时间应该与插入 n = 100000 相同，但只有在编译时才能实现这一点。 - Jason Gross