TypeFamilies vs. FunctionalDependencies & type-level recursion

[Anthony Clayden]

> 
> Sorry for the late reply.
Thanks Oleg, I take it the Northern hemisphere is now on
academic summer holidays.
> 
> [snip]
> 
> > Finally, I still think most of the "magic" in everything
> > we've been talking about boils down to being able to
> > have a type variable that can take on any type *except*
> > a certain handful.  This would allow us to avoid
> > overlapping instances of both classes and type families,
> would allow us to define TypeEq, etc.  Moreover, it would
> > be a more direct expression of what programmers intend,
> > and so make code easier to read.  Such a constraint
> cannot be part of the context, because
> 
> Alas, such `type variables' with inequality constraints
> are quite complex, and the consequences of their
> introduction are murky. Let me illustrate. First of all,
> the constraint /~ (to be used as t1 /~ Int) doesn't help
> to define TypeEq, etc. because constraints are not used
> when selecting an instance. ...

Yes indeed we can't use constraints when selecting an
instance, 
several posters have pointed this out.
I've suggested we call these inequality 'restraints' rather
than 'constraints'.
And a different syntax has been proposed, similar to pattern
guards:
      type instance TypeEq a b   | a /~ b   = HTrue

> Instances are selected only by
> matching a type to the instance head. Instance selection
> based on constraints is quite a change in the type checker
> , and is unlikely to be implemented.

I agree that selecting instances based on constraints would
be abig change, but ...

Selecting instances based on inequalities is already
implemented in GHC and Hugs.
(And has been successfully used for over a decade.) You've
used it extensively yourself in the HList work, and much
other type-level manipulation (such as IsFunction).

Unfortunately, it's not called 'instance selection based on
inequalities' (or some such), and its implementation got all
mixed up with Functional Dependencies, which to my mind is
an orthogonal part of the design.

Instance selection based on inequalities is called
'Overlapping Instances'.
The difficulty in adopting it into Haskell prime is that it
isn't thoroughly specified,
and you can currently only use it with FunDeps.

To avoid confusion with FunDeps, let's imagine we could use
overlapping instances
 with Type Families:
       type family HMember e l
       type instance HMember a HNil         = HFalse
       type instance HMember a (HCons a l') = HTrue
       type instance HMember a (HCons b l') = HMember a l'
Selecting that last instance implies a /~ b.
(Otherwise the HTrue instance would be selected).
Using inequality restraints, we'd write that last instance
as:
       type instance HMember a (HCons b l') | a /~ b =
HMember a l'

And by putting an explicit inequality we are in fact
avoiding the trouble with
overlaps and all their implicit logic:
  The compiler can check that although the instance heads do
overlap,
     the inequality disambiguates the instances.
  So type inference could only select one instance at most.

I think this could be implemented under the new OutsideIn(X)
type inference:
   Inference for the ordinary instances proceeds as usual.
   Inequalities give rise to implication terms(as used for
GADTs),
      with the inequality in the antecedent:
       (a /~ b) implies (TypeEq a b ~ HFalse) 
   As with GADTs, inference needs evidence that a /~ b
before applying the consequent.
   There is no danger of clashing with other instances of
TypeEq,
      because the instance (including inequality) doesn't
overlap any of them.

(I made some long posts to the Haskell-prime list last
month, explaining in more detail, and responding to your
TTypeable suggestion.)


> 
> _______________________________________________
> Haskell-prime mailing list
> Haskell-prime at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-prime