Fri, 19 May 2000 19:47:38 +0200, Iavor Diatchki <[EMAIL PROTECTED]> pisze:
> i do not see the need for the "forall" quantifier to be written
> explicitly however,
It is needed when the quantifier is inside a function argument,
to spell the difference between
f1 :: forall a. ([a] -> [a]) -> [a] -> [a]
and
f2 :: (forall a. [a] -> [a]) -> [a] -> [a]
the second being the same as
f2 :: forall a. (forall b. [b] -> [b]) -> [a] -> [a]
What is the difference?
f1 cannot assume anything about "a". It only knows that the function
passed as the first parameter can be applied to a value of the same
type as the second parameter, yielding the same type, and that this
type is a list of something.
f2 can use its first parameter for any type "a" it chooses, even
for different types in different places. For example to apply it to
[False,False,True] and check if the first element of the result
is True.
When calling f1, we can pass it a function [Int]->[Int] and a list of
Ints, or similarly for another type. OTOH as the first argument of
f2 we must pass a polymorphic function that will accept any list,
independently of the second argument. For example id, reverse,
List.cycle, (take 5) and (\x -> x++x) are OK, but sort is not.
I am generally talking about Haskell with GHC and Hugs extensions.
Standard Haskell does not have explicit foralls, one cannot define
a function like f2 in it, and one cannot write a type signature
depending on type variables that are bound outside.
forall is also used in local universal quantification and local
existential quantification in data types - both are language
extensions. I will not write about them here.
> and i quite like the way haskell currently deals with the situation.
Me too. Since in 99% of cases the quantifier is at the top of the
signature, I like having it implicit in those cases, although it
causes troubles (see below).
Some people get confused, but IMHO they would get confused even
when explicit forall was mandatory - the problem is in them, not in
Haskell's syntax.
> 3) f :: a f is of types 'a', where 'a' denotes some type
This descripton looks unclear for me. I hope you meant that f can be
used as a value of any type the caller chooses.
So the caller can use f as a String. OTOH there is no much freedom
in implementation of f, The only choice is bottom, and it can only
be spelt differently:
f = f
f = undefined
f = error "foo"
They are theoretically the same, but in practice their effects are
different.
> 4) f :: a -> Int f is a function, which given an object of some type 'a'
>returns an integer
In other words, the caller can choose a type for "a" and use "f" as
the type "a -> Int". This does not explain the intuitive meaning of
"f" so well, but allows uniform understanding of all polymorphic types.
> so my questions are:
>
> 1) what would it mean if one writes f :: a (in general: how does
> one think of unbound type variables)?
This type signature in program source means the same as "f :: forall a. a".
Except two cases:
- In a method signature inside class declaration, when "a" was in the
class head. It means that f will have the type "forall a. Class a => a".
- With GHC and Hugs extension of pattern type signatures, it means "f :: a"
(for "a" bound outside) if "a" was indeed bound outside by a pattern
type signature. Example:
g :: b -> b -- The name "b" here is independent of all other names,
g (x::a) = -- but the name "a" defined here can be used below:
...
where
f1 :: a -- The type of f1 is the same as of g's argument.
-- It is not implicitly quantified by forall here!
f2 :: b -- The type of f2 is forall b. b.
-- This is the same type as forall z. z, etc.
f3 :: forall a. a -- The type of f3 is the same as of f2.
-- Thus forall can be used to be sure that we introduce
-- a new type variable, and not mention one bound outside.
When you use "f :: a" in an expression, not in a type signature among
declarations, in GHC these rules apply too. In standard Haskell the
second rule obviously does not apply, because there are no pattern type
signatures, but the first does not apply either, which is not very
obvious (one has a chance to write such expression in the default
implementation of a method). In Hugs these rules don't apply for
types in expressions, but maybe they will, I don't know.
> 2) how will one write constraints on the types (e.g. as in
> (7) above)? i presume that since with the 'forall' we get the
> whole scoping thing, so the constraints have to be written per
> quantifier, i.e. something like:
>
> f:: forall a of_class Eq. (a -> Int)
No. The context is always written just inside forall, no matter if
forall is explicit or not:
f :: forall a. Eq a => a -> Int
Similarly for local quantification:
g :: Ord b => (forall a. Eq a => [a] -> [a]) -> [b] -> [b]
It does not make sense to write context together with forall when we
have multiparameter classes, another language extension.
> 3) is 'forall' going to be used at the type level as well, i.e. would one have to
>write:
> data forall a. BinaryTree a = Empty | BT a (BinaryTree a) (BinaryTree a)
I haven't heard of this (and don't see a reason).
--
__("< Marcin Kowalczyk * [EMAIL PROTECTED] http://qrczak.ids.net.pl/
\__/ GCS/M d- s+:-- a23 C+++$ UL++>++++$ P+++ L++>++++$ E-
^^ W++ N+++ o? K? w(---) O? M- V? PS-- PE++ Y? PGP+ t
QRCZAK 5? X- R tv-- b+>++ DI D- G+ e>++++ h! r--%>++ y-
