Hacker News Reader

Comment by rq1 | Hacker News Reader

Not at all. The verification is symbolic.

Let's say we're creating an array of strings separated by newlines obtained from reading a file. Call this arr[n] where n is determined at runtime.

Now let's have String index(arr:int[], i:(Fin(arr):int)), where FinInt(arr) is a dependent type that is an integer between zero and the length of the array. As the code is compiling, we have this

int i = 24951; String str = index(f, i);

The file exists in the future after the compilation. If the future file has at least 24951+1 lines, then the compiler can verify that i < n and that i is correctly typed. But if the file is short, then the type of i is incorrect. So at compile-type the type of i is indeterminate.

you get a compile time error saying f isn't known to have enough entries, and you resolve it by adding a decidable check that produces a proof that it does. (the check at runtime is just >)

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.

That’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).

Reply on news.ycombinator.com