Типовые системы функциональных объектно-ориентированных языков

Я хотел бы знать, как именно современные типизированные функциональные объектно-ориентированные языки, такие как Scala и OCaml, объединяют параметрический полиморфизм, подтипирование и другие их функции.

Являются ли они основаны на System F <: или что-то более сильное или слабее?

Есть ли хорошо изученная формальная система типа, например System F C для Haskell, которая может служить "ядром" для эти языки?

Ответы

Ответ 1

OCaml

"Ядро" теории типа OCaml состоит из расширений системы F, но модульная система соответствует сочетанию F <: (модули могут быть принуждены к более строгой подписи подтипами) и Fω.

На основном языке (без учета подтипов на уровень модуля), подтипирование очень ограничено в OCaml, поскольку подтипирование отношения нельзя отвлечь (нет ограниченная количественная оценка). Язык подчеркивает полиморфность вместо этого параметризм и, в частности, даже "расширяемый" тип поддерживает использование строкового полиморфизма в своем ядре (с комфортным слоем подтипирования между закрытыми такими типами).

Для введения в теоретико-теоретические представления OCaml см. онлайн-книгу Дидье Реми, Использование, понимание и раскрытие языка OCaml (от практики к теории и наоборот). Его глава далее читает даст вам больше информации, в частности о лечении объектной ориентации.

Проделана большая работа по формализации части модульной системы; возможно, модульные системы ML естественно не соответствуют Fω или F <: ω как основной формализм (на этот раз параметры типа называются в модульной системе, а не передается по положению, как в лямбда-исчислениях). Одним из лучших объяснений переписки является F-ing modules, впервые опубликованная в 2010 году Андреасом Росбергом, Клаудио Руссо и Дереком Драйером.

Jacques Garrigue также проделал большую работу над более продвинутыми функциями языка (которые нельзя суммировать как "просто синтаксический сахар над системой F" ), а именно "Полиморфные варианты" (структурные типы с эквивалентными рекурсиями), помеченные аргументы, и GADT). Различные описания этих аспектов можно найти на его веб-странице, включая механизированные доказательства (в Coq) полиморфных вариантов и ослабленное ограничение значения.

Вы также должны посмотреть на веб-страницу Несколько работ по Caml, в которых указывается на некоторые статьи исследования, посвященные языку OCaml.

Scala

Аналогичная страница для Scala эта. Особенно актуальными для вашего вопроса являются: