为什么依赖类型语言通常不是图灵完备的？

Question

例如 Agda 和 Coq。

与 Idris2 和 Fstar 相比。

此外，诸如 Agda 之类的依赖类型编程语言不是图灵完备的，是否存在实际缺点，或者主要是在理论上，即，不知道是否会影响编程的可用性。

Answer 1

您所读到的内容是错误信息。

例如，您可以在

IO.Base

中看到 Agda 标准库附带了一个 称为

forever

的组合器愉快地执行

IO

操作，直到 时代的终结（或者更可能的是，

IO

行动最终决定 拨打

exitSuccess

或

exitFailure

):

forever : IO {a} ⊤ → IO {a} ⊤

当然你不会找到一个函数

fix : (A → A) → A

但那是 因为类型必须诚实地对待不终止的可能性 （就像 Haskell 中的类型必须诚实地对待以下可能性） 突变，或输入输出，或失败）。为了封装这样的效果你 通常使用 monad。