type families not advertised for 6.8

[Simon Peyton-Jones]

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 at haskell.org [mailto:glasgow-haskell-
| users-bounces at haskell.org] On Behalf Of Wolfgang Jeltsch
| Sent: 19 October 2007 09:51
| To: glasgow-haskell-users at 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 at haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users