That link looks like it points to the manual for the most recent distribution, not HEAD. The edits I put into the manual for the new family instances are not there, for example.
Richard On Jan 11, 2013, at 4:56 AM, Simon Peyton-Jones <simo...@microsoft.com> wrote: > The manual for HEAD is always online here > http://www.haskell.org/ghc/dist/current/docs/html/users_guide/type-families.html#type-instance-declarations > > Simon > > From: Richard Eisenberg [mailto:e...@cis.upenn.edu] > Sent: 11 January 2013 03:03 > To: Carter Schonwald > Cc: Martin Sulzmann; glasgow-haskell-b...@haskell.org; Simon Peyton-Jones; > GHC Users Mailing List > Subject: Re: Fundeps and type equality > > 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 fromhttp://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
