Haskell-prime

Download

haskell-prime@haskell.org

October 2011

1 participants
2 discussions

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
by Anthony Clayden 11 Jun '12

11 Jun '12

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

7 22

left and right sections extended
by Christian Maeder 01 Oct '11

01 Oct '11

Hi, the following sections are currently legal in Haskell: (a + b +) and (++ a ++ b) because + is left and ++ is right associative. I would like to write (+ 1 +) and (++ " " ++) as legal generalized sections, too, to stay for (\ a -> (a + 1 +)) and (\ a b -> a ++ " " ++ b) respectively. The right-associative case would be "flip (\ b -> (++ " " ++ b))" Such an extension would be easy to implement and it would also be a generalization of putting parenthesis around symbols as in (+) or (++). Extending the grammar is easy: aexp -> ... | ( infixexp qop ) (left section) | ( qop⟨-⟩ infixexp ) (right section) Some thoughts are needed to exclude the illegal cases (as done for left and right sections). Is this worth a formal proposal or is this too confusing? Cheers Christian

2 1