Idris矢量与链接列表

Question

Idris在矢量引擎下做了什么样的优化吗？因为从它的外观来看,Idris向量只是一个已知大小的链表(在编译时已知).事实上,一般来说,你似乎可以表达以下等价(我在语法上有点猜测):

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

因此,虽然这在防止范围误差方面很好,但是矢量的真正优势(在该术语的传统用法中)是在性能方面; 特别是O(1)随机访问.似乎idris向量不支持这个(你如何编写索引函数来获得这种性能？).

• 假设Nat在重新配置Vectors 之下没有任何巫术(如果发生的那样),Idris中是否存在随机访问数据类型？
• 如何在代数类型系统中定义这样的东西？当然,似乎不可能以归纳的方式定义它.
• 在像Idris这样的类型系统中,是否有可能创建一个支持O(1)随机访问的数据类型,并且知道它的长度使得所有访问都可证明是有效的？(Haskell有数组样式的向量,但它们的具体实现对普通用户来说是不透明的,包括我)

Answer 1

它没有做任何事情来优化Vector查找(至少在写这个答案的时候).

这并不是因为这样做有任何困难,实际上,更多是因为我宁愿有一些用于编写这种优化的通用框架,而不是硬编码它们.不可否认,我们已经对硬编码进行了优化Nat,但我仍然不希望以临时方式添加更多负载.

根据您的实际需要,可能是实验性的唯一性类型系统将有所帮助,因为您可以在引擎盖下有一个低级可变的东西,并且仍然可以在高级中以纯粹的方式进行安全有效的访问和更新等级语言.走着瞧...