Fundeps and type equality

[Martin Sulzmann]

I agree with Iavor that it is fairly straight-forward to extend FC to
support FD-style type improvement. In fact, I've formalized such a proof
language in a PPDP'06 paper:
"Extracting programs from type class proofs"
(type improvement comes only at the end)

Similar to FC, coercions (proof terms) are used to represent type equations
(improvement).

Why extend FC?
Why not simply use type families to encode FDs (and thus keep FC simple and
small).

It's been a while, but as far as I remember, the encoding is only
problematic in case of the combination of FDs and overlapping instances.
Shouldn't this now be fixable given
that type family instances can be overlapping?
Maybe I'm missing something, guess it's also time to dig out some old notes
...

-Martin

On Wed, Jan 2, 2013 at 10:04 AM, Simon Peyton-Jones
<simonpj at microsoft.com>wrote:

>  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).  ****
>
> ** **
>
> Iavor is quite right****
>
> ** **
>
> 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.****
>
> ** **
>
> Iavor: I don’t think it’s straightforward, but I’m willing to be
> educated.  By all means start a wiki page to explain how, if you think it
> is.  ****
>
> ** **
>
> I do agree that injective type families would be a good thing, and would
> deal with the main reason that fundeps are sometimes better than type
> families.  A good start would be to begin a wiki page to flesh out the
> design issues, perhaps linked from
> http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions****
>
> ** **
>
> The main issues are, I think:****
>
> **·         **How to express functional dependencies like “fixing the
> result type and the first argument will fix the second argument”****
>
> **·         **How to express that idea in the proof language****
>
> ** **
>
> Simon****
>
> ** **
>
> *From:* glasgow-haskell-bugs-bounces at haskell.org [mailto:
> glasgow-haskell-bugs-bounces at haskell.org] *On Behalf Of *Iavor Diatchki
> *Sent:* 26 December 2012 02:48
> *To:* Conal Elliott
> *Cc:* glasgow-haskell-bugs at haskell.org; GHC Users Mailing List
> *Subject:* Re: Fundeps and type equality****
>
> ** **
>
> 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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130102/1b21ecee/attachment-0001.htm>