News for hackers. Stuff that matters.

A comment on Linear types can change the world (1990) [pdf]. Parent comment

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. :)

[ Parent | on HN ]
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.

[ Parent | on HN ]