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 <e...@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 <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
