[Haskell-beginners] Little question about "forall"
Baa
aquagnu at gmail.com
Thu Dec 7 16:12:48 UTC 2017
> 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 <aquagnu at gmail.com> 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 <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
> > > >
> >
> > _______________________________________________
> > Beginners mailing list
> > Beginners at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
> >
More information about the Beginners
mailing list