В разделе 23.8 своей книги Типы и языки программирования Бенджамин С. Пирс пишет следующее:
Другое хорошо изученное ограничение Системы F - полиморфизм ранга 2 , введенный Leivant (1983) [...]. Тип называется рангом 2, если путь от его корня до ∀ квантификатора не проходит слева от 2 или более стрелок, когда тип рисуется в виде дерева. [...] В системе ранга 2 все типы ограничены рангом 2. Эта система немного более мощная, чем фрагмент prenex (ML), в том смысле, что она может присваивать типы более нетипизированным лямбда-терминам .
Kfoury и Tiuryn (1990) доказали, что сложность восстановления типа для фрагмента ранга 2 системы F идентична сложности ML (т.е. DExptime-complete). Kfoury and Wells (1999) дали первый правильный алгоритм восстановления типа для системы ранга 2 и показали, что восстановление типа для рангов 3 и выше системы F неразрешимо.
Таким образом, вывод типа для полиморфизма ранга 2 известен как разрешимый, и алгоритм известен с 1999 года. Haskell поддерживает расширение языка RankNTypes, но он допускает полиморфизм ранга n.
Какие языки, если таковые имеются, реализуют параметрический полиморфизм ранга 2, но не System F?
Поскольку вывод типа является разрешимым и не имеет худшей сложности, почему ни SML, ни OCaml не расширили полиморфизм до ранга-2?
Почему мы не видим и не читаем больше о полиморфизме ранга 2 в дикой природе?