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 <e...@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.schonw...@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 <e...@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.hask...@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 < >> simo...@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-boun...@haskell.org [mailto: >>> glasgow-haskell-bugs-boun...@haskell.org] *On Behalf Of *Iavor Diatchki >>> *Sent:* 26 December 2012 02:48 >>> *To:* Conal Elliott >>> *Cc:* glasgow-haskell-b...@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 <co...@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-b...@haskell.org >>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs**** >>> >>> ** ** >>> >>> _______________________________________________ >>> Glasgow-haskell-users mailing list >>> Glasgow-haskell-users@haskell.org >>> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >>> >>> >> _______________________________________________ >> Glasgow-haskell-users mailing list >> Glasgow-haskell-users@haskell.org >> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >> >> >> >> _______________________________________________ >> Glasgow-haskell-users mailing list >> Glasgow-haskell-users@haskell.org >> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users >> >> > >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
