Are Rank2Types/RankNTypes practical without polytype variables?

Question

Since type variables cannot hold poly-types, it seems that with Rank*Types we cannot re-use existing functions because of their monotype restriction.

For example, we cannot use the function (.) when the intermediate type is a polytype. We are forced to re-implement (.) at the spot. This is of course trivial for (.) but a problem for more substantial bodies of code.

I also think making ((f . g) x) not equivalent to (f (g x)) a severe blow to referential transparency and its benefits.

It seems to me to be a show-stopper issue, and seems to make the Rank*Types extensions almost impractical for wide-spread use.

Am I missing something? Is there a plan to make Rank*Types interact better with the rest of the type-system?

EDIT: How can you make the types of (runST . forever) work out?

Answer 1

The most recent proposal for Rank-N types is Don's linked FPH paper. In my opinion it's also the nicest of the bunch. The main goal of all these systems is to require as few type annotations as possible. The problem is that when going from Hindley/Milner to System F we lose principal types and type inference becomes undecidable – hence the need for type annotations.

The basic idea of the "boxy types" work is to propagate type annotations as far as possible. The type checker switches between type checking and type inference mode and hopefully no more annotations are required. The downside here is that whether or not a type annotation is required is hard to explain because it depends on implementation details.

Remy's MLF system is so far the nicest proposal; it requires the least amount of type annotations and is stable under many code transformations. The problem is that it extends the type system. The following standard example illustrates this:

choose :: forall a. a -> a -> a
id :: forall b. b -> b

choose id :: forall c. (c -> c) -> (c -> c)
choose id :: (forall c. c -> c) -> (forall c. c -> c)

Both the above types are admissable in System F. The first one is the standard Hindley/Milner type and uses predicative instantiation, the second one uses impredicative instantiation. Neither type is more general than the other, so type inference would have to guess which type the user wants, and that is usually a bad idea.

MLF instead extends System F with bounded quantification. The principal (= most general) type for the above example would be:

choose id :: forall (a < forall b. b -> b). a -> a

You can read this as "choose id has type a to a where a must be an instance of forall b. b -> b".

Interestingly, this alone is no more powerful than standard Hindley/Milner. MLF therefore also allows rigid quantification. The following two types are equivalent:

(forall b. b -> b) -> (forall b. b -> b)
forall (a = forall b. b -> b). a -> a

Rigid quantification is introduced by type annotations and the technical details are indeed quite complicated. The upside is that MLF only needs very few type annotations and there is a simple rule for when they are needed. The downsides are:

• Types can become harder to read, because the right hand side of '<' can contain further nested quantifications.

• Until recently no explicitly typed variant of MLF existed. This is important for typed compiler transformations (like GHC does). Part 3 of Boris Yakobowski's PhD thesis has a first attempt at such a variant. (Parts 1 & 2 are also interesting; they describe a more intuitive representation of MLF via "Graphical Types".)

Coming back to FPH, its basic idea is to use MLF techniques internally, but to require type annotations on let bindings. If you only want the Hindley/Milner type, then no annotations are necessary. If you want a higher-rank type, you need to specify the requested type, but only at the let (or top-level) binding.

FPH (like MLF) supports impredicative instantiation, so I don't think your issue applies. It should therefore have no issue typing your f . g expression above. However, FPH hasn't been implemented in GHC yet and most likely won't be. The difficulties come from the interaction with equality coercions (and possibly type class constraints). I'm not sure what the latest status is, but I heard that SPJ wants to move away from impredicativity. All that expressive power comes at a cost, and so far no affordable and all-accompanying solution has been found.

Answer 2

Is there a plan to make Rank*Types interact better with the rest of the type-system?

Given how common the ST monad is, at least Rank2 types are common enough to be evidence to the contrary. However, you might look at the "sexy/boxy types" series of papers, for how approaches to making arbitrary rank polymorphism play better with others.

FPH : First-class Polymorphism for Haskell, Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones, submitted to ICFP 2008.

See also -XImpredicativeTypes -- which interestingly, is slated for deprecation!

Answer 3

About ImpredicativeTypes: that doesn't actually make a difference (I'm relatively sure) to peaker's question. That extension has to do with datatypes. For instance, GHC will tell you that:

Maybe :: * -> *
(forall a. a -> a) :: *

However, this is sort of a lie. It's true in an impredicative system, and in such a system, you can write:

Maybe (forall a. a -> a) :: *

and it will work fine. That is what ImpredicativeTypes enables. Without the extension, the appropriate way to think about this is:

Maybe :: *m -> *m
(forall a :: *m. a -> a) :: *p

and thus there is a kind mismatch when you try to form the application above.

GHC is fairly inconsistent on the impredicativity front, though. For instance, the type for id I gave above would be:

id :: (forall a :: *m. a -> a)

but GHC will gladly accept the annotation (with RankNTypes enabled, but not ImpredicativeTypes):

id :: (forall a. a -> a) -> (forall a. a -> a)

even though forall a. a -> a is not a monotype. So, it will allow impredicative instantiation of quantified variables that are used only with (->) if you annotate as such. But it won't do it itself, I guess, which leads to the runST $ ... problems. That used to be solved with an ad-hoc instantiation rule (the details of which I was never particularly clear on), but that rule was removed not long after it was added.