TypeFamilies vs. FunctionalDependencies & type-level recursion

[dm-list-haskell-prime at scs.stanford.edu]

At Tue, 14 Jun 2011 10:40:48 -0400,
Dan Doel wrote:
> 
> > 1. As things stand in GHC you can do some things with functional dependencies that you can't do with type families. The archetypical example is type equality.  We cannot write
> >        type family Eq a b :: *
> >        type instance Eq k k = True
> >        type instance Eq j k = False
> > because the two instances overlap.  But you can with fundeps
> >        class Eq a b c | a b -> c
> >        instance Eq k k True
> >        instance Eq j k False
> > As Alexey mentioned, fundeps have other disadvantages, so it's reasonable to ask whether type families could extend to handle cases like this.
> 
> Fundeps no longer allow this as of GHC 7, it seems. It causes the same
> fundep violation as the case:
> 
>     class C a b | a -> b
>     instance C a R
>     instance C T U

You absolutely still can use FunctionalDependencies to determine type
equality in GHC 7.  For example, I just verified the code below with
GHC 7.02:

*Main> typeEq True False
HTrue
*Main> typeEq (1 :: Int) (2 :: Int)
HTrue
*Main> typeEq (1 :: Int) False
HFalse

As always, you have to make sure one of the overlapping instances is
more specific than the other, which you can do by substituting a
parameter c for HFalse in the false case and fixing c to HFalse using
another class like TypeCast in the context.  (As contexts play no role
in instance selection, they don't make the instance any more
specific.)

While I don't have convenient access to GHC 6 right this second, I'm
pretty sure there has been no change for a while, as the HList paper
discussed this topic in 2004.

David


{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE UndecidableInstances #-}

class TypeCast a b | a -> b where
    typeCast :: a -> b
instance TypeCast a a where
    typeCast = id

data HTrue = HTrue deriving (Show)
data HFalse = HFalse deriving (Show)

class TypeEq a b c | a b -> c where
    typeEq :: a -> b -> c
instance TypeEq a a HTrue where
    typeEq _ _ = HTrue
instance (TypeCast HFalse c) => TypeEq a b c where
    typeEq _ _ = typeCast HFalse