【发布时间】：2013-03-04 11:30:17
【问题描述】：
关于动态类型语言与静态类型语言的争论很多。然而，在我看来，虽然静态类型语言使编译器（或解释器）能够更多地了解您的意图，但它们只是触及了可以传达的内容的表面。事实上，有些语言有一种正交机制，可以在注释中提供更多信息。
我知道像 Agda 和 Coq 这样的强类型语言对它们允许你做什么非常挑剔；我对那些不是很感兴趣。相反，我想知道存在哪些语言或理论可以扩展您可以向编译器解释您想要什么的丰富性。例如，如果你有一个 mutable 向量并将其转换为单位向量，为什么你的编译器不能选择向量投影的单位向量形式，而不是计算成本更高的通用形式？类型没有改变——构建所有必需类型所需的工作即使在像 Haskell 这样的打字非常容易的语言中也会令人反感——但似乎编译器可以知道很多关于情况。
某些语言是否已经在标准类型理论之外或在其更高级的分支之一中实现了这样的功能？
【问题讨论】：
-
为什么您对 Agda 和 Coq 不感兴趣，而您所要求的正是它们所提供的（尽管不太实用，但 Idris 的方向更实用）？不过，Haskell 的向量库已经提供了您对某些类型向量的巧妙表示的特定示例。您可能还对 LiquidHaskell 以及 Dana Xu 早期关于 GHC 合同的工作感兴趣。
-
@copumpkin - 也许我应该感兴趣，但是我所看到的所有示例都非常笨拙，因为它们的用处很大，而且我看不出如何将它们扩展到可变和对象 -面向上下文，这是推理变得更加棘手的地方，无论如何您都需要更多帮助。
-
@Rex 您是否正在寻找比依赖类型更具表现力的抽象？如果是这样，你能举个例子吗？否则，也许您实际上正在寻找一种以令人满意的方式实现它的语言。
-
考虑在cs.stackexchange.com问cs相关的问题。
标签： language-agnostic type-theory