TypeFamilies vs. FunctionalDependencies & type-level recursion

[Roman Leshchinskiy]

On 30/05/2011, at 00:55, dm-list-haskell-prime at scs.stanford.edu wrote:

> I'm absolutely not advocating making overlapping instances (or, worse,
> overlapping types) part of Haskell', nor under the impression that the
> committee would ever consider doing so.  I'm just pointing out that
> right now OverlappingInstances are the only way to do recursive
> programming at the type level, for the specific reasons I outlined.  I
> hope that before FunctionalDependencies or TypeFamilies or any other
> type-level programming becomes part of Haskell', there is a way to
> differentiate base and recursive cases *without* overlapping
> instances.

FWIW, I don't think this is really about type-level recursion. You can do recursive programming with type families:

data Z
data S n

type family Plus m n
type instance Plus Z n = n
type instance Plus (S m) n = S (Plus m n)

It's deciding type equality via overlapping instances that is problematic here. But, as others have pointed out, this is somewhat dodgy anyway. I suppose what you really want is something like this:

data True
data False

type family Equal a b

Where Equal a b ~ True if and only if a and b are known to be the same type and Equal a b ~ False if and only if they are known to be different types. You could, in theory, get this by defining appropriate instances for all type constructors in a program:

type instance Equal Int Int = True
type instance Equal Int [a] = False
type instance Equal [a] Int = False
type instance Equal [a] [b] = Equal a b
...

But that's infeasible, of course. However, nothing prevents a compiler from providing this as a built-in. Arguably, this would be much cleaner than the solution based on fundeps and overlapping instances.

Roman