Understanding a Complicated Type Signature

Question

I need help understanding this type signature which is from the Thrist package.

import Prelude hiding ((.), id)
import Control.Category
import Data.Monoid
import Control.Arrow
import Control.Monad

foldlThirst :: (forall j k . (a +> j) -> (j ~> k) -> (a +> k))  
               -> (a +> b) 
               -> Thrist (~>) b c  
               -> (a +> c)

I am confused about several things.

First what are the +> and ~> symbols? Where are they documented and what are they called?

But my confusion does stop there. I realize that the quantification is describing the threading of types of the Thrist, but I am not sure if is describing a relationship that holds for the first argument, or the whole function, or who knows...

In othercases where I have seen existential quantification, the phrase ends with a period, but here it ends with ->, is that significant?

Answer 1

First what are the +> and ~> symbols? Where are they documented and what are they called?

They're infix identifiers, just like if you used them as the name of a function. By the same token, being equivalent to lowercase identifiers (in contrast to operators beginning with : which are equivalent to upper-case alphanumeric identifiers), in a type signature they're simply type variables. In other words, it's equivalent to this:

(forall j k . (f a j) -> (g j k) -> (f a k)) 
  -> etc . . .

But my confusion does stop there. I realize that the quantification is describing the threading of types of the Thrist, but I am not sure if is describing a relationship that holds for the first argument, or the whole function, or who knows...

Explicit quantifiers are scoped only within enclosing parentheses, or to the end of the expression. In this case, they describe only the first argument, because the type variables introduced are only in scope for that argument.

In this case, it just means that the function given as the first argument must be fully polymorphic in those types. As an example, a function whose type signature starts with (a -> a) -> ... could be given not as its first argument, unifying a with Bool. In contrast, if the type signature started with (forall a. a -> a) -> ... it would require a function that works for all possible types a, the only such function being id.