Understanding the difference between two Haskell signals using forall

This article has a function with the following signature:

vreplicate :: forall an . SNatI n => a -> Vec an 

What is the difference between this signature and those who do not have forall :

 vreplicate :: SNatI n => a -> Vec an 

? I got the impression that without forall it implicitly means the same thing as before forall , which names all type variables.

+6
source share
1 answer

There are two important cases where the inclusion of forall matters. Firstly, the location of forall can change the value of the type - if it goes to the left of the arrow, this means that the function argument is "more polymorphic" than otherwise. This distinction is fundamental; however, this does not seem to apply here.

The second difference is syntactic (and not fundamental), namely: with ScopedTypeVariables variables associated with a forall open the input area, while the variables implicitly connected without forall do not. Thus, in the vreplicate body, vreplicate can use variables of type a and n and be sure that they are of the same types as in the vreplicate signature. Without forall (or without ScopedTypeVariables ), using a and n in the body of vreplicate will result in new, universally quantified variables, and it would be the responsibility of the programmer to combine them with types in the vreplicate signature, if desired. More information is available in the documentation .

Without carefully reading the paper, I cannot be sure, but I would strongly say that the latter is happening here.

+10
source

All Articles