Вот один пример, близкий к моей работе, который, я думаю, обобщает довольно хорошо: в конкатенативном языке, то есть в языке, построенном на создании функций, которые работают с общим состоянием программы, таким как стек, все функции полиморфны по отношению к часть стека, которую они не касаются, вся рекурсия - это полиморфная рекурсия, и, кроме того, все функции более высокого порядка также имеют более высокий ранг. Например, тип map на таком языке может быть:
∀αβσ. σ × список α × (.τ. τ × α → τ × β) → σ × список β
Где × - левоассоциативный тип продукта со стековым типом слева и типом со значением справа, σ и τ - переменные типа со стеком, а α и β - тип со значением переменные. map можно вызывать для любого состояния программы σ, если оно имеет список αs и функцию от αs до βs сверху, например:
"ignored" [ 1 2 3 ] { succ show } map
=
"ignored" [ "2" "3" "4" ]
Здесь есть полиморфная рекурсия, потому что map вызывает себя рекурсивно при разных экземплярах σ (то есть при разных типах «остатка стека»):
-- σ = 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" ]
И функциональный аргумент map должен иметь более высокий ранг, поскольку он также вызывается для разных типов стеков (разные экземпляры τ).
Чтобы сделать это без полиморфной рекурсии, вам понадобится дополнительный стек или локальные переменные, в которые будут помещены промежуточные результаты map, чтобы «убрать их с пути», чтобы все рекурсивные вызовы происходили на тот же тип стека. Это имеет значение для того, как функциональные языки могут быть скомпилированы, например типизированные комбинаторные машины: с полиморфной рекурсией вы можете сохранить безопасность, сохраняя простоту виртуальной машины.
Общая форма этого заключается в том, что у вас есть рекурсивная функция, которая полиморфна над частью структуры данных, такой как начальные элементы HList или подмножество полиморфной записи.
И, как уже упоминалось, @chi, основной случай, когда вам нужна полиморфная рекурсия на уровне функций в Haskell, - это когда у вас полиморфная рекурсия на уровне тип , например:
data Nest a = Nest a (Nest [a]) | Nil
example = Nest 1 $ Nest [1, 2] $ Nest [[1, 2], [3, 4]] Nil
Рекурсивная функция над таким типом всегда полиморфно рекурсивна, поскольку параметр типа изменяется с каждым рекурсивным вызовом.
Haskell требует сигнатуры типов для таких функций, но механически нет никакой разницы между рекурсией и полиморфной рекурсией. Вы можете написать полиморфный оператор с фиксированной запятой, если у вас есть дополнительный newtype, который скрывает полиморфизм:
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))))
Без всех церемоний упаковки и распаковки, это то же самое, что и fix' f = fix f.
Это также причина того, что полиморфная рекурсия не должна приводить к взрыву экземпляров функции - даже если функция специализируется на параметрах своего типа-значения, она «полностью полиморфна» в рекурсивном параметре, поэтому он вообще не манипулирует им , и поэтому ему требуется только одно скомпилированное представление.