Idris向量与链表
Idris在向量的掩护下做了什么优化吗？因为从外观上看，Idris向量只是一个已知大小的链表(编译时已知)。实际上，一般来说，您似乎可以表示以下等价性(我猜在语法上有一点)：
Vector : Nat -> Type -> Type
Vector n t = (l: List t ** length l = n)因此，虽然这在防止距离误差方面很好，但向量的真正优势(在传统术语的用法中)是在性能方面，特别是在O(1)随机访问方面。idris向量似乎不支持这种功能(如何编写索引函数以获得这种性能？)
- 假设在引擎盖下没有魔法(就像
Nat一样)来重新配置Vector，Idris中是否存在随机访问数据类型？ - 在代数型系统中如何定义这样的事物？当然，它似乎是不可能定义它的归纳。
- 在像Idris这样的类型系统中，是否有可能创建一个支持O(1)随机访问的数据类型，并且知道它的长度，以便所有访问都是有效的？(Haskell有数组式矢量，但它们的具体实现对普通用户(包括我)来说是不透明的)
回答 2
Stack Overflow用户
发布于 2014-12-24 11:15:41
它并不能优化向量查找(至少在撰写此答案时如此)。
这并不是因为做这件事有任何困难，而是因为我更希望有某种通用的框架来编写这种优化，而不是硬编码大量的优化。诚然，我们已经对Nat进行了硬编码优化，但我仍然不希望以临时的方式添加更多的负载。
取决于您实际想要的是什么，实验唯一性类型系统可能会有所帮助，因为您可以在引擎盖下有一个低级别的可变的东西，并且仍然可以在高级语言中以纯风格访问和更新。我们再看看..。
Stack Overflow用户
发布于 2015-01-01 11:09:25
然而，如果您正在寻找一些在某些情况下可以优化为常数时间查找的内容，那么下面的步骤可能是正确的。
对于编译时固定大小的向量(例如，不是在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是无关的。
https://stackoverflow.com/questions/27551529
复制相似问题
腾讯云开发者
