Hi Johannes,
Johannes Waldmann wrote:
I absolutely dislike it when I have to jump through hoops
to declare types in the most correct way, and in the most natural places.
reverse :: forall (a :: *) . [a] -> [a]
\ (xs :: [Bool]) -> ...
All of this just because it seemed, at some time,
a clever idea to allow the programmer to omit quantifiers?
As I understand it, in ML, it seemed to be a clever idea to not have
type signatures at all.
From the type-theoretic point of view, I guess this is related to your
view of what a polymorphic function is. One view says that a polymorphic
function is qualitatively different from each of its instances and that
forall is a type constructor, so there should be introduction and
elimination forms for terms of that type. Instantiation and
generalization are explicit operations with computational content, that
is, they have some effect at runtime. This view leads to System F with
its explicit type abstraction and type application forms.
The other view says that a polymorphic function is the union of all of
its instances and that instantation and generalization are implicit,
structural operations that have no computational content, that is, they
do not affect what happens at runtime. This view leads to ML with its
very implicit handling of polymorphism.
It seems that in Haskell, we started with the ML-ish view that
polymorphism is an implicit, structural thing, but we moved further and
further towards the System-F-ish view that polymorphism is an explicit,
computational thing. A good indicator for this is the Monomorphism
restriction, which supposedly helps beginners to cope with the
computational effects of polymorphism. So apparently, there *are* such
effects. Another indicator is the type classes in that they attach
further computational content with type variables.
Tillmann
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
