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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime