文章/答案/技术大牛

发布

问Idris向量与链表
EN

Stack Overflow用户

提问于 2014-12-18 16:42:00

回答 2查看 1.4K关注 0票数 21

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有数组式矢量，但它们的具体实现对普通用户(包括我)来说是不透明的)

回答已采纳

发布于 2014-12-24 11:15:41

它并不能优化向量查找(至少在撰写此答案时如此)。

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

取决于您实际想要的是什么，实验唯一性类型系统可能会有所帮助，因为您可以在引擎盖下有一个低级别的可变的东西，并且仍然可以在高级语言中以纯风格访问和更新。我们再看看..。

票数 16

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/27551529

复制

相似问题

问Idris向量与链表EN