Refinement typing

[catvayor]

No description provided.

[zfnmxt]

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

[athas]

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

[zfnmxt]

@athas Why?

[zfnmxt]

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:

futhark/src/Futhark/SoP/RefineEquivs.hs

Lines 24 to 39 in 088201e

	-- | Refine the environment with a set of 'PrimExp's with the assertion that @pe = 0@
	-- for each 'PrimExp' in the set.
	addEqZeroPEs :: forall u e m. (ToSoP u e, FromSoP u e, MonadSoP u e m) => Set (e == 0) -> m (Set (SoP u >= 0))
	addEqZeroPEs pes = do
	-- Substitute already known equivalences in the equality set.
	equivs_pes <- (fmap . fmap) (fromSoP :: SoP u -> e) getEquivs
	let pes' = S.map (substitute equivs_pes) pes
	-- Make equivalence candidates along with any extra constraints.
	(extra_inEqZs :: Set (SoP u >= 0), equiv_cands) <-
	mconcat <$> mapM addEquiv2CandSet (S.toList pes')
	-- Add one-by-one all legal equivalences to the algebraic
	-- environment, i.e., range and equivalence envs are updated
	-- as long as the new substitutions do not introduce cycles.
	addLegalCands equiv_cands
	-- Return the newly generated constraints.
	pure extra_inEqZs

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.

[athas]

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.

[athas]

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.