Haskell allows what I will call coincident overlap among type family instances. Coincident overlap occurs when two (or more) type family instances might be applicable to a given type family usage site, but they would evaluate to the same right-hand side. This post, inspired by Andy Adams-Moran’s comment to an earlier blog post, explores coincident overlap and how to extend it (or not!) to branched instances.
This post is a literate Haskell file (though there really isn’t that much code). Paste it into a .lhs file and load it into GHCi. Because the post uses branched instances, you will need the HEAD version of GHC. (Branched instances will be included in GHC 7.8, but not before.)
> {-# LANGUAGE TypeFamilies, DataKinds, GADTs, TypeOperators #-}
Our examples will be over Bools, and we need some way to get GHC to evaluate our type families. The easiest way is to use the following singleton GADT:
> data SBool :: Bool -> * where
> SFalse :: SBool False
> STrue :: SBool True
Conflict checking with type family instances
When compiling type family instances, GHC checks the instances for conflicts. To know if two instances conflict (i.e., could both match the same usage site), GHC unifies the two left-hand sides. For example, the following code is bad and is rejected:
type family F x
type instance F Int = Bool
type instance F a = DoubleCompiling the above instances gives the following error message:
Conflicting family instance declarations:
F Int -- Defined at ...
F a -- Defined at ...This check is a good thing, because otherwise it would be possible to equate two incompatible types, such as Int and Bool.
Coincident overlap among unbranched instances
Here is a nice example of how coincident overlap is useful:
> type family (x :: Bool) && (y :: Bool) :: Bool
> type instance False && a = False -- 1
> type instance True && b = b -- 2
> type instance c && False = False -- 3
> type instance d && True = d -- 4
Although the first two equations fully define the && operation, the last two instances allow GHC to reduce a use of && that could not otherwise be reducible. For example:
> and1 :: SBool a -> SBool (True && a)
> and1 x = x
>
> and2 :: SBool a -> SBool (a && True)
> and2 x = x
and1 uses the second instance of &&, but and2 requires the fourth instance. If we comment that instance out, and2 fails to compile, because GHC cannot figure out that a && True must be a for all values of a. For various good reasons, perhaps to be explored in another post, GHC does not do case analysis on types during type inference.
How does GHC know that overlap is coincident? During the conflict check, GHC looks for a substitution that unifies two potentially-conflicting instances. In our case, the fourth and first instances would conflict under the substitution {a |-> True, d |-> False}. However, after finding the unifying substitution, GHC checks the right-hand sides under that same substitution. If they are the same, then GHC considers the overlap to be coincident and allows the instance pair. In our case, applies the substitution {a |-> True, d |-> False} to False and d and discovers that both are False, and so the instances are allowed.
Coincident overlap within branched instances
When thinking about branched instances and coincident overlap, there are two possibilities to consider: coincident overlap within a branched instance and coincident overlap among two separate branched instances. Let’s consider the first case here.
Imagine we define || analogously to &&, but using one branched instance:
> type family (x :: Bool) || (y :: Bool) :: Bool
> type instance where
> False || a = a -- 1
> True || b = True -- 2
> c || False = c -- 3
> d || True = True -- 4
Now, let’s consider simplifying the type e || False. The first two branches don’t match, but the third does. Now, following the rule for branched instance simplification (as stated in the Haskell wiki), we check to see if any previous branches might be applicable to e || False, for any possible instantiation of e. The first branch certainly might apply, and so e || False fails to simplify. This is surely counterintuitive, because the third branch matches e || False exactly!
Just to prove this behavior, I tried running this code through GHC:
bar :: SBool a -> SBool (a || False)
bar x = xHere is the error:
Couldn't match type ‛a’ with ‛a || 'False’At first blush, it seems I’ve missed something important here in the implementation — allowing coincident overlap within a branched instance. But, there is a major problem with such overlap in this setting. Let’s think about how coincident overlap would work in this setting. After selecting the third branch to simplify e || False (with the substitution {c |-> e}), GHC checks to see if any previous branch could be applicable to e || False. The first branch, False || a, unifies with e || False, so it might be applicable later on. The unifying substitution is {a |-> False, e |-> False}. Now, if we wanted to check for coincident overlap, we would apply both substitutions ({c |-> e} and {a |-> False, e |-> False}) to the right-hand sides. In this case, we would see that both right-hand sides would become False, and it seems we should allow the simplification of e || False to e.
Let’s try a harder case. What if we want to simplify (G f) || False, for some type family G? The third branch matches, with the substitution {c |-> G f}. Now, we check earlier branches for applicability. The first branch is potentially applicable, if G f simplifies to False. But, we can’t produce a substitution over type variables to witness to check right-hand sides. In this case, it wouldn’t be hard to imagine a substitution like {(G f) |-> False}, but that’s a slippery slope to slide down. What if f appears multiple times in the type, perhaps under different type family applications? How do we deal with this? There may well be an answer, but it would be subtle and likely quite fragile from the programmer’s point of view. So, we decided to ignore the possibility of coincident overlap within a branch. We were unable to come up with a compelling example of why anyone would want this feature, it seemed hard to get right, and we can just write || using separate instances, anyway.
Coincident overlap between branched instances
Consider the following (contrived) example:
type family F (x :: Bool) (y :: Bool) :: *
type instance where
F False True = Int
F a a = Int
F b c = Bool
type instance F d True = IntIs this set of instances allowable? Is that your final answer?
I believe that this set of instances wouldn’t produce any conflicts. Anything that matches F d True would have to match one of the first two branches of the branched instance, meaning that the right-hand sides coincide. However, it is difficult to reason about such cases, for human and GHC alike. So, for the sake of simplicity, we also forbid coincident overlap whenever even one instance is branched. This means that
type instance F Int = Booland
type instance where F Int = Boolare very subtly different.
Andy Adams-Moran’s example
This post was partially inspired by Andy Adams-Moran’s comment in which Andy poses this example, paraphrased slightly:
> data T a
> type family Equiv x y :: Bool
> type instance where
> Equiv a a = True -- 1
> Equiv (T b) (T c) = True -- 2
> Equiv (t d) (t e) = Equiv d e -- 3
> Equiv f g = False -- 4
Alas, this does not work as well as one would like. The problem is that we cannot simplify, say, Equiv (T a) (T b) to True, because this matches the second branch but might later match the first branch. Simplifying this use would require coincident overlap checking within branched instances. We could move the first branch to the third position, and that would help, but not solve the problem. With that change, Equiv x x would not simplify, until the head of x were known.
So, is this the “compelling example” we were looking for? Perhaps. Andy, why do you want this? Can your use case be achieved with other means? Do you (anyone out there) have a suggestion for how to deal with coincident overlap within branched instances in a simple, easy-to-explain manner?
Types and Kinds 
I don’t understand this remark: “This check is a good thing, because otherwise it would be possible to equate two incompatible types, such as Int and Bool.”. Care to elaborate?
Say we were allowed instances as follows:
type instance F Int = Int
type instance F a = Bool
Now, suppose we have these declarations:
foo :: a -> F a
foo _ = True
bad = foo (3 :: Int)
The declaration of `foo` should type-check: after all, we know that `F a` is just `Bool` from the type family instance for `F a`. We know that the call of `foo` on the last line should type-check, with `a` set to `Int`. But, what is the type of `bad`? The return type of `foo` is `F a`, but `a` was instantiated to `Int`, so `bad` should have type `F Int`… which is really just `Int`. Thus, `bad` will have the value `True` but the type `Int`. This is bad indeed.
I hope this clarifies it!
Well, foo doesn’t necessarily have to type check. I’m drawing a parallel to Scala’s type projections and implicit parameters where it wouldn’t compile (well, it would compile if you restrict the “result type” of F to be subtype of Bool which would then produce a compile error when defining F Int = Int). But maybe type families in Haskell are based on a different philosophy.
When the type family enhancement first appeared, overlapping instances were required to be ‘confluent’. This ‘Coincident Overlap’ seems to be subtly different. I thought the purpose of the NewAxioms/branched instance stuff was to support overlapping instances being non-confluent (“disfluent” anybody?).
On first reading the example for ||, I thought: but those instances are all confluent, why would you bother using branching? Then I got to the two examples (apparently the same but one branched, one not) that are “very subtly different”, and the example just before of a 3-instance branch vs a stand-alone instance that overlaps.
I appreciate that the discussion is down to pretty obscure corner cases; and I can’t see any real use for Andy A-A’s example; but I’m feeling queasy about the whole thing.
I was never convinced by the branching instances approach. I don’t see instance selection as sufficiently similar to case expressions; because in cases, the semantics are that evaluation can always tell whether one branch applies and if not move on to the next, so will always make progress. Instance selection can get ‘stuck’ even when there’s an instance that applies (but in a ‘blocked’ branch). (OK instance selection anyway can get stuck, and it sometimes needs whole-program analysis to see why.)
Instances (in general) are different to cases because instance declarations can be scattered all over the program (and other modules). I think of them all ‘competing to be chosen’ at compile time.
Does the following way of thinking help? (I’ll follow Andy A-A’s example):
To move on from one branch to try the next, there must be type evidence that that branch doesn’t match. That evidence is a type disequality, and we can add it as a guard on all subsequent branches (in the same group).
So after rejecting:
> Equiv a a
We must have: Equiv a’ a” | a’ /~ a”
Substitute that into the next branch:
> Equiv (T b) (T c) | (T b) /~ (T c) — reduces to b /~ c
And if that branch fails the next branch must have:
> Equiv (t d) (t e) | (t d) /~ (t e), ((t d), (t e)) /~ ((T _), (T _))
— reduces to d /~ e, t /~ T
Confluence checking amongst branches then amounts to this:
Compare the instance heads pair-wise as if they were separate instances.
If the heads overlap, form the mgu instance for the overlap.
Substitute that into the RHS of the instance; if the same result then the branches are confluent OK.
[Up to this point I believe is existing behaviour for checking stand-alone instances.]
If not confluent, substitute the mgu into the disequality guards.
If you get a contradiction (in one guard or the other), then it’s not ambiguous which branch will get chosen; no problem.
So I can still keep my mental image of each instance (branch) ‘competing to be chosen’.
I didn’t give the guards for the last branch, and that’s because they’re rather messy. (I’m not happy.)
> Equiv f g | f /~ g, (f, g) /~ ((T _), (T _)),
(f, g) /~ ((t _), (t _))
In particular, that typevar t is freshly introduced on the RHS of a disequality (not sourced from the instance head). So testing the disequality will need some sort of pattern binding mechanism. Yeuch!
Andy A-M’s example has been nagging at me. (Yes I know it’s been 3 years 😉
Here’s a better solution for that last Equiv f g branch. Split it into several branches, which are confluent/coincident:
> Equiv (t’ d) (t” e) | t’ /~ t” = False
> Equiv (t’ d) g | g /~ (_ _) = False
> Equiv f (t” e) | f /~ (_ _) = False
Note there’s no new tyvars introduced in the guards. All of the guards have a bare tyvar from the head on LHS of the disequality.
Here’s another solution, following those same rules:
> Equiv (t’ d) g | g /~ (t’ _). = False
> Equiv f (t” e) | f /~ (t” _) = False
> Equiv f g | f /~ (_ _), g /~ (_ _) = False
More important: how did I get there, and is there a general method? The idea being that we treat branched instances as some sort of sugar for stand-lone instances you could write for yourself — if we had disequality guards.
I prefer standalone instances because:
* I think it’s a cleaner mental model that fits with Class instances;
* I like the way associated type instances are amongst the type decls
and Class instances they apply for;
* if we’re going to get better rapprochement between type families and fundeps
— especially multiple multi-directional fundeps for the same class —
then type family instances have to be distributed;
* there’s a few corner cases of overlaps you can’t express with type funs.
Some of that reasoning went into the design for ORF. In particular that the pseudo-instances for the Has class are to be created on-the-fly. So are necessarily distributed. So can’t appear together as branched instances. Furthermore anonymous records are going to need overlapping instances in rather unpredictable ways. So no hope of some monster branched structure.
Thanks for your comment, AntC. I like your way of thinking about branches as standalone instances with disequality guards — that captures precisely what is going on. Since writing this post, I’ve been pondering different ways of attacking coincidence checking within groups (without needing to look at use sites, which might mention type families), and came up with something similar to what you mention. In particular, I also came up with the idea of figuring out, a priori, if there were branches that are surely coincident (like the first two in A. A-M.’s example) and then (essentially) relaxing the disequality guards. I hadn’t thought of the idea of substituting into the disequality guards, though — I’ll have to ponder that one more.
I should also point out that this coincident overlap has been in GHC for quite some time. However, a quick-ish search through the research papers on type families didn’t come up with any mention of coincident overlap. Instead, every paper says that there can be no overlap. Period. When I discussed how to deal with coincident overlap with branched instances with Simon PJ, he was quite surprised to learn about coincident overlap at all.
Thanks Richard. By the way, I’m not claiming any big innovation with disequality guards. They are for instance discussed in Sulzman & Stuckey ‘A Theory of Overloading’, under Constraint Handling Rules.
Yes, overlap has been in TF’s since the beginning. It is not correct to say that overlap is banned altogether. (And I’m sure there are or at least were examples on wiki pages and in some of the early TF papers.) I think you should search on ‘confluence’.
Here we go Type Family “overlap is permitted”: http://www.haskell.org/ghc/docs/latest/html/users_guide/type-families.html#type-family-overlap
The example is:
type instance F (a, Int) = [a]
type instance F (Int, b) = [b] — overlap permitted
And I’m pretty sure that example is from one of the research papers — I’d look at the ones back in 2005/2006. (Heck! did TF’s really arrive that long ago?!) [SPJ was co-author of all those papers, so he darn well ought to know about overlaps. Perhaps it’s the way you tell ’em?]
The instances exhibit what I’d call ‘partial’ overlap. That is, there are some substitutions that match both instances; some only one; some only t’other. From my experience of what people want to do with overlaps, that’s relatively unusual. More commonly there is a ‘wider’ and a ‘narrower’ instance; a substitution that matches the narrower necessarily matches the wider. In that case the disequality guards work rather smoother. (And in the branching structure, you have to put the narrower first.)
While I’m at it, a couple of apologies:
Andy’s surname is A-M, not A-A as I put.
Martin’s is Sulzmann (double ‘n’).
I’m interested in implementing inference/resolution for foreign type systems using ~ and type-level equality/equivalence, where foreign means Java, .NET, Objective-C, etc.
Consider Andrew Appleyard’s Salsa (www.haskell.org/haskellwiki/Salsa), a bridge and type system mapping between Haskell and .NET. Each .NET type is mapped into a Haskell label (and a bunch of associated instances), along with a unique encoding for that type as a type-level list of type-level hex digits. Method overloading resolution is some neat type-level recursion, which relies on distinguishing .NET types based on their encoding. (Pause for a moment to consider that Andrew did all this *without* type-level literals, promoted datatypes, or kind signatures.)
With a more direct type-level equality, this is much simpler. There are limits though. While it works beautifully for vanilla Java types, Java Generics (represented by labels with type parameters) end up requiring type signatures when used (sad panda). This is because the type-level equality only “fires” when both arguments are ground, and operations over Generics ought to be polymorphic.
A type-level /equivalence/ might allow one to get around this. I expect there are other approaches that don’t require anything beyond the type-level equality. Caveat: I haven’t tried applying the ideas mentioned in this post or by AntC.
BTW: this kind of machinery could be used to implement row types for type-safe databases, but that would also suffer from a lack of polymorphism. For example, we might be able to give join a beautifully polymorphic type, we’d just need to get very specific at every use (i.e., type signature hell).
Thanks Andy (A-M) I think you’re righ on both counts: row types for type-safe databases, … give join a beautifully polymorphic type. Here’s a proof of ‘capability’ (as in crude and non-scalable approach).
Make our rows Haskell tuples. Make them Type Indexed Products (I call them TIPles). Class Has1 will extract element type e from a row, providing that element appears uniquely.
> class Has1 e r where get1 :: r -> e — ‘pulls’ e from r
> instance Has1 e (a, b, c, d, e) where get1 (_, _, _, _, x) = x
Crucially this relies on overlapping instances to guarantee Type-Indexing. (If more than one type e appears in the tuple, we get compile fail.) It’s non-scalable because we need 5 instances declared for a 5-tuple. I’m assuming our elements are newtypes with (in Relational terms) an attribute name/label and underlying type (what Codd called domain):
> newtype CustomerId = CustomerId Int
Here’s a ‘beautiful’ join:
> instance (Eq e, r3 ~ (a, b, c, d, e, g, h)
> => Join (a, b, c, d, e) (e, g, h) where
> (x1, x2, x3, x4, x5) `join` (y1, y2, y3) | x5 == y1 = (x1, x2, x3, x4, x5, y2, y3)
Again crucuially relies on overlapping instances to guarantee uniqueness. Again non-scalable — we need well over 100 instances to cover a 5-tuple joining to a 3-tuple.
You’re right that it would also suffer from a lack of polymorphism. OTOH I’m not ever-so convinced that you need polymorphism for persistent databases. But certainly you can’t match (for example) a Maybe alpha to a Maybe beta and expect type inference to improve alpha and beta to the same type. (There’s possibly different stories w.r.t. existential types or parametric polymorphic rows — but it rapidly gets very non-beautiful.)
Rats! that ‘beautiful’ instance for Join is missing the third argument in the instance head, being r3 (result of the join).
“… type-level equality only “fires” when both arguments are ground, …”
There’s a similar consideration in the HList paper with their tests for type equality. But I wonder if that’s quite right. We’re not wanting equality exactly so much as provable unifiability.
For your `Equiv a a` branch, all we need is that the use site give us two skolem types (say g0017, g0026) such that we can show they’re unifiable, possibly by showing they’re each unifiable via some 3rd, 4th, etc variables in the environment. (Unifiability is commutative and transitive.)
But for inference to be able to reject the `Equiv a a` branch and plump for one of the others, it has to prove that if a’ ~ (T b) and a” ~ (T c) then b is not unifiable with c. Or if a’ ~ (t’ d) and a” ~ (t” e) then either t’ is not unifiable with t” or d is not unifiable with e (or neither). Or if either a’ or a” are non-atomic types, the other is atomic; or if both atomic, they are different.
So what’s sufficient evidence that two skolems are _not_ unifiable? I think: we have to ground both to unequal types. We might half-ground the first to (Maybe d) then we have to get the second to at least [e] before we can be sure.
Then I see how we get into type signature hell — which I’ve experienced myself.
Some of this discussion has made it into a proposal for a change to type family instances. The email introducing the change is at http://www.haskell.org/pipermail/glasgow-haskell-users/2013-May/023980.html
Hi Richard, thank you for the discussion on ghc-users. Back to the main part of this post on coincident overlap, I’ve been thinking about your comment “So, we decided to ignore the possibility of coincident overlap within a branch. We were unable to come up with a compelling example of why anyone would want this feature, it seemed hard to get right, and we can just write || using separate instances, anyway.”
One of the ‘features’ of overlapping (class) instances that we tend to take for granted is to select the most specific instance and reject the program if that is not unique (in the absence of IncoherentInstances).
Here’s a possible “compelling example”:
> class Has1 e r where get1 :: r -> e — ‘pull’ a unique e out of r
> instance Has1 e (a, b, e) where get1 (_, _, z) = z
> instance Has1 e (a, e, c) where get1 (_, y, _) = y
> instance Has1 a (e, b, c) where get1 (x, _, _) = g
> … get1 (True, “ambiguous”, False) :: Bool …
These instances overlap, so I can’t put them standalone. If I want to translate to ‘closed type families’, I suspect that the example usage would pick the first instance, rather than rejecting as ambiguous.
(There’s a similar risk with type-indexing HList’s. To guard against that, there’s a constraint (Lacks e l’) => … in which l’ is the tail of the HList beyond e. Getting Lacks to work needs some particularly ugly instance-trickery.)
I guess you’re going to say that we can put type inequality constraints on all of those instances.
In the evolution of thought that has occurred since my original post here, Simon PJ, Dimitrios V, and I (who am in the middle of an internship at Microsoft Research Cambridge), have agreed that coincident overlap within closed type families (the new nomenclature for branched instances) would indeed be useful. This is supported in the current implementation of closed type families. See http://hackage.haskell.org/trac/ghc/wiki/NewAxioms for a full accounting of what has been done.