Simon Peyton-Jones
[from 29 Jul 2011]
So, let me ask: does anyone (eg Oleg) have concrete proposals on the table for things they'd like GHC to do?
Arising from the thread, two particular things jump out at me. ...
The two things are, I think, trying to achieve the same objective. Namely, supporting type-level inference driven from a type-level equality predicate. Of those two things (details continued below), I understand Oleg does have a concrete proposal for the first (and a prototype). My proposal earlier in the thread was along the lines of your second particular thing. But I delayed replying immediately: - Oleg suggested I refer back to several similar threads in July 2010 (thank you, that was indeed a valuable discussion) - GHC has now delivered robust type inference with type equality constraints, - and superclass constraints. - And we have the beginnings of data Kinds - And there has been 'loose talk' of closed Kinds (To explain that last: I believe the type inference for closed Kinds will need a similar mechanism to overlapping instances for TypeFamilies.) Although this thread is titled FunctionalDependencies, I'm not going to say anything about them except that they interfere badly with overlaps, so both have got an unfair reputation IMHO. Thanks to the improvements in type inference, SPJ has shown a technique he called "a functional-dependency-like mechanism (but using equalities) for the result type". That applies for Type Class instances, and GHC supports overlapping for those, so I've used the technique to simulate overlapping TypeFamily instances.
1. Support for type representations. Oleg showed this:
| I have implemented type-level TYPEREP ...
2. Support for overlapping type function equations.
There seems no reason in principle to disallow type instance F where F Int = Bool F a = [a] There is overlap, but it is resolved top-to-bottom. The only real
into FC. The only decent way seems to me to be to allow FC axioms to do
rendering might be ax32 a = case a of Int -> F Int ~ Bool _ -> F a ~ [a] That is, the axioms become type-indexed. I don't know what complications
difficulty with this is how to render it pattern matching themselves. So the FC that would add.
I favour support for overlapping type function equations, but not exactly that approach. I think a major complication from the programmer's point of view is that the type function equations would have to be declared all in the same place. (I suspect there would be a similar restriction with closed Kinds.) A complication for type inference is carrying around some representation of that case statement, and applying the top-to-bottom inference. I think it preferable from a programmer's point of view to have separately declared stand-alone instances. And I guess this might be easier to manage for type inference. And I propose a form for the instances that achieves the type function above, but with what you might call "explicitly non-overlapping overlaps", like this: type instance F Int = Bool type instance F a | a /~ Int = [a] -- explicit dis-equality restraint These can't overlap, because the restraint (aka type-level guard) says "you must have evidence that typevar a is not Int before this binding applies". And we can validate those instances for non-overlap: the instance heads overlap just in case a ~ Int. (I suspect much of this logic is already in place to handle overlapping instances. In a 2010 post Oleg gave a very convincing characterisation.) [Something very similar to dis-equality guards was briefly shown in Sulzmann & Stuckey. A Theory of Overloading (2002).] I'm calling these "restraints" because they're not like constraints. Restraints block instance matching, whereas constraints validate the instance _after_ matching. But the terminology is going to get confusing, because inside type inference, I think they'd be implemented as what's called "implication constraints" (as used for GADT's). That second binding gives rise to an axiom: (a /~ Int ==> F a ~ [a]) -- using ==> for implication (The axiom for the first binding is as usual, no implication needed.) I dislike Oleg's TypeRep approach, because it brings in another layer of encoding. I think it would be simpler from a programmer's point of view to have types 'standing for themselves'. I prefer "explicitly non-overlapping overlaps" because the type function guards look and behave similarly to guards for function bindings. (But a significant difference is that type function instances must be mutually exclusive, and that's how come they can be declared stand-alone. The requirement to be mutually exclusive means we avoid all that trouble with IncoherentInstances and imported overlaps silently changing behaviour -- I would explain further, but this post has gone on long enough.) AntC