Fundeps and type equality
Martin Sulzmann
martin.sulzmann.haskell at googlemail.com
Fri Jan 11 08:24:25 CET 2013
Thanks, indeed you're right.
For better or worse, so let's extend FC to include FD-style improvement :)
Aren't we running then into the same 'type soundness' issues (connected to
ordering of overlapping instances) you mention below?
There's currently no issue for FDs because FD-style improvement is not
manifested in GHC's internal language FC.
So, if FD-style improvement will be treated similarly compared to type
families, then we might have to rethink the entire case of overlapping type
class instances?
-Martin
On Thu, Jan 10, 2013 at 7:56 PM, Richard Eisenberg <eir at cis.upenn.edu>wrote:
> For better or worse, the new overlapping type family instances use a
> different overlapping mechanism than functional dependencies do. Class
> instances that overlap are chosen among by order of specificity;
> overlapping instances can be declared in separate modules. Overlapping
> family instances must be given an explicit order, and those that overlap
> must all be in the same module. The decision to make these different was to
> avoid type soundness issues that would arise with overlapping type family
> instances declared in separate modules. (Ordering a set of family instance
> equations by specificity, on the other hand, could easily be done within
> GHC.)
>
> So, as yet, we can't fully encode functional dependencies with type
> families, I don't think.
>
> Richard
>
> On Jan 2, 2013, at 4:01 PM, Martin Sulzmann <
> martin.sulzmann.haskell at googlemail.com> wrote:
>
>
> 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
>>
>>
> _______________________________________________
> 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/20130111/eca06d36/attachment.htm>
More information about the Glasgow-haskell-users
mailing list