Fri, 19 May 2000 14:48:24 +0200, Jan Brosius <[EMAIL PROTECTED]> pisze:
> On the other hand someone's remark and about the meaning Haskell gives to
> these two types and I wonder since today if one means by a -> a a type
> indication to be understood as a function having this type signature
> means that the function is only defined for some a 's and by forall a.
> a -> a a type indication to be understood
> as a function that is really defined for ALL type's a .
Not quite. Let's have an example:
rep:: Int -> (a -> a) -> (a -> a)
rep 0 f = id
rep n f = f . rep (n-1) f
What is the type of f inside rep?
It is not "forall a. a -> a". If it was, one could write
rep 0 f = if f True then id else undefined
and it would not have any semantics, because one can pass the function
"\x -> x+1" as the second argument of rep.
It is not "exists a. a -> a". If it was, one could not write the
second equation for rep, because the function "not" should have the
type "exists a. a -> a" too, and it clearly cannot be used instead of
"f" in the second equation. In other words, the fact that exists some
type "a" for which "f" has the type "a -> a" does not guarantee that
this is exacly this "a" that is needed here.
So what is the type of f?
Answer: it is "a -> a", where "a" is bound by the fact that rep is
polymorphic. It is bound by an implicit kind-of-lambda over types
at the definition of rep.
You cannot write such type in a standard Haskell program, i.e. you
cannot change "f" in the body of rep by "(f :: sometype)", for any type
expression "sometype". But this type, depending on instantiation of a
polymorphic function it is used in, clearly exists, has well-defined
semantics, and is extremely useful.
> I am well aware that the predicates (I would prefer to speak about
> functional relations) Free ( ) and Variable( ) are NOT IMPLEMENTED
> yet , so up to now these predicates serve only the purpose of an
> additional documentation ;
They don't have any semantics defined yet. I mean not informal
explanation what they mean, but how they fit into the type system
of Haskell, what are the typing rules.
I'm afraid it cannot be done in any useful way.
> But I think they might be useful.
> E.g. let's trying to say that instead of the function
>
> pr2:: (a, b) -> b
> pr2 (x,y) = y
>
> I wanted a slightly differing function
>
> pr2':: forall a. [forall b `notin Free(a) . (a,b) -> b]
> pr2' (x,y) = y
What do you gain by the restriction of type of pr2', compared to
pr2? How can the body of a function make use of the restriction? If it
cannot, I don't see why to complicate the type system by introducing
useless constructs.
But first, we must know what it means at all.
> With the above I filter out all arguments having a type of the form
> (a, T(a)) ;
f:: forall c. c -> [c]
f y = let g x = pr2' (x, y) in ...
Does the above compile when we replace "..." with something of the
right type (e.g. []), and if so, what is the inferred type of g as
seen inside "..."?
--
__("< 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-
