futhark
futhark copied to clipboard
diku-dk
Refinement typing
@catvayor I'm going to work on this same branch for the checking pass; it shouldn't conflict with your work (but if there's an issue do let me know).
I have a suggestion for Futhark.Internalise.Refinement: instead of adding #[unsafe] to the things it can prove, reject the program if it cannot prove everything safe (possibly involving migrating checks to be function preconditions).
I've done some hacking to allow the SoP system to convert from arbitrary representations into SoPs, but it still needs work. One of the things I'm not sure about with the current SoP system is that there is significant conversion back-and-forth between the original representation and SoP representation of an expression. For example, here on lines 29 and 30:
https://github.com/diku-dk/futhark/blob/088201e35ebcf747ff00e929b7d62a8d79ea9bed/src/Futhark/SoP/RefineEquivs.hs#L24-L39
In the above this is done to substitute in known equivalences into the new equations (pes) that will refine the environment; this can simplify (or even enable outright) conversion of the new equations into SoPs (e.g., if the equation is x/y and you have y -> 1 in the environment (where 1 is a SoP)).
But there's merit to keeping everything in SoP land (at least in terms of simplicity) and substituting in and constructing source terms will be a pain and jank. And of course the analysis could inspect the environment for hints about y in the above example without actually converting the whole expression back.
Why?
Because our goal for now is to figure out when and how verification fails, which is easier when it does not happen silently.
Long term, it is my impression that this entire mechanism is about optionally asking it to verify the dynamic safety of a program, after which the compilation can occur without inserting any safety checks at all. Again, it's not a hidden optimisation: it's something the user explicitly asks for, and a failure to verify should be noisy.
I also strongly recommend keeping things in SoP form as much as possible. Constructing source language expressions is a sign you're on the wrong track.