[Haskell-cafe] Haskell is a declarative language? Let's see how easy it is to declare types of things.

[Tillmann Rendel]

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