Le Fri, 6 Jan 2012 10:59:29 +0100,
Yves Parès a écrit :
> 2012/1/6 AUGER Cédric
>
> > 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
2012/1/6 AUGER Cédric
> 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 the s
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 Wed, 4 Jan 2012 20:13:34 +0100,
Yves Parès 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 'id' exi
> 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 t
Le Wed, 4 Jan 2012 16:22:31 +0100,
Yves Parès 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' refers to. I
Le Wed, 4 Jan 2012 14:41:21 +0100,
Yves Parès 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 the type of f w
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 c
On Wed, Jan 4, 2012 at 9:08 AM, Thiago Negri 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 bound by
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 ->
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
> 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
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
On Wed, Jan 4, 2012 at 08:41, Yves Parès 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 forall in
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
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 typ
On Wed, Jan 4, 2012 at 9:41 PM, Yves Parès 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.
_
> 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 8:15 PM, Yucheng Zhang 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 the wrong expect
On Wed, Jan 4, 2012 at 7:58 PM, Yves Parès 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 not expect the t
> 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
On Wed, Jan 4, 2012 at 3:46 AM, Yves Parès 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 subsome declare n
> 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
>
Le Tue, 3 Jan 2012 20:46:15 +0100,
Yves Parès 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 -> Either String
>
> 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]
On Wed, Jan 4, 2012 at 2:48 AM, Bardur Arantsson 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 different type can't
2012/1/3 Yucheng Zhang
(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 ntV g of
Noth
On Wed, Jan 4, 2012 at 1:07 AM, Yves Parès 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 type is
Coul
On Wed, Jan 4, 2012 at 1:38 AM, Yucheng Zhang wrote:
> On Wed, Jan 4, 2012 at 1:07 AM, Yves Parès 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 misunderstood the suggestion. I will try
On Wed, Jan 4, 2012 at 1:07 AM, Yves Parès 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 by
>
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.
2
On Wed, Jan 4, 2012 at 12:44 AM, Yves Parès 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 subsome type sign
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 +01
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).
2012/1/3 Yucheng Zhang
> As I investigated the code more carefully, I found that
As I investigated the code more carefully, I found that the type unification
failure may not be related to the suspected class constraint on data
constructor.
I have made minor changes to the original code to remove the Ord constraint,
including introducing a FakedMap with no requirement on Ord. T
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 req
> two uses of the same data constructor in an expression will not unify
those type variables because it's scoped to the data constructor itself
Which is somewhat clearer when using GADTs:
data LegGram t s where
LegGram :: Ord nt => M.Map nt [RRule nt t s] -> LegGram t s
Here, as the LegGram d
On Tue, Jan 3, 2012 at 7:49 PM, Yucheng Zhang 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:
http://www.haskell.org/ghc/docs
On Tue, Jan 3, 2012 at 06:43, Yves Parès 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 s])
>
> Short an
On Tue, Jan 3, 2012 at 7:46 PM, Brandon Allbery 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 some descript
On Tue, Jan 3, 2012 at 06:35, Yucheng Zhang 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 permit it
>
R
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
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
On Tue, Jan 3, 2012 at 05:50, Yucheng Zhang wrote:
> On Tue, Jan 3, 2012 at 6:44 PM, Brandon Allbery
> wrote:
> > On Tue, Jan 3, 2012 at 05:17, Yucheng Zhang wrote:
> >>
> >> subsome :: [RRule nt t s] -> Either String ([t], s)
> >>
> >> It seems to me that the compiler is not sure the two 'nt'
On Tue, Jan 3, 2012 at 6:44 PM, Brandon Allbery wrote:
> On Tue, Jan 3, 2012 at 05:17, Yucheng Zhang 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
On Tue, Jan 3, 2012 at 05:17, Yucheng Zhang 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 enabled already.
On Tue, Jan 3, 2012 at 5:43 PM, AUGER Cédric 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 (LegGram
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 tra
Hi all, I am an Haskell newbie; can someone explain me why there is
no reported error in @legSome@ but there is one in @legSomeb@
(I used leksah as an IDE, and my compiler is:
$ ghc -v
Glasgow Haskell Compiler, Version 7.2.1, stage 2 booted by GHC version
6.12.3 )
What I do not understand is tha
49 matches
Mail list logo