hello,
i have been following the evolution of haskell for about 2 years now in my spare
time, but haven't had time to really get into haskell programming. so i am not
an expert or anything. i do not see the need for the "forall" quantifier to be written
explicitly however, and i quite like the way haskell currently deals with the
situation.
here is how i think about functions and their types. i would be glad if someone points
out any mistakes i made, as (as i wrote above) i am by no means an advanced haskell
user and
am still learning. anyways here we go:
1) f :: Int f is of type integer
2) f :: Int -> Int f is a function, which given an integer produces and integer
3) f :: a f is of types 'a', where 'a' denotes some type
(since we haven't imposed any restrictions on 'a' it can be
any type,
so the implicit universal quantification done by haskell makes
sense)
(would bottom be of this type?)
4) f :: a -> Int f is a function, which given an object of some type 'a'
returns an integer
(i.e. f does not assume anything about what its parameter
might be,
so f works on paramters of any type)
5) f :: a -> a f is a function, which given an object of some type 'a'
returns
an object of the *same* type 'a' 9again no restrictions on
what 'a' might be)
6) f :: (Eq a) => a f is of type 'a', but 'a' is of class Eq, so now we have
imposed
some restrictions on the types of which f can be, i.e. any
type,
which can deal with equality
7) f :: (Eq a) => a -> Int
is a function, which assumes that its parameter can deal with
equality
(so the function can compare the parameter to things for
equality).
however it does not assume anything else about its parameter.
etc...
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 is i think what the big discussion was all about, here are the solutions i can
see:
1.1 this is an ivalid expressions, but then we get a more verbose version of what we
have at the moment, is it worthed?
1.2 it is a valid expression and is the same as f :: forall a.a , i.e. it is
implicitly universally
quantified by haskell, so f :: forall a.a and f :: a is really the same thing. the
probelm with
this is that there is more than one way to write the same thing and will probably
confuse the issue even more.
1.3 it is a valid expression, but has some other meaning, but what?
1.4 f is a type variable :-) . i just tought of this now, and i think this *really*
will confuse things
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)
but what about:
f :: forall a of_class Eq. forall a.a
now i think f :: forall a.a
something like this may happen in a large type expressions (and with 'forall' they
will become quite large),
when one renames variables, and accidentally a type variable might get bounded by the
wrong quantifier.
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)
3.1 now as far as i understand BinaryTree is of kind * -> * (ie a type constructor),
which is different to *
would the 'forall' for types range over * only, or both?
4) why is 'forall' needed? could someone plese give an example.
thanks
yavor
--
iavor s. diatchki
university of cape town
email: [EMAIL PROTECTED]
web: http://www.cs.uct.ac.za/~idiatchk
