Dear All,
Please could somebody post a short, plain text summary of the discussion
in this thread? The recent exchanges have been long and involved, which
has made it impossible for me (and other busy onlookers too, I suspect)
to keep up. Without such a summary, I think that this thread may be
reaching the end of it's useful life, at least for the main Haskell list.
I make these suggestions because I sense that there is a lot of confusion,
misunderstanding, and talking at cross purposes, and because I'm not at
all sure that the current discussions are on course to reach a conclusion.
I will make one brief attempt (although it has turned out to be less
brief than I'd intended) to try and clarify some of the issues, based
on the following comment that I noticed in a recent message:
| And that's the reason why I should find it weird if in
| Haskell 98+ one would distinguish between
|
| a -> a and [forall a. a -> a]
Without the context that a good summary would provide, this sentence makes
little sense. Going back even to the presentation of the core ML type
system by Damas and Milner in 1982, there is a very significant difference
between these two. Moreover, a system in which there was no distinction
between the two types would not even be sound. For example, in the
following core ML/Haskell fragment, the definition of g can be assigned
any type of the form a -> a, but it cannot be given a type (scheme) of the
form (forall a. a -> a):
\x -> let g = (\y -> if True then x else y)
in x
I would therefore find it extremely "weird" if any language claiming the
Damas and Milner type system as an ancestor did not distinguish between
a -> a and (forall a. a -> a).
I suspect however, that the confusion here comes from the notation that
Haskell uses in type signature declarations such as:
myId :: a -> a
myId x = x
Here, the declared type "a -> a" actually corresponds to (forall a. a -> a)
in the underlying formal type system. [Note that I use "quotes" to
distinguish types in the syntax of Haskell from types in the underlying
system.] The type (a -> a) is also present in the underlying formal
system, but there is no way to write this type in the current syntax of
Haskell.
Currently, and going beyond the Haskell standard, Hugs does allow you to
use "a -> a" to mean (a -> a), but only in the presence of an explicitly
scoped type variable, as in:
f (x::a) = let g :: a -> a
g = (\y -> if True then x else y)
in x
Remove the "::a" part on the left hand side, and the occurrence of "a -> a"
on the right will then be interpreted following the standard Haskell rules
as (forall a. a -> a), and that will trigger a type error because this is
not a correct type for g.
I hope that this helps!
All the best,
Mark
