Re: [Haskell-beginners] Little question about "forall"

7 Dec 2017

      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  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
Beginners@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners