Applications of polymorphic recursion

Sometimes you want encode some constraints in types, so that they are enforced at compile time.

For instance, a complete binary tree can be defined as

data CTree a = Tree a | Dup (CTree (a,a))

example :: CTree Int
example = Dup . Dup . Tree $ ((1,2),(3,4))

The type will prevent non complete trees like ((1,2),3) to be stored inside, enforcing the invariant.

Okasaki's book shows many of such examples.

If one then wants to operate on such trees, polymorphic recursion is needed. Writing a function which computes the height of a tree, sums all the numbers in a CTree Int, or a generic map or fold requires polymorphic recursion.

Now, it is not terribly frequent to need/want such polymorphically recursive types. Still, they are nice to have.

In my personal opinion, monomorphisation is a bit unsatisfactory not only because it prevents polymorphic recursion, but because it requires to compile the polymorphic code once for every type it is used at. In Haskell or Java, using Maybe Int, Maybe String, Maybe Bool does not cause the Maybe-related functions to be compiled thrice and appear thrice in the final object code. In C++, this happens, bloating the object code. It is true, though, that in C++ this allows more efficient specializations to be used (e.g. std::vector<bool> can be implemented with a bitvector). This further enables C++'s SFINAE, etc. Still, I think I prefer it when the polymorphic code is compiled once, and type checked once -- after which it is guaranteed to be type safe a all types.

Here’s one example close to my work that I think generalises fairly well: in a concatenative language, that is, a language built on composing functions that operate on a shared program state such as a stack, all functions are polymorphic with respect to the part of the stack they don’t touch, all recursion is polymorphic recursion, and moreover all higher-order functions are also higher-rank. For instance, the type of map in such a language might be:

∀αβσ. σ × List α × (∀τ. τ × α → τ × β) → σ × List β

Where × is a left-associative product type with a stack-kinded type on the left and a value-kinded type on the right, σ and τ are stack-kinded type variables, and α and β are value-kinded type variables. map can be called on any program state σ as long as it has a List of αs and a function from αs to βs on top, like:

"ignored" [ 1 2 3 ] { succ show } map
=
"ignored" [ "2" "3" "4" ]

There’s polymorphic recursion here because map calls itself recursively on different instantiations of σ (i.e., different types of “rest of the stack”):

-- σ = Bottom × String
"ignored"           [ 1 2 3 ] { succ show } map
"ignored" 1 succ show [ 2 3 ] { succ show } map cons

-- σ = Bottom × String × String
"ignored" "2"           [ 2 3 ] { succ show } map cons
"ignored" "2" 2 succ show [ 3 ] { succ show } map cons cons

-- σ = Bottom × String × String × String
"ignored" "2" "3"           [ 3 ] { succ show } map cons cons
"ignored" "2" "3" 3 succ show [ ] { succ show } map cons cons cons

-- σ = Bottom × String × String × String × String
"ignored" "2" "3" "4" [ ] { succ show } map cons cons cons
"ignored" "2" "3" "4" [ ] cons cons cons
"ignored" "2" "3" [ "4" ] cons cons
"ignored" "2" [ "3" "4" ] cons
"ignored" [ "2" "3" "4" ]

And the functional argument of map needs to be higher-rank because it’s called on different stack types as well (different instantiations of τ).

In order to do this without polymorphic recursion, you would need an additional stack or local variables in which to place the intermediate results of map to get them “out of the way” so that all recursive calls take place on the same type of stack. This has implications for how functional languages can be compiled to e.g. typed combinator machines: with polymorphic recursion you can preserve safety while keeping the virtual machine simple.

The general form of this is that you have a recursive function which is polymorphic over part of a data structure, such as the initial elements of an HList or a subset of a polymorphic record.

And as @chi has already mentioned, the main instance where you need polymorphic recursion at the function level in Haskell is when you have polymorphic recursion at the type level, such as:

data Nest a = Nest a (Nest [a]) | Nil

example = Nest 1 $ Nest [1, 2] $ Nest [[1, 2], [3, 4]] Nil

A recursive function over such a type is always polymorphically recursive, since the type parameter changes with each recursive call.

Haskell requires type signatures for such functions, but apart from the types, mechanically there’s no difference between recursion and polymorphic recursion. You can write a polymorphic fixed-point operator if you have a secondary newtype that hides the polymorphism:

newtype Forall f = Abstract { instantiate :: forall a. f a }

fix' :: forall f. ((forall a. f a) -> (forall a. f a)) -> (forall a. f a)
fix' f = instantiate (fix (\x -> Abstract (f (instantiate x))))

Without all the wrapping & unwrapping ceremony, this is the same as fix' f = fix f.

This is also the reason that polymorphic recursion doesn’t need to result in a blowup of instantiations of a function—even if the function is specialised in its value-kinded type parameters, it’s “fully polymorphic” in the recursive parameter, so it doesn’t manipulate it at all, and thus only needs a single compiled representation.

I can share a real example I was using in my project.

Long story short, I have a data structure TypeRepMap where I store types as the keys and this type matches the type of the corresponding value.

For benchmarking my library I needed to make a list of 1000 types to check how fast lookup in this data structure works. And here comes the polymorphic recursion.

To do so I introduced the following data types as type-level natural numbers:

data Z
data S a

Using these data types I was able to implement the function which builds TypeRepMap of the desired size.

buildBigMap :: forall a . Typeable a 
            => Int 
            -> Proxy a 
            -> TypeRepMap 
            -> TypeRepMap
buildBigMap 1 x = insert x
buildBigMap n x = insert x . buildBigMap (n - 1) (Proxy @(S a))

so when I run buildBigMap with size n and Proxy a then it calls itself recursively with n - 1 and Proxy (S a) at each step, so the types are growing on each step.