3 ms·
Wait what? The whole point of dependetly-typed languages is that programs you write in them are fully typechecked at compile time.
by gergoerdi 10y ago
Wait what? The whole point of dependetly-typed languages is that programs you write in them are fully typechecked at compile time.
- asQuirreL 10y agoIn a dependently typed language, types may rely upon arbitrary terms that are computed at runtime, and yet you are correct that dependently typed programs are checked statically. The way this is achieved is if a property can only be checked at runtime, then the burden of proof for that property is moved from the typechecker to the program. The program must verify the property at runtime and create a witness to the proof, which it can then pass to functions to say that it has done the necessary work. So I guess the answer is yes and no. I would say the whole point of dependently-typed languages is that we can statically determine that somebody is maintaining correctness, be it at compile time or at run time.