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