TypeFamilies vs. FunctionalDependencies & type-level recursion

Andrea Vezzosi sanzhiyan at gmail.com
Tue Jun 14 18:59:55 CEST 2011


On Tue, Jun 14, 2011 at 6:31 PM, Dan Doel <dan.doel at gmail.com> wrote:
> Sorry about the double send, David. I forgot to switch to reply-all in
> the gmail interface.
>
> On Tue, Jun 14, 2011 at 11:49 AM,
> <dm-list-haskell-prime at scs.stanford.edu> wrote:
>> 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.
>
> Okay. I don't really write a lot of code like this, so maybe I missed
> the quirks.
>
> In that case, HList has been relying on broken behavior of fundeps for
> 7 years. :) Because the instance:
>
>    instance TypeEq a b c
>
> violates the functional dependency, by declaring:
>
>    instance TypeEq Int Int Int
>    instance TypeEq Int Int Char
>    instance TypeEq Int Int Double
>    ...
>    instance TypeEq Int Char Int
>    instance TypeEq Int Char Char
>    ...
>
> and adding the constraint doesn't actually affect which instances are
> being declared, it just adds a constraint requirement for when any of
> the instances are used.

I think we can argue on the truth of this point, since i don't think
that e.g. instance Ord a => Ord [a] where {...} declares an instance
for Ord [Int -> Int], even if instance resolution won't look at the
context at first.

HList is ensuring the fundep is respected, which has to be done by the
programmer when one is using UndecidableInstances, by relying on the
fact that with OverlappingInstances a more general instance matches
only when a more specific one can be shown not to match (one problem
here is that this assumption is currently broken for type variables
that come out of an existential wrapper, but surprisingly not so for
the equivalent RankNTypes encoding).

-- Andrea



More information about the Haskell-prime mailing list