Re:Linear types can change the world (1990) [pdf]
by mcaruso on Wednesday January 10, 2018 @08:44AM
(#16114825)
In your f2 example, could you ever use/inspect the preProof argument? If the proof calculation is erased, I assume preProof could never be used in any way. Although depending on what the type PRE really is it might not be something you could do anything useful with in the first place.
I should probably learn Idris already, that would probably clear up these questions. :)
Re:Linear types can change the world (1990) [pdf]
by chriswarbo on Wednesday January 10, 2018 @12:37PM
(#16116999)
> In your f2 example, could you ever use/inspect the preProof argument?
Yes you could, but if your return value relies on details of the proof (e.g. branching on different cases) then it may no longer be erasable. Unless those parts of the return value can also be erased... it gets tricky :)
You're right to mention Idris, since it treats proofs in this way. In languages like ATS, there is a clear separation between erasable "proof-like" things and runtime "value-like" things, which makes things more predictable, but can lead to duplication.
For example, if a function claims to return a value of type T, and we can prove that the function halts, then we know that a value of type T must exist (it's whatever the function will return, however long that takes).
This is how dependently typed languages can implement pre and post conditions: we can represent conditions as types, and put preconditions as extra argument types, and postconditions as extra return values (e.g. in a tuple).
For example, we might have a function 'f1' which turns 'A' values into 'B' values:
If we require some precondition 'PRE' to hold for the argument, and postcondition 'POST' to hold for the return value, we can use dependent types to represent them: We can 'f1' by just giving it an 'A' argument, but the precondition won't be checked. Likewise, we learn nothing about whether the output satisfies the postcondition.With 'f2', we must give it an extra argument, representing a proof that the precondition holds for the given 'A' value. The function must also do more work: not only must it return a 'B' value, but it must also give us a proof that that 'B' value satisfies the postcondition (we can pass that proof around, e.g. if another function requires it as a precondition).
If we can prove that these calculations will halt, then we don't actually need to run them at all! Knowing that 'PRE a' can be proved in a finite amount of time (however long) is itself a proof of 'PRE a'! (And likewise for 'POST b'). Hence we can "erase" this proof stuff after type checking, to generate code equivalent to 'f1'.
If we don't know whether or not those proof calculations will halt, we can't use this shortcut, and we're forced to run the proof calculations in full at runtime (which may not halt, or might take a trillion years!).