Closed type families have precedence and it is very useful for overlapping instances. It would be really useful to have precedence in open type families.
I am sure there is a reason this is not supported, do you know why?
For one thing, how would you specify the order syntactically, when different instances can be in different compilation units?
We already have a modular precedence system for infix operators. So we could mirror that: have a fixed number of type family instance precedence levels and specify for each instance which precedence level it has.
The tricky thing is type soundness, which is imperiled if you allow some type family application F X to reduce to S in one context and T in a different context, because then you can prove S ~ F X ~ T and hence write unsafeCoerce. Closed type families avoid this by ensuring that a later equation fires only if none of the earlier equations apply (or if they do apply, that the results are consistent).
Well, you can prove S ~ F X in one context and F X ~ T in the other, but I think if you add appropriate checks then I think you can make it so that you can never combine these contexts and get S ~ T out of it.
This reminds me of world semantics for type classes (see Section 4.4 of Scott Kilpatrick’s Non-Reformist Reform for Haskell Modularity).
Edit: Actually, @adamgundry can you give an example? I’ve tried this:
module A where
type family F a
module B where
import A
type instance F Bool = Int
module C where
import A
type instance F Bool = ()
And that seems to work properly with a check at import-time:
ghci> import B
ghci> import C
<interactive>:1:1: error: [GHC-34447]
Conflicting family instance declarations:
A.F GHC.Types.Bool = GHC.Types.Int -- Defined in module B
A.F GHC.Types.Bool = () -- Defined in module C
This seems tricky to establish, given that the soundness argument for System FC isn’t aware of such things as module boundaries. Moreover, if a module knows that S ~ F X, pretty much any definition it exposes might depend on that fact, and hence be unsafe to compose with definitions from the other module.
My point was that GHC rejects such examples (both on-the-nose conflict as you demonstrate, but also inconsistent overlapping type family instances), because to accept them would be unsound.
2 Likes
Indeed. What it needs is a way to say: this instance applies except when …; and to express the exception(s) in some sort of a notation that the compiler can examine; so it can check all instances in imports are apart from instances in this module. IOW not merely a precedence system
Instance Apartness Guards, which specifically addresses how to handle separate compilation units.
I’ve dummied-up an implementation. It works for me and means instance logic/esp FunDeps is easier to follow IMO
class {-# INSTANCEGUARDS #-} Add a b r | a b -> r, r a -> b, r b -> a
instance Add Zero b b
instance (Add a b r) => Add (Succ a) b (Succ r) | b /~ (Succ r)
1 Like
FWIW the Lean 4 manual has a section on default instances and instance priorities, so there is certainly prior art. Whether Haskell’s type class system can support this is another story.
1 Like
Prior art for a strict language - it may be easier to reimplement default and prioritised instances in another strict or total language rather than Haskell. (Of course, there’s another option: bring laziness to the likes of Lean, Idris, and Agda - any expression not used by dependent types can still be lazy! :-)