Я хотел бы знать, как именно современные типизированные функциональные объектно-ориентированные языки, такие как Scala и OCaml, объединяют параметрический полиморфизм, подтипирование и другие их функции.
Являются ли они основаны на System F <: или что-то более сильное или слабее?
Есть ли хорошо изученная формальная система типа, например System F C для Haskell, которая может служить "ядром" для эти языки?
"Ядро" теории типа OCaml состоит из расширений системы F, но модульная система соответствует сочетанию F <: (модули могут быть принуждены к более строгой подписи подтипами) и Fω.
На основном языке (без учета подтипов на уровень модуля), подтипирование очень ограничено в OCaml, поскольку подтипирование отношения нельзя отвлечь (нет ограниченная количественная оценка). Язык подчеркивает полиморфность вместо этого параметризм и, в частности, даже "расширяемый" тип поддерживает использование строкового полиморфизма в своем ядре (с комфортным слоем подтипирования между закрытыми такими типами).
Для введения в теоретико-теоретические представления OCaml см. онлайн-книгу Дидье Реми, Использование, понимание и раскрытие языка OCaml (от практики к теории и наоборот). Его глава далее читает даст вам больше информации, в частности о лечении объектной ориентации.
Проделана большая работа по формализации части модульной системы; возможно, модульные системы ML естественно не соответствуют Fω или F <: ω как основной формализм (на этот раз параметры типа называются в модульной системе, а не передается по положению, как в лямбда-исчислениях). Одним из лучших объяснений переписки является F-ing modules, впервые опубликованная в 2010 году Андреасом Росбергом, Клаудио Руссо и Дереком Драйером.
Jacques Garrigue также проделал большую работу над более продвинутыми функциями языка (которые нельзя суммировать как "просто синтаксический сахар над системой F" ), а именно "Полиморфные варианты" (структурные типы с эквивалентными рекурсиями), помеченные аргументы, и GADT). Различные описания этих аспектов можно найти на его веб-странице, включая механизированные доказательства (в Coq) полиморфных вариантов и ослабленное ограничение значения.
Вы также должны посмотреть на веб-страницу Несколько работ по Caml, в которых указывается на некоторые статьи исследования, посвященные языку OCaml.
Аналогичная страница для Scala эта. Особенно актуальными для вашего вопроса являются: