6 ms·

Err... the problem with this is that the size of a list/array is sometimes determined at runtime. This means that if you use dependent types, you can't determin

Err... the problem with this is that the size of a list/array is sometimes determined at runtime. This means that if you use dependent types, you can't determine whether a program is correctly typed until you run the code.

rq1 7y ago
Not at all. The verification is symbolic.
- ErotemeObelus 7y ago
  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.
  - aeneasmackenzie 7y ago
    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 >)
- 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 ago
    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).

rq1 7y ago

Not at all. The verification is symbolic.

ErotemeObelus 7y ago
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.
- aeneasmackenzie 7y ago
  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 >)
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 ago
  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).