Ian: isn't the documentation URL below supposed to be updated nightly from
HEAD? I got it from here:
http://www.haskell.org/ghc/download#snapshots
S
From: [email protected] [mailto:[email protected]]
On Behalf Of Richard Eisenberg
Sent: 11 January 2013 14:42
To: Simon Peyton-Jones
Cc: [email protected]; Martin Sulzmann; GHC Users Mailing List
Subject: Re: Fundeps and type equality
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
<[email protected]<mailto:[email protected]>> 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:[email protected]]
Sent: 11 January 2013 03:03
To: Carter Schonwald
Cc: Martin Sulzmann;
[email protected]<mailto:[email protected]>;
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
<[email protected]<mailto:[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]<mailto:[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]<mailto:[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]<mailto:[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 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:
[email protected]<mailto:[email protected]>
[mailto:[email protected]<mailto:[email protected]>]
On Behalf Of Iavor Diatchki
Sent: 26 December 2012 02:48
To: Conal Elliott
Cc: [email protected]<mailto:[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]<mailto:[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]<mailto:[email protected]>
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
_______________________________________________
Glasgow-haskell-users mailing list
[email protected]<mailto:[email protected]>
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________
Glasgow-haskell-users mailing list
[email protected]<mailto:[email protected]>
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________
Glasgow-haskell-users mailing list
[email protected]<mailto:[email protected]>
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________
ghc-devs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/ghc-devs
