[Haskell-beginners] 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 <aquagnu at gmail.com> 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 at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
> >