4 ms·
The solution is to just accept that types might change during runtime. Give up the assumption that types are fixed at compilation and that the compiler can catc
by ErotemeObelus 7y ago
The solution is to just accept that types might change during runtime. Give up the assumption that types are fixed at compilation and that the compiler can catch all errors.
Computer programs exist inseparably from the operating system. The type of a circle might change to that of an ellipse. The size of a file can only be known at runtime. The only way the compiler can catch all errors is if no object is mutable and everything except for closed variables is allocated on the stack. And both of those preconditions are insane.
This is still superior to dynamic typed languages because it tells you exactly what the type problem is and where.
- rq1 7y agoThat’s not true. Even if you don’t know the size (n) of something at compile. You can always make sure in one of branches of your program that some other number m is equal to n even if they’re unknown. This the compiler can tell. For instance to produce an element x of type Fin n from an integer (n known at runtime), the compiler can make sure that you produced a proof that x < n. Usually the cast operation looks like this: Integer -> Maybe (Fin n). There is then only two possible branches in your program at this point and the compiler enforces it. (Just (Fin n) case and Nothing case).