TypeFamilies vs. FunctionalDependencies & type-level recursion

[Andrea Vezzosi]

On Tue, Jun 14, 2011 at 4:40 PM, Dan Doel <dan.doel at gmail.com> wrote:
> On Tue, Jun 14, 2011 at 5:36 AM, Simon Peyton-Jones
> <simonpj at microsoft.com> wrote:
>> There was an interesting thread on haskell-prime [1], about the relationship between functional dependencies and type families.  This message is my attempt to summarise the conclusions of that thread.  I'm copying other interested parties (eg Oleg, Dimitrios)
>>  [1] http://www.haskell.org/pipermail/haskell-prime/2011-May/003416.html
>>
>> 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

Are you sure that worked before? The following still does anyhow:

    {-# LANGUAGE MultiParamTypeClasses, OverlappingInstances,
FunctionalDependencies
                            , EmptyDataDecls, FlexibleInstances,
UndecidableInstances #-}

    class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b
    class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a->b
    class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a->b
    instance TypeCast'  () a b => TypeCast a b where typeCast x = typeCast' () x
    instance TypeCast'' t a b => TypeCast' t a b where typeCast' = typeCast''
    instance TypeCast'' () a a where typeCast'' _ x  = x

    data R
    data T
    data U
    class C a b | a -> b
    instance TypeCast R b => C a b
    instance TypeCast U b => C T b

In fact this is how IsFunction was implemented in 2005[1], and the
same transformation appears to work for the Eq class too.
If we allow TypeFamilies we can use (~) instead of the TypeCast hack,
fortunately.

[1] http://okmij.org/ftp/Haskell/isFunction.lhs

-- Andrea

> for R /~ U. Which I find somewhat sensible, because the definitions
> together actually declare two relations for any type:
>
>    Eq T T False
>    Eq T T True
>
> and we are supposed to accept that because one is in scope, and has a
> particular form, the other doesn't exist. But they needn't always be
> in scope at the same time.
>
> Essentially, GHC 7 seems to have separated the issue of type-function
> overlapping, which is unsound unless you have specific conditions that
> make it safe---conditions which fundeps don't actually ensure (fundeps
> made it 'safe' in the past by not actually doing all the computation
> that type families do)---from the issue of instance overlapping, which
> is always sound at least. But if I'm not mistaken, type families can
> handle these cases.
>
> I'd personally say it's a step in the right direction, but it probably
> breaks a lot of HList-related stuff.
>
> -- Dan
>
> _______________________________________________
> Haskell-prime mailing list
> Haskell-prime at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-prime
>