[Haskell-beginners] Little question about "forall"
Baa
aquagnu at gmail.com
Thu Dec 7 15:31:54 UTC 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 <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
> >
More information about the Beginners
mailing list