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 <[email protected]> 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 <[email protected]> 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 > <[email protected]> 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 <[email protected]> >> 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: [email protected] >> [mailto:[email protected]] On Behalf Of Iavor Diatchki >> Sent: 26 December 2012 02:48 >> To: Conal Elliott >> Cc: [email protected]; 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 <[email protected]> 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 >> [email protected] >> http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs >> >> >> >> >> _______________________________________________ >> Glasgow-haskell-users mailing list >> [email protected] >> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >> >> >> _______________________________________________ >> Glasgow-haskell-users mailing list >> [email protected] >> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > > _______________________________________________ > Glasgow-haskell-users mailing list > [email protected] > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > >
_______________________________________________ Glasgow-haskell-users mailing list [email protected] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
