Fundeps and type equality

[Brent Yorgey]

I don't think that's true (though a few minutes of searching has not
yet turned up anything describing the original motivation for data
families).  Sometimes you really do want to construct a family of new
data types, instead of just mapping to existing ones.  I think
everyone agrees that using data families as a stand-in for injective
type families is a kludgy hack.

-Brent

On Wed, Dec 26, 2012 at 09:19:56PM +0200, Roman Cheplyaka wrote:
> 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
> 
> 
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users