关于动态类型语言与静态类型语言的争论很多。然而，在我看来，虽然静态类型语言使编译器（或解释器）能够更多地了解您的意图，但它们只是触及了可以传达的内容的表面。实际上，某些语言具有正交机制，可以在注释中提供更多信息。
我知道像 Agda 和 Coq 这样的强类型语言对它们允许你做什么非常挑剔。我对那些不是很感兴趣。相反，我想知道存在哪些语言或理论可以扩展您可以向编译器解释您想要什么的丰富性。例如，如果您有一个可变向量并将其转换为单位向量，为什么您的编译器不能选择向量投影的单位向量形式而不是计算量更大的通用形式？类型没有改变——构建所有必需类型所需的工作即使在像 Haskell 这样的打字非常容易的语言中也会令人反感——但似乎编译器可以知道很多关于情况。
某些语言是否已经在标准类型理论之外或在其更高级的分支之一中实现了这样的功能？