Fundeps and type equality
Carter Schonwald
carter.schonwald at gmail.com
Fri Jan 11 22:36:15 CET 2013
Cool!
For some reason I had thought that wasn't previously allowed, thanks for
clarifying!
That said, the new overlapping type families should make things a bit
easier to write.
awesome
-Carter
On Fri, Jan 11, 2013 at 4:04 PM, Richard Eisenberg <eir at cis.upenn.edu>wrote:
> Recursive type level functions are actually not new -- type families as
> they have existed for some time can be recursive. The new overlap mechanism
> doesn't really interact with the recursion feature in any interesting way.
> For anything moderately interesting and recursive, though, you will have to
> enable UndecidableInstances, but the only potential harm that extension can
> cause is for GHC to hang; your program will still be guaranteed not to
> crash if it compiles.
>
> Enjoy hacking with types!
> Richard
>
> On Jan 11, 2013, at 3:52 PM, Carter Schonwald wrote:
>
> One thing thats unclear (or at least implicit) about the overlapping type
> families from the docs is this:
> does it let me write recursive type level functions? (I really really
> really want that :) )
>
> thanks
> -Carter
>
>
> On Thu, Jan 10, 2013 at 10:03 PM, Richard Eisenberg <eir at cis.upenn.edu>wrote:
>
>> Yes, I finished and pushed in December. A description of the design and
>> how to use the feature is here:
>> http://hackage.haskell.org/trac/ghc/wiki/NewAxioms
>>
>> There's also a section (7.7.2.2 to be exact) in the manual, but building
>> the manual from source is not for the faint of heart.
>>
>> Richard
>>
>> On Jan 10, 2013, at 3:14 PM, Carter Schonwald <carter.schonwald at gmail.com>
>> wrote:
>>
>> so the overlapping type families are in HEAD?
>>
>> Awesome! I look forward to finding some time to try them out :)
>>
>>
>> On Thu, Jan 10, 2013 at 1: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
>>>
>>>
>>>
>>> _______________________________________________
>>> 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/9da5ded7/attachment.htm>
More information about the Glasgow-haskell-users
mailing list