[Haskell-cafe] Aren't type system extensions fun?

[Thomas Davie]

On 26 May 2008, at 23:02, Andrew Coppin wrote:

> Haskell 98 provides a simple and clean type system, which I feel I  
> understand very well.
>
> GHC provides a vast zoo of strange and perplexing type system  
> extensions, which I don't understand at all. (Well, some of it is  
> simple enough - e.g., multiparameter type classes. But GADTs? FDs?  
> ATs? Hmm...)
>
> Anyway, it seems there is a large set of such type system extensions  
> that involve writing "forall" all over the place. I have by now more  
> or less managed to comprehend the fact that
>
> data Thing = forall x. Thing x
>
> allows a type variable to appear on the RHS that is *not* present on  
> the LHS, thus "hiding" the type of something inside the structure.  
> And for some reason, they call this "existential  
> quantification" [which I can't spell never mind pronounce].
>
> Today I was reading a potentially interesting paper, and I stumbled  
> across something referred to as a "rank-2 type". Specifically,
>
> class Typable x => Term x where
>   gmapT :: (forall y. Term y => y -> y) -> x -> x
>
> At this point, I am at a complete loss as to how this is any  
> different from
>
> gmapT :: Term y => (y -> y) -> x -> x
>
> Can anybody enlighten me?
>
> This is probably the first real use I've ever seen of so-called  
> rank-2 types, and I'm curios to know why people think they need to  
> exist. [Obviously when somebody vastly more intelligent than me says  
> something is necessary, they probably know something I don't...]
>
> At this point, I don't think I even wanna *know* what the hell a  
> rank-N type is... o_O

This is perhaps best explained with an example of something that can  
be typed with rank-2 types, but can't be typed otherwise:

main = f id 4

f g n = (g g) n

We note that the same instance of id must be made to have both the  
type (Int -> Int) and ((Int -> Int) -> (Int -> Int)) at the same  
time.  Rank 2 types allows us to do this.

Bob