16

I'm pretty sure everyone is familiar with generic methods of the form:

T DoSomething<T>(T item)

This function is also called parametrically polymorphic (PP), specifically rank-1 PP.

Let's say this method can be represented using a function object of the form:

<T> : T -> T

That is, <T> means it takes one type parameter, and T -> T means that it takes one parameter of type T and returns a value of the same type.

Then the following would be a rank-2 PP function:

(<T> : T -> T) -> int 

The function takes no type parameters itself, but takes a function which takes a type parameter. You can continue this iteratively, making the nesting deeper and deeper, getting PP of higher and higher rank.

This feature is really rare among programming languages. Even Haskell doesn't allow it by default.

Is it useful? Can it describe behaviors that are difficult to describe otherwise?

Also, what does it mean for something to be impredicative? (in this context)

  • 1
    Interestingly, TypeScript is one mainstream language with full rank-n PP support. For example, the following is valid TypeScript code: let sdff = (g : (f : <T> (e : T) => void) => void) => {} – GregRos Oct 19 '16 at 15:25
11

In general, you use higher-rank polymorphism when you want the callee to be able to select the value of a type parameter, rather than the caller. For example:

f :: (forall a. Show a => a -> Int) -> (Int, Int)
f g = (g "one", g 2)

Any function g that I pass to this f must be able to give me an Int from a value of some type, where the only thing g knows about that type is that it has an instance of Show. So these are kosher:

f (length . show)
f (const 42)

But these are not:

f length
f succ

One particularly useful application is in using the scoping of types to enforce the scoping of values. Suppose we have an object of type Action<T>, representing an action we can run to produce a result of type T, such as a future or callback.

T runAction<T>(Action<T>)

runAction :: forall a. Action a -> a

Now, suppose that we also have an Action that can allocate Resource<T> objects:

Action<Resource<T>> newResource<T>(T)

newResource :: forall a. a -> Action (Resource a)

We want to enforce that those resources are only used inside the Action where they were created, and not shared between different actions or different runs of the same action, so that actions are deterministic and repeatable.

We can use higher-ranked types to accomplish this by adding a parameter S to the Resource and Action types, which is totally abstract—it represents the “scope” of the Action. Now our signatures are:

T run<T>(<S> Action<S, T>)
Action<S, Resource<S, T>> newResource<T>(T)

runAction :: forall a. (forall s. Action s a) -> a
newResource :: forall s a. a -> Action s (Resource s a)

Now when we give runAction an Action<S, T>, we are assured that because the “scope” parameter S is fully polymorphic, it cannot escape the body of runAction—so any value of a type that uses S such as Resource<S, int> likewise cannot escape!

(In Haskell, this is known as the ST monad, where runAction is called runST, Resource is called STRef, and newResource is called newSTRef.)

  • The ST monad is a very interesting example. Can you give some more examples of when higher-rank polymorphism would be useful? – GregRos Mar 23 '15 at 13:01
  • @GregRos: It’s also handy with existentials. In Haxl, we had an existential like data Fetch d = forall a. Fetch (d a) (MVar a), which is a pair of a request to a data source d and a slot in which to store the result. The result and slot must have matching types, but that type is hidden, so you can have a heterogeneous list of requests to the same data source. Now you can use higher-rank polymorphism to write a function that fetches all requests, given a function that fetches one: fetch :: (forall a. d a -> IO a) -> [Fetch d] -> IO (). – Jon Purdy Mar 23 '15 at 18:52
8

Higher rank polymorphism is extremely useful. In System F (the core language of typed FP languages you're familiar with), this is essential for admitting "typed Church encodings" which is actually how System F does programming. Without these, system F is completely useless.

In System F, we define numbers as

Nat = forall c. (c -> c) -> c -> c

Addition has the type

plus : Nat -> Nat -> Nat
plus l r = Λ t. λ (s : t -> t). λ (z : t). l s (r s z)

which is a higher rank type (the forall c. appears inside those arrows).

This comes up in other places too. For example, if you want to indicate that a computation is a proper continuation passing style (google "codensity haskell") then you'd right this as

type CPSed A = forall c. (A -> c) -> c

Even talking about an uninhabited type in System F requires higher rank polymorphism

type Void = forall a. a 

The long and short of this, writing a function in a pure type system (System F, CoC) requires higher rank polymorphism if we want to deal with any interesting data.

In System F in particular, these encodings need to be "impredicative". This means that a forall a. quantifies over absolutely all types. This critically includes the very type we're defining. In forall a. a that a could actually stand for forall a. a again! In languages like ML this isn't the case, they're said to be "predicative" since a type variable quantifies only over the set of types without quantifiers (called monotypes). Our definition of plus required impredicativity as well because we instantiated the c in l : Nat to be Nat!

Finally, I'd like to mention one last reason where you'd like both impredicativity and higher rank polymorphism even in a language with arbitrarily recursive types (unlike System F). In Haskell, there's a monad for effects called the "state thread monad". The idea is that the state thread monad lets you mutate things but requires to escape it that your result not depend on anything mutable. This means that ST computations are observably pure. To enforce this requirement we use higher rank polymorphism

runST :: forall a. (forall s. ST s a) -> a

Here by ensuring that a is bound outside the scope where we introduce s, we know that a stands for a wellformed type which doesn't rely on s. We use s to parameritize all the mutable things in that particular state thread so we know that a is independent of mutable things and thus that nothing escapes the scope of that ST computation! A wonderful example of using types to rule out ill-formed programs.

By the way, if you're interested in learning about type theory I'd suggest investing in a good book or two. It's hard to learn this stuff in bits and pieces. I'd suggest one of Pierce or Harper's books on PL theory in general (and some elements of type theory). The book "Advanced topics in types and programming languages" also covers a good amount of type theory. Finally "Programming in Martin Lof's type theory" is a very good exposition into the intensional type theory Martin Lof outlined.

  • Thank you for your recommendations. I'll look them up. The topic is really interesting, and I wish some more advanced type system concepts would be adopted by more programming languages. They give you a lot more expressive power. – GregRos Mar 23 '15 at 13:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.