| > Absolutely not; quite the reverse. It means that some of the *code* for | type functions happens to be in the 6.8 release --- but that code has bugs. | It's only in 6.8 for our convenience (to avoid too great a divergence between | the HEAD and 6.8), but we do not plan to *support* type functions in 6.8. | Doing that would delay 6.8 by 3 months. | | Do you make any difference between associated type synonyms and type | functions in this respect? No difference: both are in the 6.8 code base, but we won't support them there. Both are in the HEAD, and we will support them there. (Associated data types have the same status -- but the 6.8 code for associated data types is quite a bit solider, so they'll probably work. No promises though!) Simon

| What does this imply for 6.8 support for FD's, as they now use | the same type-coercions? Actually FDs do not use type coercions, in GHC at least. As Mark originally described them, FDs guide inference; and in particular, they give rise to some unifications that would not otherwise occur. In terms of the intermediate language, that means there is no "evidence" associated with a FD; it's just the type checker's business. That means that various potentially-useful things can't be expressed, notably when FDs are combined with existentials or GADTs, that involve *local* equalities, which were beyond the scope of Marks's original paper. As the recent thread about FDs shows, FDs are quite tricky, at least if one goes beyond the well-behaved definition that Mark originally gave. (And FDs are much more useful if you go beyond.) Our current plan is to regard FDs as syntactic sugar for indexed type families. We think this can be done -- see our IFL workshop paper http://research.microsoft.com/%7Esimonpj/papers/assoc-types No plans to remove them, however. After all, we do not have much practical experience with indexed type families yet, so it's too early to draw many judgements about type families vs FDs. I recommend Iavor's thesis incidentally, which has an interesting chapter about FDs, including some elegant (but I think unpublished) syntactic sugar that makes a FD look more like a function. I don't think it's online, but I'm sure he can rectify that. Simon

Wolfgang Yes, that’s interesting. As you know, you have to turn off overlap checks and allow non-terminating instances to make this HList stuff work. There's nothing to stop us doing the same for type functions, although we have not yet done so. (Too busy making the basic thing work.) For example, | In fact, after thinking and experimenting I came to the conclusion that it’s | probably just not possible to define a type function TypeEqTF t1 t2 which for | *all* types t1 and t2 yields True or False, depending on whether t1 and t2 | are equal or not. That's a nice crisp example. It's a pure function, at the level of types, so you'd think it should be definable. And I don't think there is any reason we couldn't do so (in due course). For example, overlap is fine, so long as when we *use* an equation there is only one that applies, so that there is a unique answer. Similarly I think we could reasonably allow type instance F t t = ... You are certainly right that type functions today don't do all that FDs (as implemented in GHC at least) do. It'd be quite useful to identify just what extra features are needed in the type-function world would be needed to do HList kind of stuff. (Oh, it's just possible that HList might be architected differently if type functions were available.) Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell- | users-bounces@haskell.org] On Behalf Of Wolfgang Jeltsch | Sent: 19 October 2007 09:51 | To: glasgow-haskell-users@haskell.org | Subject: Re: type families not advertised for 6.8 | | Am Freitag, 19. Oktober 2007 09:25 schrieb Simon Peyton-Jones: | > […] | | > Our current plan is to regard FDs as syntactic sugar for indexed type | > families. We think this can be done -- see our IFL workshop paper | > http://research.microsoft.com/%7Esimonpj/papers/assoc-types | | I doubt this can be done in all cases. Take the following code which is more | or less from HList: | | {-# LANGUAGE | MultiParamTypeClasses, | FunctionalDependencies, | FlexibleInstances, | OverlappingInstances, | UndecidableInstances, | TypeFamilies, | EmptyDataDecls | #-} | | data False | | data True | | class TypeEq t1 t2 b | t1 t2 -> b where | typeEq :: t1 -> t2 -> b | | instance TypeEq t t True where | typeEq = undefined | | instance (b ~ False) => TypeEq t1 t2 b where | typeEq = undefined | | If you convert this code according to the above-cited paper to use type | families instead of functional dependencies, you run into several problems. | | First, type families don’t allow overlapping with conflicting results. | Interestingly, the compiler doesn’t complain about the overlapping but about | two other things. In the first instance declaration you have something like | | type TypeEqTF t t = True | | which results in the error “Conflicting definitions for `t'”. In addition, | the second instance declaration which includes something like | | type TypeEqTF t1 t2 = b | | causes the error “Not in scope: type variable `b'”. This latter problem can | be circumvented by writing | | type TypeEqTF t1 t2 = False | | but it shows that the automatic translation doesn’t work here. | | In fact, after thinking and experimenting I came to the conclusion that it’s | probably just not possible to define a type function TypeEqTF t1 t2 which for | *all* types t1 and t2 yields True or False, depending on whether t1 and t2 | are equal or not. | | > […] | | > Simon | | Best wishes, | Wolfgang | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

| But the problem in the HList example is that two equations apply where the | most specific one should be taken. There is no difficulty in principle with this. You just need to state (and implement) the rule that the most specific equation applies. That is, there's no reason in principle you should not be able to write type instance Eq t t = True type instance Eq a b = False BUT, we need to take care here. There is one way in which indexed type family instances differ in a fundamental way from type-class instances (and hence FDs). Suppose we have module M where class C a where { foo :: ... } instance C [a] where ... Now suppose you import this into module X module X where import M instance C [Int] where ... Now, with type classes it's sort-of-OK that inside M we'll use one instance decl for (C [Int]), but a different one inside X. OK, so the two implementations of method foo will be different, but the program won't crash. Things are different with type families. Suppose we have module M where type family F :: * -> * type instance F [a] = a module X where import M type instance F [Int] = Bool Then you'll get a *seg fault* if you use the F [a] instance in one place, and the F [Int] instance in another place, when resolving a constraint involving F [Int]! (Because Bool /= Int.) That is why the current impl strictly rules out overlap for type families. Our proposed solution is that you can only use overlapping type-family instances for "closed" type families; here "closed" means that you can't add "more" instance later. Something like this: type family Eq :: * -> * -> * where Eq t t = True Eq t1 t2 = False (The 'where' means it's a closed family.) Which is fine for the application you mention. Of course none of this is implemented! Simon

| | > Of course none of this is implemented! | | But it all sounds very cool. I would like it. :-) ...and you shall have it :-) Simon

Yes, GHC also uses `cast` to express the coercion for a newtype. A type class with just one method is represented by a newtype. Nothing to do with FDs; this is two source-language constructs using the same intermediate-language encoding. (Though using casts for newtype did give rise to an unexpected interaction that I have yet to sort out! http://hackage.haskell.org/trac/ghc/ticket/1496) Simon | -----Original Message----- | From: Remi Turk [mailto:rturk@science.uva.nl] | Sent: 20 October 2007 21:25 | To: Simon Peyton-Jones | Cc: glasgow-haskell-users@haskell.org; Jean-Philippe Bernardy | Subject: Re: type families not advertised for 6.8 | | On Fri, Oct 19, 2007 at 08:25:22AM +0100, Simon Peyton-Jones wrote: | > | What does this imply for 6.8 support for FD's, as they now use | > | the same type-coercions? | > | > Actually FDs do not use type coercions, in GHC at least. As Mark | | Excuse me, it turns out I didn't look carefully enough: It's not | functional dependencies, it's classes-with-only-one-method: | | module Bar where | | bar = fmap id [] | | Compiles to the following Core with 6.8.0.20071002: | | Bar.bar :: forall a_a5M. [a_a5M] | [GlobalId] | [] | Bar.bar = | \ (@ a_a5M) -> | (GHC.Base.$f8 | `cast` ((GHC.Base.:Co:TFunctor) [] | :: (GHC.Base.:TFunctor) [] | ~ | forall a_a5G b_a5H. (a_a5G -> b_a5H) -> [a_a5G] -> [b_a5H])) | @ a_a5M @ a_a5M (GHC.Base.id @ a_a5M) (GHC.Base.[] @ a_a5M) | | | Or does this simply mean that only type-functions (the type/axiom | stuff) is not supported in 6.8, but type coercions (~ and cast) are supported | (although perhaps not at the source level)?