TypeFamilies vs. FunctionalDependencies & type-level recursion
Andrea Vezzosi
sanzhiyan at gmail.com
Tue Jun 14 17:27:07 CEST 2011
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
>
More information about the Haskell-prime
mailing list