为什么没有设计完全编译检查的语言？

Question

原谅设计非常糟糕的伪代码,但我希望它能解决这个问题:

float sqrt takes float n : [0,inf)
    // fancy algorithm
    return result

void main
    x = sqrt -1             // Compilation error
    y = sqrt float.max      // This works
    z = (y + 1) * (y + 1)   // Compilation error (this would result in overflow)

在编译期间,编译器会分析sqrt函数并将其表征为

sqrt : [0,float.max] -> [0, sqrt float.max[

它通过对+, -, *, /运算符执行相同的操作来实现此目的.

---

在main函数中,第一个语句不能编译,因为sqrt不接受负输入.第三个语句不编译,因为*运算符只接受会导致输出的输入[float.min, float.max].

Answer 1

您正在寻找的是COQ,Agda和Idris等语言,类型系统允许通过值对类型进行参数化.(依赖类型)

这并不像您想象的那么容易,并且通常需要完整的证明(在呼叫方面)满足条件.在你的情况下,你必须证明sqrt的参数不能是负数.在这种情况下,这很简单

sqrt(5)

但在以下情况下不是那么容易:

sqrt(some_long_computation_on_floats(f))

你需要在这里证明some_long_computation_on_floats只返回正数.哪种可能或不可能.