2012/1/6 AUGER Cédric sedri...@gmail.com
when you write forall a. exists b. a - b - a, then you allow the
caller to have access to b to produce a (didn't you write a-b-a?)
Yes, sorry, I always assumed independence between the type variables. Like
in:
f :: forall a. a - (forall b. b - a)
being
Le Fri, 6 Jan 2012 10:59:29 +0100,
Yves Parès limestr...@gmail.com a écrit :
2012/1/6 AUGER Cédric sedri...@gmail.com
when you write forall a. exists b. a - b - a, then you allow the
caller to have access to b to produce a (didn't you write
a-b-a?)
Yes, sorry, I always assumed
Thanks Cédric for your explanations.
To sum up, that's the way I understood all this, in a bit less formal way:
(Could help some, I guess)
Universal quantification (forall) means that the *caller *will instanciate
(fix) the type variables, and that *callee *cannot know those types.
Existential
Le Tue, 3 Jan 2012 20:46:15 +0100,
Yves Parès limestr...@gmail.com a écrit :
Actually, my question is why the different type can't be unified
with the
inferred type?
Because without ScopedTypeVariable, both types got expanded to :
legSome :: *forall nt* t s. LegGram nt t s - nt -
Ocaml community (where most people strongly rely on type inference
and do not put types very often)
Well it's the same for Haskell.
foo :: bar - foobar - barfoo
foo b = let *fooAux :: foobar - barfoo* -- You can comment it out
fooAux fb = if f b fb
then
On Wed, Jan 4, 2012 at 3:46 AM, Yves Parès limestr...@gmail.com wrote:
Because without ScopedTypeVariable, both types got expanded to :
legSome :: forall nt t s. LegGram nt t s - nt - Either String ([t], s)
subsome :: forall nt t s. [RRule nt t s] - Either String ([t], s)
So you see
f :: a - a
f x = x :: a -- invalid
Perfect example indeed.
The confusing point to me is that the 'a' from 'f' type signature on
its own is not universally quantified as I expected,
and it is dependent on the type of 'f'.
This dependence is not obvious for a beginner like me.
It's indeed
On Wed, Jan 4, 2012 at 7:58 PM, Yves Parès limestr...@gmail.com wrote:
f :: forall a. a - a
f x = x :: forall a. a
Which is obviously wrong: when you have entered f, x has been instatiated to
a specific type 'a', and then you want it to x to be of any type? That
doesn't make sense.
I did
On Wed, Jan 4, 2012 at 8:15 PM, Yucheng Zhang yczhan...@gmail.com wrote:
I expected the type of 'x' to be universally quantified, and thus can be
unified
with 'forall a. a' with no problem.
I've never been thinking in a detailed level, and the 'x' appears to be able to
take any type, and thus
I expected the type of 'x' to be universally quantified, and thus can be
unified with 'forall a. a' with no problem
As I get it. 'x' is not universally quantified. f is. [1]
x would be universally quantified if the type of f was :
f :: (forall a. a) - (forall a. a)
[1] Yet here I'm not sure
On Wed, Jan 4, 2012 at 9:41 PM, Yves Parès limestr...@gmail.com wrote:
Would you try:
f :: a - a
f x = undefined :: a
And tell me if it works? IMO it doesn't.
It works.
As I understand, in this situation we are specializing the 'undefined
:: forall a. a'
to a more specific dependent type.
One should keep in mind the distinction between schematic variables
(which participate in unification) and universally quantified
variables. Let's look at the forall-elimination rule
G |- e : forall a. A
E
G |- e : A[a := t]
If the term e has the
Yes but as I understood it the type inferer was taking your type annotation
for granted, and apparently in fact it re-specifies it.
What you said was in reality:
f :: forall. a - a
f x = undefined :: forall a1. a1
And it turned it into:
f :: forall. a - a
f x = undefined :: a
(here, 'a' would be
On Wed, Jan 4, 2012 at 08:41, Yves Parès limestr...@gmail.com wrote:
Would you try:
f :: a - a
f x = undefined :: a
And tell me if it works? IMO it doesn't.
It won't; a will be a new type variable unrelated to the one in the
signature, in the absence of ScopedTypeVariables and an explicit
So is there anyway to force the scoping of variables, so that
f :: a - a
f x = x :: a
becomes valid?
Do we need to do it the Ocaml way, that is not declaring the first
line, activate XScopedVariables and do:
f :: a - a = \x - x :: a
or
f (x :: a) = x :: a
or
some other thing
?
I don't see the
I don't see the point in universally quantifying over types which are
already present in the environment
I think it reduces the indeterminacy you come across when you read your
program (where does this type variable come from, btw?)
So is there anyway to force the scoping of variables, so that
Do not compile:
f :: a - a
f x = x :: a
Couldn't match type `a' with `a1'
`a' is a rigid type variable bound by
the type signature for f :: a - a at C:\teste.hs:4:1
`a1' is a rigid type variable bound by
an expression type signature: a1 at C:\teste.hs:4:7
Oleg explained why those work in his last post. It's the exact same logic
for each one.
f :: a - a
f x = x :: a
We explained that too: it's converted (alpha-converted, but I don't exactly
know what 'alpha' refers to. I guess it's phase the type inferer goes
through) to:
f :: forall a. a - a
f
On Wed, Jan 4, 2012 at 9:08 AM, Thiago Negri evoh...@gmail.com wrote:
Do not compile:
f :: a - a
f x = x :: a
Couldn't match type `a' with `a1'
`a' is a rigid type variable bound by
the type signature for f :: a - a at C:\teste.hs:4:1
`a1' is a rigid type variable
Got it. Thanks. :)
The gotcha for me is that I was thinking as a generic type 'a' that I
may and not in terms if something is typed a generic 'a', then it
must fit in ANY type. I think this is a common mistake, as I did read
about it more than once.
I.e.,
undefined :: a means a value that can
Le Wed, 4 Jan 2012 14:41:21 +0100,
Yves Parès limestr...@gmail.com a écrit :
I expected the type of 'x' to be universally quantified, and thus
can be unified with 'forall a. a' with no problem
As I get it. 'x' is not universally quantified. f is. [1]
x would be universally quantified if
Le Wed, 4 Jan 2012 16:22:31 +0100,
Yves Parès limestr...@gmail.com a écrit :
Oleg explained why those work in his last post. It's the exact same
logic for each one.
f :: a - a
f x = x :: a
We explained that too: it's converted (alpha-converted, but I don't
exactly know what 'alpha'
f :: forall a. (forall b. b - b) - a - a
f id x = id x
is very similar to the first case, x is still universally quantified (a)
and there is an existential quantification in id (b).
I don't get it. What is 'id' existentially quantified in?
f calls id so f will decide what will be its type.
Le Wed, 4 Jan 2012 20:13:34 +0100,
Yves Parès limestr...@gmail.com a écrit :
f :: forall a. (forall b. b - b) - a - a
f id x = id x
is very similar to the first case, x is still universally
quantified (a) and there is an existential quantification in id (b).
I don't get it. What is
Perhaps you should give us the error the compiler give you.
Plus:
data LegGram nt t s = Ord nt = LegGram (M.Map nt [RRule nt t s])
will become invalid. Currently, such class constraints are ignored.
You should remove the 'Ord nt' constraint and add it to you legSome
function. (Maybe that's a
On Tue, Jan 3, 2012 at 5:43 PM, AUGER Cédric sedri...@gmail.com wrote:
legSomeb :: LegGram nt t s - nt - Either String ([t], s)
-- but without it I have an error reported
legSomeb (LegGram g) ntV =
case M.lookup ntV g of
Nothing - Left No word accepted!
Just l - let sg = legSomeb
On Tue, Jan 3, 2012 at 05:17, Yucheng Zhang yczhan...@gmail.com wrote:
subsome :: [RRule nt t s] - Either String ([t], s)
It seems to me that the compiler is not sure the two 'nt' are equal.
The ScopedTypeVariables can make the compiler believe they are equal.
But ScopedTypeVariables is
On Tue, Jan 3, 2012 at 6:44 PM, Brandon Allbery allber...@gmail.com wrote:
On Tue, Jan 3, 2012 at 05:17, Yucheng Zhang yczhan...@gmail.com wrote:
subsome :: [RRule nt t s] - Either String ([t], s)
It seems to me that the compiler is not sure the two 'nt' are equal.
The ScopedTypeVariables
On Tue, Jan 3, 2012 at 05:50, Yucheng Zhang yczhan...@gmail.com wrote:
On Tue, Jan 3, 2012 at 6:44 PM, Brandon Allbery allber...@gmail.com
wrote:
On Tue, Jan 3, 2012 at 05:17, Yucheng Zhang yczhan...@gmail.com wrote:
subsome :: [RRule nt t s] - Either String ([t], s)
It seems to me
As I understand it, both ways work.
legSome ((LegGram g)::LegGram nt t s) ntV
If you compile this without ScopedTypeVariables extension, GHC will
remind you of it:
Illegal signature in pattern: LegGram nt t s
Use -XScopedTypeVariables to permit it
So another solution is to avoid
That is error-prone.
Plus the code does not need ScopedTypeVariables. The real problem comes
from the use of a class constraint on the LegGram data constructor.
data LegGram nt t s = Ord nt = LegGram (M.Map nt [RRule nt t s])
Short answer: you *can't *add class constraints to an already declared
On Tue, Jan 3, 2012 at 06:35, Yucheng Zhang yczhan...@gmail.com wrote:
legSome ((LegGram g)::LegGram nt t s) ntV
If you compile this without ScopedTypeVariables extension, GHC will
remind you of it:
Illegal signature in pattern: LegGram nt t s
Use -XScopedTypeVariables to
On Tue, Jan 3, 2012 at 7:46 PM, Brandon Allbery allber...@gmail.com wrote:
Right, but I think this is conflating two aspects of ScopedTypeVariables and
may not bring them into scope fully. Although, that's a question for
someone who understands ghc's type system far better than I do.
I found
On Tue, Jan 3, 2012 at 06:43, Yves Parès limestr...@gmail.com wrote:
That is error-prone.
Plus the code does not need ScopedTypeVariables. The real problem comes
from the use of a class constraint on the LegGram data constructor.
data LegGram nt t s = Ord nt = LegGram (M.Map nt [RRule nt t
On Tue, Jan 3, 2012 at 7:49 PM, Yucheng Zhang yczhan...@gmail.com wrote:
I found some descriptions of ScopedTypeVariables here:
http://hackage.haskell.org/trac/haskell-prime/wiki/ScopedTypeVariables
Sorry, I found just now a more up-to-date description in the GHC documentation:
Thanks all,
I finally give up to put Ord in the LegGram type.
What was annoying me was that @legsome@ was in fact an instance of a
class I defined. So I changed its signature to make it depend on Ord.
That is not very nice, since at first glance, there could be
implementations which does not
The other much simpler solution no one has mentioned yet is to just
pull 'subsome' out as its own top-level declaration. Having such a
big function nested locally within a 'let' is ugly anyway, and it
makes it harder to test and debug than necessary.
-Brent
On Tue, Jan 03, 2012 at 05:44:01PM
On Wed, Jan 4, 2012 at 12:44 AM, Yves Parès limestr...@gmail.com wrote:
Remove subsome type signature. You are redeclaring type variables which
obviously cannot match those of legSome.
This cannot work without scoped type variables (and ad-hoc foralls to bring
them to scope, of course).
That
Brent is right. Separating functions is nicer to read and cleaner. Plus it
enhances testability.
I wonder why the redeclared type variables cannot match those of legSome?
Try to put a totally wrong type to subsome, like
subsome :: Int
and tell us from the error what type is actually inferred.
On Wed, Jan 4, 2012 at 1:07 AM, Yves Parès limestr...@gmail.com wrote:
Try to put a totally wrong type to subsome, like
subsome :: Int
and tell us from the error what type is actually inferred.
The error is like
Couldn't match type `nt' with `Int'
`nt' is a rigid type variable bound
On Wed, Jan 4, 2012 at 1:38 AM, Yucheng Zhang yczhan...@gmail.com wrote:
On Wed, Jan 4, 2012 at 1:07 AM, Yves Parès limestr...@gmail.com wrote:
Try to put a totally wrong type to subsome, like
subsome :: Int
and tell us from the error what type is actually inferred.
Sorry, I found I
On Wed, Jan 4, 2012 at 1:07 AM, Yves Parès limestr...@gmail.com wrote:
I wonder why the redeclared type variables cannot match those of legSome?
Try to put a totally wrong type to subsome, like
subsome :: Int
and tell us from the error what type is actually inferred.
The actually inferred
2012/1/3 Yucheng Zhangyczhan...@gmail.com
(Hopefully being a little more explicit about this can help you
understand where things are going wrong.)
[--snip--]
legSome :: LegGram nt t s - nt - Either String ([t], s)
The 'nt' you see above
legSome (LegGram g) ntV =
case Main.lookup
On Wed, Jan 4, 2012 at 2:48 AM, Bardur Arantsson s...@scientician.net wrote:
'subsome' to a different type than the one you intended -- and indeed one
which can't be unified with the inferred type. (Unless you use
ScopedTypeVariables.)
Thanks for the reply.
Actually, my question is why the
Actually, my question is why the different type can't be unified with the
inferred type?
Because without ScopedTypeVariable, both types got expanded to :
legSome :: *forall nt* t s. LegGram nt t s - nt - Either String ([t], s)
subsome :: *forall nt* t s. [RRule nt t s] - Either String ([t],
45 matches
Mail list logo
