...@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
; 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
| The -XOverlappingInstances flag instructs GHC to allow more than one
| instance to match, provided there is a most specific one. For example,
| the constraint C Int [Int] matches instances (A), (C) and (D), but the
| last is more specific, and hence is chosen. If there is no most-specific
|
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
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
On January 11, 2013 13:55:58 Simon Peyton-Jones wrote:
| The -XOverlappingInstances flag instructs GHC to allow more than one
| instance to match, provided there is a most specific one. For example,
| the constraint C Int [Int] matches instances (A), (C) and (D), but the
| last is more
*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
: 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
:* 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
On January 10, 2013 13:56:02 Richard Eisenberg wrote:
Class instances that overlap are chosen among by order of specificity;
Sorry to jump in the middle here, but this caught my attention as this sort of
specificity determination is exactly what I had in mind when I was working on
my The shape
-haskell-users@haskell.org
| Cc: Richard Eisenberg; Martin Sulzmann; Simon Peyton-Jones
| Subject: Class instance specificity order (was Re: Fundeps and type equality)
|
| On January 10, 2013 13:56:02 Richard Eisenberg wrote:
| Class instances that overlap are chosen among by order of specificity
On Thu, 2013-01-10 at 22:17 +, Simon Peyton-Jones wrote:
Is
http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#instance-overlap
insufficiently clear? If so, let's clarify it.
Thanks for getting back to me Simon. The document says
For example, consider
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
...@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
: 26 December 2012 02:48
To: Conal Elliott
Cc: glasgow-haskell-bugs@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
: 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
-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
Hi Iavor,
Thanks much for the explanation.
Before this experiment with FDs, I was using a type family. I tried
switching to FDs, because I wanted the compiler to know that the family is
injective in order to assist type-checking. Can we declare type families to
be injective? Now I see that I ran
Hi Iavor,
Thanks much for the explanation.
Before this experiment with FDs, I was using a type family. I tried
switching to FDs, because I wanted the compiler to know that the family is
injective in order to assist type-checking. Can we declare type families to
be injective? Now I see that I ran
I presume that injectivity of type families is the sole reason why data
families exist.
Roman
* Conal Elliott co...@conal.net [2012-12-26 10:23:46-0800]
Hi Iavor,
Thanks much for the explanation.
Before this experiment with FDs, I was using a type family. I tried
switching to FDs,
I don't think that's true (though a few minutes of searching has not
yet turned up anything describing the original motivation for data
families). Sometimes you really do want to construct a family of new
data types, instead of just mapping to existing ones. I think
everyone agrees that using
* Brent Yorgey byor...@seas.upenn.edu [2012-12-26 14:49:16-0500]
I don't think that's true (though a few minutes of searching has not
yet turned up anything describing the original motivation for data
families). Sometimes you really do want to construct a family of new
data types, instead of
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
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
| And here we know that y=Bool; yet since we don't write the type sig
| directly we can't say it. So GHC's implementation of fundeps rejects
| this program; again it can't be translated into System F.
|
| Conveniently, this is a good example of my other problem with fundeps :-)
| I can work
I think that if you use the HEAD, much of
this will work, if you use the type-equality
notation. But you will probably encounter bugs
too. And in so doing, and reporting them, you'll
be doing us a service.
I did originally intend to try all this with the
HEAD, but one obstacle to this is
| I did originally intend to try all this with the
| HEAD, but one obstacle to this is the lack of recent linux
| binaries in http://www.haskell.org/ghc/dist/current/dist/
Ian is fixing that. We'd missed the fact that the bindists weren't being built.
Hold on a day or two.
Simon
| I'm trying to understand what fundeps do and don't let me do. One
| particular source of confusion is why the following program doesn't
| typecheck:
|
| {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
| module Fundeps where
|
| class Dep a b | a - b, b - a
|
| conv :: (Dep a
On Dec 3, 2007, at 4:02 AM, Simon Peyton-Jones wrote:
GHC's new intermediate language, System FC, is specifically designed
to do this. Currently we're in transition: equality constraints are
starting to work, but fundeps are implemented as they always were.
I hope we can eventually
| Is it really a good idea to permit a type signature to include
| equality constraints among unifiable types? Does the above type
| signature mean something different from a -a? Does the type signature:
| foo :: (a~Bar b) = a - Bar b
| mean something different from:
| foo :: Bar b -
On Mon, 3 Dec 2007, Simon Peyton-Jones wrote:
No, you didn't miss anything. I wouldn't expect anyone to write these
types directly. But it can happen:
class C a b | a-b
instance C Int Bool
class D x where
op :: forall y. C x y = x - y
instance D Int
Jan-Willem Maessen:
Is it really a good idea to permit a type signature to include
equality constraints among unifiable types? Does the above type
signature mean something different from a -a? Does the type
signature:
foo :: (a~Bar b) = a - Bar b
mean something different from:
foo
On 13 Apr 2006 03:27:03 -, [EMAIL PROTECTED] [EMAIL PROTECTED] wrote:
Creighton Hogg wrote:
No instance for (MatrixProduct a (Vec b) c)
arising from use of `*' at interactive:1:3-5
Probable fix: add an instance declaration for (MatrixProduct a
(Vec b) c)
In
Creighton Hogg wrote:
No instance for (MatrixProduct a (Vec b) c)
arising from use of `*' at interactive:1:3-5
Probable fix: add an instance declaration for (MatrixProduct a
(Vec b) c)
In the definition of `it': it = 10 * (vector 10 ([0 .. 9]))
Let us look at the
Hello Johannes,
Thursday, February 02, 2006, 2:17:42 PM, you wrote:
JW When I first learned functional dependencies
JW I remember I was really confused by their syntax.
JW First, it is hard to find it defined:
i should wrote this earlier, but nevertheless:
Hugs documentation contains
In article
[EMAIL PROTECTED]
ft.com,
Simon Peyton-Jones [EMAIL PROTECTED] wrote:
Here's a less complicated variant of the same problem:
class C a b | a - b where {}
instance C Int Int where {}
f :: (C Int b) = Int - b
f x = x
Is the defn of f legal? Both
Ashley Yakeley wrote:
If this were allowed, it would effectively allow type-lambda
class C a b | a - b
instance C Int Bool
instance C Bool Char
newtype T a = MkT (forall b.(C a b) = b)
helperIn :: (forall b.(C a b) = b) - T a
helperIn b = MkT b; -- currently won't work
helperOut :: T a
| I believe something along the lines of the following would work:
|
| class C a b | a - b where { foo :: b - String }
| instance C Int Int where { foo x = show (x+1) }
| x :: forall b. C Int b = b
| x = 5
|
| (Supposing that the above definition were valid; i.e., we didn't get
the
| type
| The reason, which is thoroughly explained in Simon Peyton-Jones'
| message, is that the given type signature is wrong: it should read
| f1 :: (exists b. (C Int b) = Int - b)
|
| Right. Simon pointed out that this is a pretty useless function, but
not
| entirely so, since the result of
| entirely so, since the result of it is not of type 'forall b. b', but
| rather of 'forall b. C Int b = b'. Thus, if the C class has a
function
| which takes a 'b' as an argument, then this value does have use.
I disagree. Can you give an example of its use?
I believe something
| The reason, which is thoroughly explained in Simon Peyton-Jones'
| message, is that the given type signature is wrong: it should read
| f1 :: (exists b. (C Int b) = Int - b)
Can you give an example of its use?
Yes, I can.
class (Show a, Show b) = C a b | a - b where
doit:: a -
| since this claims that it will take a Bool and produce a value of type
b
| for all types b. However, would it be all right to say (in
| pseudo-Haskell):
|
| f :: exists b . Bool - b
| f x = x
But this is a singularly useless function, because it produces a result
of utterly unknown type, so
The reason, which is thoroughly explained in Simon Peyton-Jones'
message, is that the given type signature is wrong: it should read
f1 :: (exists b. (C Int b) = Int - b)
Right. Simon pointed out that this is a pretty useless function, but not
entirely so, since the result of it is not
Hello!
It seems we can truly implement Monad2 without pushing the
envelope too far. The solution and a few tests are given below. In
contrast to the previous approach, here we lift the type variables
rather than bury them. The principle is to bring the type logic
programming at the level
Interesting example
| class Monad2 m a ma | m a - ma, ma - m a where
| return2 :: a - ma
| bind2 :: Monad2 m b mb = ma - (a - mb) - mb
| _unused :: m a - ()
| _unused = \_ - ()
| instance Monad2 [] a [a] where
| bind2 = error urk
The functional dependencies say
m a -
Hi Simon, all,
Here's a less complicated variant of the same problem:
class C a b | a - b where {}
instance C Int Int where {}
f :: (C Int b) = Int - b
f x = x
This is interesting, but I'm not entirely sure what the problem is (from a
theoretical, not
Hello!
Simon Peyton-Jones wrote:
class C a b | a - b where {}
instance C Int Int where {}
f1 :: (forall b. (C Int b) = Int - b)
f1 x = undefined
Indeed, this gives an error message
Cannot unify the type-signature variable `b' with the type `Int'
Expected type: Int
Suppose we are in case 1. Then the programmer has written a too-general
type signature on f. The programmer *must* know that b=Int in this case
otherwise his function definition makes no sense. However, I don't really
see a reason why this should be an error rather than just a warning. If
The reason, which is thoroughly explained in Simon Peyton-Jones'
message, is that the given type signature is wrong: it should read
f1 :: (exists b. (C Int b) = Int - b)
Sigh, read this after posting :)
___
Haskell mailing list
[EMAIL
On Monday 16 December 2002 18:18, Ashley Yakeley wrote:
In article [EMAIL PROTECTED],
Hal Daume III [EMAIL PROTECTED] wrote:
I spent about a half hour toying around with this and came up with the
following, which seems to work (in ghci, but not hugs -- question for
smart people: which is
Hi,
I spent about a half hour toying around with this and came up with the
following, which seems to work (in ghci, but not hugs -- question for
smart people: which is correct, if either?)...
class Mul a b c | a b - c where
mul :: a - b - c-- our standard multiplication, with fundeps
In article [EMAIL PROTECTED],
Hal Daume III [EMAIL PROTECTED] wrote:
I spent about a half hour toying around with this and came up with the
following, which seems to work (in ghci, but not hugs -- question for
smart people: which is correct, if either?)...
Both are correct. Hugs fails
At 2002-12-14 15:27, [EMAIL PROTECTED] wrote:
I define
class Mul a b c | a b - c, b a - c where mul :: a - b - c
The two constraints are identical. Each one says given a and b, you have
c.
What you want is essentially this:
class (Mul b a c) = Mul a b c where
mul :: a - b - c
mul a
--- Tom Pledger [EMAIL PROTECTED] wrote:
anatoli writes:
:
| The same error message is given for
|
| data Foo a = (Eq b) = MkFoo b
Since the type variable a is orphaned, how about reducing it to this?
data Foo = forall b . Eq b = MkFoo b
This is possible (the semantics is
Hi everybody:
I think I've found what's the problem. Still no solution in sight :(
The problem has nothing to do with fundeps. Consider an example:
data Foo a = (Eq a) = MkFoo a
This gives the same error message: type variable a is not locally
bound. Apparently, 'a' in 'Eq a' hides 'a' in
Hi Marcin,
| module M where
|
| class Seq s a | s - a where
| m :: Seq s b = (a - b) - s a - s b
This combination of constructor classes and functional dependencies
looks very odd! The dependency says that, if you pick a particular
implementation s of sequences, then there will be at most
56 matches
Mail list logo
