Fundeps and type equality

[Conal Elliott]

Hi Iavor,

Thanks much for the explanation.

Before this experiment with FDs, I was using a type family. I tried
switching to FDs, because I wanted the compiler to know that the family is
injective in order to assist type-checking. Can we declare type families to
be injective? Now I see that I ran into a similar problem almost two years
ago:
http://haskell.1045720.n5.nabble.com/Injective-type-families-td3385084.html.
I guess the answer is still "no", judging by this ticket:
http://hackage.haskell.org/trac/ghc/ticket/6018 .

-- Conal


On Tue, Dec 25, 2012 at 6:47 PM, Iavor Diatchki <iavor.diatchki at gmail.com>wrote:

> Hello Conal,
>
> GHC implementation of functional dependencies is incomplete: it will use
> functional dependencies during type inference (i.e., to determine the
> values of free type variables), but it will not use them in proofs, which
> is what is needed in examples like the one you posted.  The reason some
> proving is needed is that the compiler needs to figure out that for each
> instantiation of the type `ta` and `tb` will be the same (which, of course,
> follows directly from the FD on the class).
>
> As far as I understand, the reason that GHC does not construct such proofs
> is that it can't express them in its internal proof language (System FC).
>  It seems to me that it should be fairly straight-forward to extend FC to
> support this sort of proof, but I have not been able to convince folks that
> this is the case.  I could elaborate, if there's interest.
>
> In the mean time, the way forward would probably be to express the
> dependency using type families, which I find tends to be more verbose but,
> at present, is better supported in GHC.
>
> Cheers,
> -Iavor
> PS: cc-ing the GHC users' list, as there was some talk of closing the
> ghc-bugs list, but I am not sure if the transition happened yet.
>
>
>
>
>
> On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott <conal at conal.net> wrote:
>
>> I ran into a simple falure with functional dependencies (in GHC 7.4.1):
>>
>> > class Foo a ta | a -> ta
>> >
>> > foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool
>> > foo = (==)
>>
>> I expected that the `a -> ta` functional dependency would suffice to
>> prove that `ta ~ tb`, but
>>
>>     Pixie/Bug1.hs:9:7:
>>         Could not deduce (ta ~ tb)
>>         from the context (Foo a ta, Foo a tb, Eq ta)
>>           bound by the type signature for
>>                      foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb ->
>> Bool
>>           at Pixie/Bug1.hs:9:1-10
>>           `ta' is a rigid type variable bound by
>>                the type signature for
>>                  foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool
>>                at Pixie/Bug1.hs:9:1
>>           `tb' is a rigid type variable bound by
>>                the type signature for
>>                  foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool
>>                at Pixie/Bug1.hs:9:1
>>         Expected type: ta -> tb -> Bool
>>           Actual type: ta -> ta -> Bool
>>         In the expression: (==)
>>         In an equation for `foo': foo = (==)
>>     Failed, modules loaded: none.
>>
>> Any insights about what's going wrong here?
>>
>> -- Conal
>>
>> _______________________________________________
>> Glasgow-haskell-bugs mailing list
>> Glasgow-haskell-bugs at haskell.org
>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20121226/5e3abb36/attachment.htm>