Fundeps and type equality

[Roman Cheplyaka]

I presume that injectivity of type families is the sole reason why data
families exist.

Roman

* Conal Elliott <conal at conal.net> [2012-12-26 10:23:46-0800]
> 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
> >>
> >>
> >

> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users