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:
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:
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.
Small toy examples which show that you can do X with polymorphic recursion but you can't without it.
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.