TypeFamilies vs. FunctionalDependencies & type-level recursion
AntC
anthony_clayden at clear.net.nz
Wed May 23 12:55:31 CEST 2012
Simon Peyton-Jones <simonpj at ...> writes:
> [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
difficulty with this is how to render it
> into FC. The only decent way seems to me to be to allow FC axioms to do
pattern matching themselves. So the FC
> 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
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
More information about the Haskell-prime
mailing list