Applications of polymorphic recursion

Question

One limitation of implementing polymorphism in a language via monomorphisation (and monomorphisation only) is that you lose the ability to support polymorphic recursion (e.g. see rust-lang #4287).

What are some compelling use cases for supporting polymorphic recursion in a programming language? I have been trying to find libraries/concepts which use this and so far I've come across one example:

1. In "The Naming Problem" where we'd like to have both (a) fast capture avoiding substitution and (b) fast alpha equivalence checking, there is the bound library (more detailed explanation here). Both of these properties are desirable when writing a compiler for a functional programming language.

To prevent the question from being overly broad, I'm looking for other programs/libraries/research papers that present applications of polymorphic recursion to traditional computer science problems such as those involved in writing compilers.

Examples of things that I'm not looking for:

1. Answers showing how you can encode X from category theory using polymorphic recursion, unless they demonstrate how encoding X can be beneficial for solving Y which falls under the criterion above.

2. Small toy examples which show that you can do X with polymorphic recursion but you can't without it.

Answer 1

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.