4 ms·
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. Alth
by mcaruso 9y ago
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. :)
- chriswarbo 9y ago> 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.