3 ms·
It is done statically. Types are a compile time construct, languages like Agda and Coq have no type information at runtime. This means if one can't statically p
by jroesch 13y ago
It is done statically. Types are a compile time construct, languages like Agda and Coq have no type information at runtime. This means if one can't statically prove that their types are correct the code won't compile.
For example if my function returns a Vector[A, N] (a vector of A's with size N), and I try to pass it's return value to a function that expects a of type Vector[A, 2] my code will not compile. This is because there is no way one can prove forall A N. Vector[A, N] satisfies Vector[A, 2].
- tel 13y agoNot all things are statically checkable. If you want to take in some runtime data and treat it as a Vector[A, 3] then you'll need to include a dynamically failing check like (List -> Maybe (Vector n a)).
- ajanuary 13y agoI don't know Agda or Coq but I assume all it would take is to test the size and throw a runtime error for it to statically assert that it is the correct size after the test. Now the compiler is helping you write the runtime preconditions checks and handling that you should be writing anyway.
- tel 13y agoYeah, that's exactly how dynamic data can enter a statically typed regime of code. Dependent types make it so that it's impossible to bring dynamic data into type-controlled parts of your code without first performing and passing those tests. Which seems weak since smart developers should do that anyway, but (a) there's still some divide between "should" and "it's impossible" and (b) this is just the tip of the iceberg about what dependent types offer anyway.