Little question about "forall"

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Baa
Reply | Threaded
Open this post in threaded view
|

Little question about "forall"

Baa
Hello everyone!

Suppose I have:

  class C a where
    someA :: a

  f :: C a => a -> Int
  f a =
    let x = someA :: a in -- BUG!!
      0
 
BUG as I understand I due to `:: a` - this is another `a`, not the same as
in `f` singature. But seems that it's the same `a` if `f` is the "method"
of some instance. And such bug does not happen if I return it, so my question
is how to create such `x` of type `a` in the body of the `f`? How to use
`a` anywhere in the body of `f`? Is it possible?
 
I found a way if I change signature to `forall a. C a => a -> Int`. But there
are another questions in the case:
 
 - as I know all such params are under "forall" in Haskell by-default. Seems
   it's not true?
 - in method body seems they are under "forall" but in simple functions - not?
 - i'm not sure what exactly does this "forall", IMHO it unbounds early bound
   type's variables (parameters) by typechecker, but how `a` can be bound in the
   just begining of signature (where it occurs first time) ?!
 
As for me, looks that w/o "forall" all `a`, `b`, `c`, etc in the body of
simple functions always are different types. But w/ "forall" Haskell typechecker
makes something like (on type-level):
 
   let a = ANY-TYPE
   in
      ... here `a` can occur and will be bound to ANY-TYPE
 
Where am I right and where am I wrong? :)

===
Best regards, Paul
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Little question about "forall"

David McBride
As to your original code, the only actual bug is that someA :: a is wrong.  The actual type of someA is someA :: C a => a, so you could have written

class C a where
  someA :: a

f :: C a => a -> Int
f a =
  let x :: C a => a
      x = someA -- absolutely works
  in 0


But remember that in x, 'a' is not the same as the 'a' in f, so you might as well have written this

  f :: C a => a -> Int
  f a =
    let x :: C b => b
        x = someA -- also works
    in 0

This is how it works.  When you write

f :: C a => a -> ()
f =
  let x = someA  -- without ':: a'
  ()

The problem is that by not giving an explicit type to x, ghc infers a type and for all intents and purposes it is as though you wrote

f :: C a => a -> ()
f =
  let x :: C a1 => a1
      x = someA
      -- also  if you had written x = some :: a, it just means you effectively wrote
      -- let x :: C a1 => a1
      --     x = someA :: a
      -- but 'a1' is not equivalent to 'a', so it errors.
  ()

And so it says hey wait, a and a1 could be different types.  That is why you often see ghc referring to 'a1' or 'a0' in error messages, because when it infers a type it has to give a name to it in order to report on it.

What ScopedTypeVariables does is allow you to specify that for the entire scope of this forall, 'a' in any type signature always refers to the same type.

f :: forall a. C a => a -> ()
f = undefined
where
  some :: a -- this is guaranteed to be the a from above.
  some = undefined

  somethingelse :: forall a. a -- this is a different a
  somethingelse = undefined

some :: a -- this toplevel a is of course also different.
some = undefined

So you could just go
{-# LANGUAGE ScopedTypeVariables #-}

f :: forall a. C a => a -> Int
f a =
  let
     x :: a  -- now the a is the same a as above, so the constraint C a is understood.
     x = someA
  in 0

I really love the ScopedTypeVariables extension, and so do a lot of other people.  I honestly think it should be on by default because the pitfalls of not having it on are a lot worse than the pitfalls of having it on.  The only pitfall I know of to having it on is that if you have a function with tons of lets and / or wheres, you might not notice you had used the type variable 'a' in two different incompatible places.

Hopefully all this makes sense.



On Thu, Dec 7, 2017 at 6:41 AM, Baa <[hidden email]> wrote:
Hello everyone!

Suppose I have:

  class C a where
    someA :: a

  f :: C a => a -> Int
  f a =
    let x = someA :: a in -- BUG!!
      0

BUG as I understand I due to `:: a` - this is another `a`, not the same as
in `f` singature. But seems that it's the same `a` if `f` is the "method"
of some instance. And such bug does not happen if I return it, so my question
is how to create such `x` of type `a` in the body of the `f`? How to use
`a` anywhere in the body of `f`? Is it possible?

I found a way if I change signature to `forall a. C a => a -> Int`. But there
are another questions in the case:

 - as I know all such params are under "forall" in Haskell by-default. Seems
   it's not true?
 - in method body seems they are under "forall" but in simple functions - not?
 - i'm not sure what exactly does this "forall", IMHO it unbounds early bound
   type's variables (parameters) by typechecker, but how `a` can be bound in the
   just begining of signature (where it occurs first time) ?!

As for me, looks that w/o "forall" all `a`, `b`, `c`, etc in the body of
simple functions always are different types. But w/ "forall" Haskell typechecker
makes something like (on type-level):

   let a = ANY-TYPE
   in
      ... here `a` can occur and will be bound to ANY-TYPE

Where am I right and where am I wrong? :)

===
Best regards, Paul
_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners


_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Baa
Reply | Threaded
Open this post in threaded view
|

Re: Little question about "forall"

Baa
Hello, David!

> But remember that in x, 'a' is not the same as the 'a' in f, so you

Exactly, and I often hit errors like "Can't match rigid type 'M a' with
rigid type 'M a1'"! So, the question comes down to "forall" and
"ScopedTypeVariables". Did I understand you correctly:

this extension expands type-variable scope to whole function body. But
what sort of type vairables? Only under "forall ...", right ?

And another question: type-variables under "forall" - they are rigid?
Or free? I can't understand the terminology. I thought early that they
are called "rigid", but in documentation of "ScopedTypeVariables"
extension they are called "free". IMHO symbol ∀ means "unbound", so
"free". But I often hit errors when GHC says something about rigid, so
I'm not sure - what is rigid? Bound?

And last: why I need "forall a." in beginning of signature while
Haskell assumes "forall" for all type variables by default? Or I'm not
right here...


> As to your original code, the only actual bug is that someA :: a is
> wrong. The actual type of someA is someA :: C a => a, so you could
> have written
>
> class C a where
>   someA :: a
>
> f :: C a => a -> Int
> f a =
>   let x :: C a => a
>       x = someA -- absolutely works
>   in 0
>
>
> But remember that in x, 'a' is not the same as the 'a' in f, so you
> might as well have written this
>
>   f :: C a => a -> Int
>   f a =
>     let x :: C b => b
>         x = someA -- also works
>     in 0
>
> This is how it works.  When you write
>
> f :: C a => a -> ()
> f =
>   let x = someA  -- without ':: a'
>   ()
>
> The problem is that by not giving an explicit type to x, ghc infers a
> type and for all intents and purposes it is as though you wrote
>
> f :: C a => a -> ()
> f =
>   let x :: C a1 => a1
>       x = someA
>       -- also  if you had written x = some :: a, it just means you
> effectively wrote
>       -- let x :: C a1 => a1
>       --     x = someA :: a
>       -- but 'a1' is not equivalent to 'a', so it errors.
>   ()
>
> And so it says hey wait, a and a1 could be different types.  That is
> why you often see ghc referring to 'a1' or 'a0' in error messages,
> because when it infers a type it has to give a name to it in order to
> report on it.
>
> What ScopedTypeVariables does is allow you to specify that for the
> entire scope of this forall, 'a' in any type signature always refers
> to the same type.
>
> f :: forall a. C a => a -> ()
> f = undefined
> where
>   some :: a -- this is guaranteed to be the a from above.
>   some = undefined
>
>   somethingelse :: forall a. a -- this is a different a
>   somethingelse = undefined
>
> some :: a -- this toplevel a is of course also different.
> some = undefined
>
> So you could just go
> {-# LANGUAGE ScopedTypeVariables #-}
>
> f :: forall a. C a => a -> Int
> f a =
>   let
>      x :: a  -- now the a is the same a as above, so the constraint C
> a is understood.
>      x = someA
>   in 0
>
> I really love the ScopedTypeVariables extension, and so do a lot of
> other people.  I honestly think it should be on by default because
> the pitfalls of not having it on are a lot worse than the pitfalls of
> having it on.  The only pitfall I know of to having it on is that if
> you have a function with tons of lets and / or wheres, you might not
> notice you had used the type variable 'a' in two different
> incompatible places.
>
> Hopefully all this makes sense.
>
>
>
> On Thu, Dec 7, 2017 at 6:41 AM, Baa <[hidden email]> wrote:
>
> > Hello everyone!
> >
> > Suppose I have:
> >
> >   class C a where
> >     someA :: a
> >
> >   f :: C a => a -> Int
> >   f a =
> >     let x = someA :: a in -- BUG!!
> >       0
> >
> > BUG as I understand I due to `:: a` - this is another `a`, not the
> > same as in `f` singature. But seems that it's the same `a` if `f`
> > is the "method" of some instance. And such bug does not happen if I
> > return it, so my question
> > is how to create such `x` of type `a` in the body of the `f`? How
> > to use `a` anywhere in the body of `f`? Is it possible?
> >
> > I found a way if I change signature to `forall a. C a => a -> Int`.
> > But there
> > are another questions in the case:
> >
> >  - as I know all such params are under "forall" in Haskell
> > by-default. Seems
> >    it's not true?
> >  - in method body seems they are under "forall" but in simple
> > functions - not?
> >  - i'm not sure what exactly does this "forall", IMHO it unbounds
> > early bound
> >    type's variables (parameters) by typechecker, but how `a` can be
> > bound in the
> >    just begining of signature (where it occurs first time) ?!
> >
> > As for me, looks that w/o "forall" all `a`, `b`, `c`, etc in the
> > body of simple functions always are different types. But w/
> > "forall" Haskell typechecker
> > makes something like (on type-level):
> >
> >    let a = ANY-TYPE
> >    in
> >       ... here `a` can occur and will be bound to ANY-TYPE
> >
> > Where am I right and where am I wrong? :)
> >
> > ===
> > Best regards, Paul
> > _______________________________________________
> > Beginners mailing list
> > [hidden email]
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
> >  

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Reply | Threaded
Open this post in threaded view
|

Re: Little question about "forall"

David McBride
Rigid just means the compiler knows the type without having to infer it.  And if the type is inferred to be different than what you said it should be, you get an error that says 's' is  a rigid type variable bound by ... presumably the type signature.

I'm not sure what free means.  My best guess is that a local variable is free if it is not referred to in the type signature of the encompassing (? surrounding?) scope.

forall a. is just what what ScopedTypeVariables uses to ensure that local variables in the function with the same type variables are no longer free, and that they must adhere to the type signature of the encompassing scope.

My terminology is terrible, and I've probably made a mistake, but hopefully someone will correct me.

On Thu, Dec 7, 2017 at 10:31 AM, Baa <[hidden email]> wrote:
Hello, David!

> But remember that in x, 'a' is not the same as the 'a' in f, so you

Exactly, and I often hit errors like "Can't match rigid type 'M a' with
rigid type 'M a1'"! So, the question comes down to "forall" and
"ScopedTypeVariables". Did I understand you correctly:

this extension expands type-variable scope to whole function body. But
what sort of type vairables? Only under "forall ...", right ?

And another question: type-variables under "forall" - they are rigid?
Or free? I can't understand the terminology. I thought early that they
are called "rigid", but in documentation of "ScopedTypeVariables"
extension they are called "free". IMHO symbol ∀ means "unbound", so
"free". But I often hit errors when GHC says something about rigid, so
I'm not sure - what is rigid? Bound?

And last: why I need "forall a." in beginning of signature while
Haskell assumes "forall" for all type variables by default? Or I'm not
right here...


> As to your original code, the only actual bug is that someA :: a is
> wrong. The actual type of someA is someA :: C a => a, so you could
> have written
>
> class C a where
>   someA :: a
>
> f :: C a => a -> Int
> f a =
>   let x :: C a => a
>       x = someA -- absolutely works
>   in 0
>
>
> But remember that in x, 'a' is not the same as the 'a' in f, so you
> might as well have written this
>
>   f :: C a => a -> Int
>   f a =
>     let x :: C b => b
>         x = someA -- also works
>     in 0
>
> This is how it works.  When you write
>
> f :: C a => a -> ()
> f =
>   let x = someA  -- without ':: a'
>   ()
>
> The problem is that by not giving an explicit type to x, ghc infers a
> type and for all intents and purposes it is as though you wrote
>
> f :: C a => a -> ()
> f =
>   let x :: C a1 => a1
>       x = someA
>       -- also  if you had written x = some :: a, it just means you
> effectively wrote
>       -- let x :: C a1 => a1
>       --     x = someA :: a
>       -- but 'a1' is not equivalent to 'a', so it errors.
>   ()
>
> And so it says hey wait, a and a1 could be different types.  That is
> why you often see ghc referring to 'a1' or 'a0' in error messages,
> because when it infers a type it has to give a name to it in order to
> report on it.
>
> What ScopedTypeVariables does is allow you to specify that for the
> entire scope of this forall, 'a' in any type signature always refers
> to the same type.
>
> f :: forall a. C a => a -> ()
> f = undefined
> where
>   some :: a -- this is guaranteed to be the a from above.
>   some = undefined
>
>   somethingelse :: forall a. a -- this is a different a
>   somethingelse = undefined
>
> some :: a -- this toplevel a is of course also different.
> some = undefined
>
> So you could just go
> {-# LANGUAGE ScopedTypeVariables #-}
>
> f :: forall a. C a => a -> Int
> f a =
>   let
>      x :: a  -- now the a is the same a as above, so the constraint C
> a is understood.
>      x = someA
>   in 0
>
> I really love the ScopedTypeVariables extension, and so do a lot of
> other people.  I honestly think it should be on by default because
> the pitfalls of not having it on are a lot worse than the pitfalls of
> having it on.  The only pitfall I know of to having it on is that if
> you have a function with tons of lets and / or wheres, you might not
> notice you had used the type variable 'a' in two different
> incompatible places.
>
> Hopefully all this makes sense.
>
>
>
> On Thu, Dec 7, 2017 at 6:41 AM, Baa <[hidden email]> wrote:
>
> > Hello everyone!
> >
> > Suppose I have:
> >
> >   class C a where
> >     someA :: a
> >
> >   f :: C a => a -> Int
> >   f a =
> >     let x = someA :: a in -- BUG!!
> >       0
> >
> > BUG as I understand I due to `:: a` - this is another `a`, not the
> > same as in `f` singature. But seems that it's the same `a` if `f`
> > is the "method" of some instance. And such bug does not happen if I
> > return it, so my question
> > is how to create such `x` of type `a` in the body of the `f`? How
> > to use `a` anywhere in the body of `f`? Is it possible?
> >
> > I found a way if I change signature to `forall a. C a => a -> Int`.
> > But there
> > are another questions in the case:
> >
> >  - as I know all such params are under "forall" in Haskell
> > by-default. Seems
> >    it's not true?
> >  - in method body seems they are under "forall" but in simple
> > functions - not?
> >  - i'm not sure what exactly does this "forall", IMHO it unbounds
> > early bound
> >    type's variables (parameters) by typechecker, but how `a` can be
> > bound in the
> >    just begining of signature (where it occurs first time) ?!
> >
> > As for me, looks that w/o "forall" all `a`, `b`, `c`, etc in the
> > body of simple functions always are different types. But w/
> > "forall" Haskell typechecker
> > makes something like (on type-level):
> >
> >    let a = ANY-TYPE
> >    in
> >       ... here `a` can occur and will be bound to ANY-TYPE
> >
> > Where am I right and where am I wrong? :)
> >
> > ===
> > Best regards, Paul
> > _______________________________________________
> > Beginners mailing list
> > [hidden email]
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
> >

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners


_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
Baa
Reply | Threaded
Open this post in threaded view
|

Re: Little question about "forall"

Baa
> forall a. is just what what ScopedTypeVariables uses to ensure that
> local variables in the function with the same type variables are no
> longer free, and that they must adhere to the type signature of the
> encompassing scope.

Hmm, OK, so the extension analizes code/AST and finds a types which are
under "forall" and links them (to be exactly the same type at whole
scope).

Only open question here is: seems that "forall-by-default" is not
absilutely true :)

> My terminology is terrible, and I've probably made a mistake, but
> hopefully someone will correct me.

May be I'm not correctly here but Haskell-terminology IMHO is terrible
at whole: I found in mail-lists posts about it (that terms are
unsuccessful, confusing). As for me, after some Prolog experience I
understand what is unification, bound var and not-bound var
intuitively - it's clean terminology. So, GHC type-checker for me is
some kind of Prolog and if result is True (with all constaints and
types relations) then type-checking is passed. But terminology is
different and confuse me and I suppose other newbies too: I found
already "rigid", "free", "skolem", "bound", etc :-)

David, thanks a lot!!

===
Best regards, Paul


>
> On Thu, Dec 7, 2017 at 10:31 AM, Baa <[hidden email]> wrote:
>
> > Hello, David!
> >  
> > > But remember that in x, 'a' is not the same as the 'a' in f, so
> > > you  
> >
> > Exactly, and I often hit errors like "Can't match rigid type 'M a'
> > with rigid type 'M a1'"! So, the question comes down to "forall" and
> > "ScopedTypeVariables". Did I understand you correctly:
> >
> > this extension expands type-variable scope to whole function body.
> > But what sort of type vairables? Only under "forall ...", right ?
> >
> > And another question: type-variables under "forall" - they are
> > rigid? Or free? I can't understand the terminology. I thought early
> > that they are called "rigid", but in documentation of
> > "ScopedTypeVariables" extension they are called "free". IMHO symbol
> > ∀ means "unbound", so "free". But I often hit errors when GHC says
> > something about rigid, so I'm not sure - what is rigid? Bound?
> >
> > And last: why I need "forall a." in beginning of signature while
> > Haskell assumes "forall" for all type variables by default? Or I'm
> > not right here...
> >
> >  
> > > As to your original code, the only actual bug is that someA :: a
> > > is wrong. The actual type of someA is someA :: C a => a, so you
> > > could have written
> > >
> > > class C a where
> > >   someA :: a
> > >
> > > f :: C a => a -> Int
> > > f a =
> > >   let x :: C a => a
> > >       x = someA -- absolutely works
> > >   in 0
> > >
> > >
> > > But remember that in x, 'a' is not the same as the 'a' in f, so
> > > you might as well have written this
> > >
> > >   f :: C a => a -> Int
> > >   f a =
> > >     let x :: C b => b
> > >         x = someA -- also works
> > >     in 0
> > >
> > > This is how it works.  When you write
> > >
> > > f :: C a => a -> ()
> > > f =
> > >   let x = someA  -- without ':: a'
> > >   ()
> > >
> > > The problem is that by not giving an explicit type to x, ghc
> > > infers a type and for all intents and purposes it is as though
> > > you wrote
> > >
> > > f :: C a => a -> ()
> > > f =
> > >   let x :: C a1 => a1
> > >       x = someA
> > >       -- also  if you had written x = some :: a, it just means you
> > > effectively wrote
> > >       -- let x :: C a1 => a1
> > >       --     x = someA :: a
> > >       -- but 'a1' is not equivalent to 'a', so it errors.
> > >   ()
> > >
> > > And so it says hey wait, a and a1 could be different types.  That
> > > is why you often see ghc referring to 'a1' or 'a0' in error
> > > messages, because when it infers a type it has to give a name to
> > > it in order to report on it.
> > >
> > > What ScopedTypeVariables does is allow you to specify that for the
> > > entire scope of this forall, 'a' in any type signature always
> > > refers to the same type.
> > >
> > > f :: forall a. C a => a -> ()
> > > f = undefined
> > > where
> > >   some :: a -- this is guaranteed to be the a from above.
> > >   some = undefined
> > >
> > >   somethingelse :: forall a. a -- this is a different a
> > >   somethingelse = undefined
> > >
> > > some :: a -- this toplevel a is of course also different.
> > > some = undefined
> > >
> > > So you could just go
> > > {-# LANGUAGE ScopedTypeVariables #-}
> > >
> > > f :: forall a. C a => a -> Int
> > > f a =
> > >   let
> > >      x :: a  -- now the a is the same a as above, so the
> > > constraint C a is understood.
> > >      x = someA
> > >   in 0
> > >
> > > I really love the ScopedTypeVariables extension, and so do a lot
> > > of other people.  I honestly think it should be on by default
> > > because the pitfalls of not having it on are a lot worse than the
> > > pitfalls of having it on.  The only pitfall I know of to having
> > > it on is that if you have a function with tons of lets and / or
> > > wheres, you might not notice you had used the type variable 'a'
> > > in two different incompatible places.
> > >
> > > Hopefully all this makes sense.
> > >
> > >
> > >
> > > On Thu, Dec 7, 2017 at 6:41 AM, Baa <[hidden email]> wrote:
> > >  
> > > > Hello everyone!
> > > >
> > > > Suppose I have:
> > > >
> > > >   class C a where
> > > >     someA :: a
> > > >
> > > >   f :: C a => a -> Int
> > > >   f a =
> > > >     let x = someA :: a in -- BUG!!
> > > >       0
> > > >
> > > > BUG as I understand I due to `:: a` - this is another `a`, not
> > > > the same as in `f` singature. But seems that it's the same `a`
> > > > if `f` is the "method" of some instance. And such bug does not
> > > > happen if I return it, so my question
> > > > is how to create such `x` of type `a` in the body of the `f`?
> > > > How to use `a` anywhere in the body of `f`? Is it possible?
> > > >
> > > > I found a way if I change signature to `forall a. C a => a ->
> > > > Int`. But there
> > > > are another questions in the case:
> > > >
> > > >  - as I know all such params are under "forall" in Haskell
> > > > by-default. Seems
> > > >    it's not true?
> > > >  - in method body seems they are under "forall" but in simple
> > > > functions - not?
> > > >  - i'm not sure what exactly does this "forall", IMHO it
> > > > unbounds early bound
> > > >    type's variables (parameters) by typechecker, but how `a`
> > > > can be bound in the
> > > >    just begining of signature (where it occurs first time) ?!
> > > >
> > > > As for me, looks that w/o "forall" all `a`, `b`, `c`, etc in the
> > > > body of simple functions always are different types. But w/
> > > > "forall" Haskell typechecker
> > > > makes something like (on type-level):
> > > >
> > > >    let a = ANY-TYPE
> > > >    in
> > > >       ... here `a` can occur and will be bound to ANY-TYPE
> > > >
> > > > Where am I right and where am I wrong? :)
> > > >
> > > > ===
> > > > Best regards, Paul
> > > > _______________________________________________
> > > > Beginners mailing list
> > > > [hidden email]
> > > > http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
> > > >  
> >
> > _______________________________________________
> > Beginners mailing list
> > [hidden email]
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
> >  

_______________________________________________
Beginners mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners