Interested Article - Язык модулей ML
- 2021-07-06
- 1
Язык модулей ML — система модулей , используемая преимущественно в языках программирования семейства ML , имеющая аппликативную семантику, иначе говоря, представляющая собой небольшой функциональный язык , оперирующий модулями .
Является наиболее развитой системой модулей среди встречающихся в языках программирования
.Общие сведения
В простейшей форме язык модулей состоит из трёх видов модулей:
- структура
- сигнатура
- функтор
Сигнатуру можно рассматривать как описание структуры, а структуру, соответственно, как реализацию сигнатуры. Многие языки предоставляют похожие конструкции, обычно под другими названиями: сигнатуры часто называются интерфейсами или спецификациями пакетов, а структуры часто называются реализациями ( implementations ) или пакетами. Вне зависимости от терминологии, идея состоит в назначении типа целому фрагменту кода. В отличие от многих языков, в ML отношения между сигнатурами и структурами выстраиваются по схеме « многие-ко-многим » , а не « многие-к-одному » или « один-к-одному » . Сигнатура может описывать множество разных структур, а структура может соответствовать многим разным сигнатурам. Большинство других языков связаны более сильными ограничениями, требуя, чтобы данная структура имела единственную сигнатуру, или чтобы данная сигнатура выводилась из единственной структуры. Это не так в случае ML .
В мейнстримных объектно-ориентированных языках вроде C++ или Java , абстракция обеспечивается посредством классов , которые совмещают в одной концепции сразу ряд возможностей ( наследование , и ), что затрудняет их формализацию и может приводить к нежелательным последствиям при неосторожном использовании. В отличие от классов, язык модулей ML полностью фокусируется на абстракции , предоставляя обширный спектр её форм и обеспечивая надёжную формальную базу для их исследования. Он предоставляет возможности управления иерархией пространств имён , тончайшей настройки интерфейсов , абстракцией на стороне реализатора и на стороне клиента .
Функторы являются уникальным понятием, не имеющим аналогов в большинстве языков
. Они являются функциями над структурами, то есть вычисляют новые структуры на основе уже вычисленных, естественно, в соответствии с определёнными сигнатурами. Это позволяет решать самые разнообразные задачи структурирования сложных программ .При этом соблюдаются два требования :
- полная статическая типобезопасность зависимостей между компонентами разных модулей;
- возможность раздельной компиляции модулей (в том числе функторов, в том числе, если в программе нет ни одной структуры, которая могла бы быть передана данному функтору в качестве параметра).
На практике возможность раздельной компиляции не всегда используется — существуют полнопрограммно-оптимизирующие компиляторы, раскрывающие рамки модулей для значительного повышения быстродействия программ .
Язык
Структуры и сигнатуры
Окружение ( англ. environment ) в ядре ML ( англ. Core ML ) представляет собой коллекцию определений ( типов , в том числе функциональных , и значений , в том числе функциональных и исключительных ). Окружение имеет лексическую область видимости .
Структура
(
structure
) представляет собой «материализованное» окружение, превращённое в значение, которым можно манипулировать
. В отношении ранних реализаций языка модулей это определение является в некотором роде условностью, так как изначально структуры могли определяться или вычисляться
только на верхнем уровне кода (в глобальном окружении). Последующие работы развивают язык модулей до
первоклассного
уровня
.
Введение понятия структуры требует пересмотра определения окружения в ядре языка. Отныне окружение представляет собой коллекцию типов, значений и структур. Соответственно, структура представляет собой коллекцию типов, значений и других структур. Рекурсивное вложение структур не допускается, хотя некоторые реализации их поддерживают .
Основным средством определения структур являются
инкапсулированные объявления
, то есть объявления, заключённые в синтаксические скобки
struct...end
. Например, следующая структура реализует
стек
, определяя внутреннюю организацию объектов
алгебраического типа
«стек» и минимально необходимый набор функций над ним:
struct
type 'a t = 'a list
val empty = []
val isEmpty = null
val push = op ::
val pop = List.getItem
end
«Значением» этого инкапсулированного объявления является структура. Чтобы это значение использовать, необходимо назначить ему идентификатор:
structure Stack = struct
type 'a t = 'a list
val empty = []
val isEmpty = null
val push = op ::
val pop = List.getItem
end
Теперь доступ к компонентам структуры может осуществляться посредством составных (или квалифицированных) имён, например,
Stack.push
,
Stack.empty : Stack.t
.
Сигнатура
(
signature
) представляет собой перечисление описаний элементов структуры, то есть
интерфейс
структуры. Каждый элемент этого перечисления называется спецификацией. Если в сигнатуре для
значения
x
специфицирован
тип
t
, то в структуре идентификатор
x
должен
к значению
типа
t
. Можно понимать сигнатуру как своего рода «
тип
» структуры, но сигнатура не является типом в строгом понимании, так как тип представляет собой множество
значений
, а «значение сигнатуры» может содержать
типы
(которые в ML значениями не являются). Каждый идентификатор в сигнатуре должен быть единственен. Правило
лексического
затенения имён в сигнатурах не соблюдается, поэтому порядок их перечисления значения не имеет, но типы должны быть объявлены до их использования, поэтому традиционно их помещают в начало сигнатуры.
Определение сигнатуры записывается в синтаксических скобках
sig...end
. Например, структура
Stack
имеет следующую сигнатуру (компилятор
выводит
её автоматически):
structure Stack : sig
type 'a t = 'a list
val empty: 'a t
val isEmpty: 'a t -> bool
val push: 'a * 'a t -> 'a t
val pop: 'a t -> ('a * 'a t) option
end
Основным свойством сигнантур является то, что структуры могут сопоставляться ( англ. match ) с ними. Структура является сопоставимой с данной сигнатурой, если она содержит как минимум перечисленные в сигнатуре типы, значения и вложенные структуры . Существуют две формы сопоставления структур с сигнатурами: прозрачное ( англ. transparent ) и тёмное ( англ. opaque ). Обобщённо возможность выбирать форму подписывания называется свойством полупрозрачности ( англ. translucency ) сигнатур .
Выведенная компилятором «сигнатура по умолчанию» обычно является избыточной, так как предоставляет в общий доступ информацию о реализации своих компонентов, что является нарушением принципа абстракции . Поэтому в большинстве случаев программист явно описывает желаемую сигнатуру и осуществляет подписывание сигнатурой ( англ. signature ascription ) или опечатывание ( англ. sealing ) , обеспечивая таким образом сокрытие выбранных им компонентов структуры от остальной программы . Говоря более точно, осуществляется структуры, прошедшей сопоставление.
Например, разработчик может определить сигнатуру, описывающую разнообразные потоки данных ( структуры данных с последовательным доступом), и назначить ей идентификатор:
signature STREAM = sig
type 'a t
val empty : 'a t
val isEmpty: 'a t -> bool
val push: 'a * 'a t -> 'a t
val pop: 'a t -> ('a * 'a t) option
end
Собственная сигнатура структуры может обогащать ( англ. enrich ) сигнатуру, с которой производится сопоставление, то есть содержать большее количество компонентов, большее количество типов и эти типы могут быть более общими. Отношение обогащения формально записывается как (сигнатура обогащает сигнатуру ).
В данном случае можно записать: .
Прозрачное сопоставление традиционно имеет синтаксис «
S : SS
», а тёмное — «
S :> SS
». Однако, создатели
OCaml
отказались от поддержки прозрачного сопоставления полностью, то есть все сопоставления в
OCaml
являются тёмными, но для простоты используется синтаксис «
S : SS
».
В простейших случаях можно подписывать сигнатуру немедленно, не назначая ей отдельного идентификатора:
structure Stack :> sig
type 'a t
val isEmpty: 'a t -> bool
val push: 'a * 'a t -> 'a t
val pop: 'a t -> ('a * 'a t) option
end = struct
type 'a t = 'a list
val empty = []
val isEmpty = null
val push = op ::
val pop = List.getItem
end
Однако, на практике безымянные сигнатуры довольно редки, поскольку применение сигнатур не ограничивается лишь сокрытием .
Одна структура в разных контекстах может сопоставляться с разными сигнатурами, а одна сигнатура может служить интерфейсом для разных структур. Сигнатура определяет класс структур (в математическом понимании термина « класс ») . Разный «вид извне» для одной структуры, с разной степенью абстракции , можно обеспечить посредством нескольких сигнатур с разным набором спецификаций . Порядок следования объявлений не имеет значения и не влияет на сопоставимость структур с сигнатурами.
Это можно рассматривать как простейший аналог
абстрактных классов
(в терминах
объектно-ориентированного программирования
) в том смысле, что сигнатура описывает общий
интерфейс
, а сопоставимые с ней структуры реализуют этот интерфейс различным образом. Однако, в ML связь «родитель-потомок» явно не объявляется, поскольку
система типов
ML имеет
семантику, то есть сопоставление структуры с сигнатурой осуществляется тем же механизмом, что и сопоставление значения
5
с типом
int
.
Например, можно определить структуру, которая реализует
очередь
, но которая также сопоставима с сигнатурой
STREAM
:
structure Queue = struct
datatype 'a t = T of 'a list * 'a list
val empty = T ([], [])
val isEmpty = fn T ([], _) => true
| _ => false
val normalize = fn ([], ys) => (rev ys, [])
| q => q
fun push (y, T (xs, ys)) = T (normalize (xs, y::ys))
val pop = fn (T (x::xs, ys)) => SOME (x, T (normalize (xs, ys)))
| _ => NONE
end
Поскольку структура
Stack
не была явным образом подписана более бедной сигнатурой, то внешняя программа «знает» о том, что тип
t
тождественен типу
list
и может использовать это знание, обрабатывая объекты этого типа методами стандартного модуля
List
. Если впоследствии потребуется изменить реализацию структуры
Stack
(например, представив стек посредством заранее выделенного
массива
), то это потребует переписывания всего кода, который использовал это знание. То же верно и для структуры
Queue
. Более того, если некий модуль был параметризован
собственной сигнатурой структуры
Stack
, то ему будет невозможно передать в качестве параметра структуру
Queue
.
Таким образом, экспортирование лишней информации из структур существенно ухудшает модифицируемость программ. Для повышения уровня абстракции следует подписывать структуры более бедными сигнатурами, например:
structure Stack :> STREAM = struct
type 'a t = 'a list
val empty = []
val isEmpty = null
val push = op ::
val pop = List.getItem
end
Структура
Stack
сопоставлена с сигнатурой
STREAM
тёмным образом, поэтому внешняя программа будет иметь возможность в полной мере оперировать значениями типа
Stack.t
, но не будет иметь доступа к его реализации, и из всех возможных значений этого типа она будет иметь возможность использовать лишь значение
Stack.empty
(опять же, «не зная» о том, что оно равно
nil
). Любая обработка данных этого типа будет осуществляться
абстрактно
, без учёта его реализации, и осуществлять её можно лишь посредством функций
Stack.push
и
Stack.pop
.
Но нигде сигнатуры так ни важны и ни полезны, как при использовании функторов
.Наследование
Структуры могут вкладываться друг в друга:
structure E = struct
structure A
structure B
...
end
Естественно, сигнатуры позволяют описывать вложенные структуры. При этом, как и в остальных случаях, вложение структур контролируется на основании сигнатур, а не по тождественному совпадению:
signature D = sig
structure A : C
structure B : C
end
Сигнатуры можно
включать
(синтаксис
include S
) друг в друга, последовательно обогащая интерфейс:
signature POOR = sig
type 'a t
val isEmpty: 'a t -> bool
val push: 'a * 'a t -> 'a t
val pop: 'a t -> ('a * 'a t) option
end
signature RICH = sig
include POOR
val empty : 'a t
end
Согласно описанной семантике, подписывание сигнатуры не обязательно осуществлять немедленно. Если требуется разработать некий набор тесно взаимосвязанных модулей, которые более «дружны» между собой, чем с остальной программой, то после окончания его разработки можно подписать структуры более бедными сигнатурами:
structure SomeModule :> RICH = struct ... end
...
structure SomeModule :> POOR = SomeModule
Последнюю строку не следует рассматривать как
разрушающее присваивание
. Данная
идиома
основана на
лексической видимости
, являющейся неотъемлемым компонентом семантики любого
аппликативного языка
. Как в ядре
ML
, так и на уровне модулей, конструкция
x = a
всегда означает привязку значения к идентификатору. Привязка не является
присваиванием
, она «создаёт» новый идентификатор, не имеющий никакого отношения к (возможно) определённому ранее
. Исходная структура
SomeModule
по-прежнему существует в программе, но последующий код не имеет доступа к тем её компонентам, что не входят в состав более бедной сигнатуры (в данном случае это константа
empty
).
Структуру можно
открыть
(синтаксис
open S
). В простейшем случае это можно рассматривать как
синтаксический сахар
, служащий для удобства использования инкапсулированных в модуле определений (аналог конструкции
with
в языке
Pascal
):
fun foo x =
let
open SMLofNJ.Cont
in
fun f x = callcc (fn k => ... throw k ...)
fun g x = isolate ...
end
Если то же самое сделать на верхнем уровне программы (в глобальном окружении), это можно рассматривать как аналог конструкции
using namespace
в языке
C++
. Например, структуры, реализующие стандартные типы и операции над ними (
Int
,
Real
,
String
и другие) открыты по умолчанию (подробнее об этом см.
). Однако, возможность открытия структур существует также и внутри других структур, и в этом случае открытие служит инструментом
включения
структур друг в друга с целью последовательного расширения функциональности (аналог простейшего
наследования классов
). Например:
structure B = struct
open A
...
end
Структура
B
включает в себя все определения структуры
A
и дополняет их новыми определениями. Это тождественно тому, чтобы явно перечислить все определения
A
внутри
B
. Такая возможность имеет два недостатка
:
- если в открываемой структуре существуют идентификаторы, совпадающие с уже имеющимися в данном контексте идентификаторами, то последние станут недоступными для прямого обращения. И наоборот, определения после открытия затенят импортированные компоненты. Конфликта имён не происходит — только последнее определение является видимым — но это может создавать неудобства для разработчика. Исключение составляет совпадение имён типов с имеющимися именами значений, так как компилятор ML всегда может определить смысл идентификатора из контекста его использования (см. вывод типов ). Проблема затенения имён особенно актуальна при включении двух и более структур.
- иногда становится трудно определить, что именно включается из открываемой структуры, особенно при открытии крупных структур, определяющих большое количество идентификаторов.
Поэтому часто рекомендуется вместо открытия использовать введение короткого локального идентификатора , например:
structure SomeModule :> sig
fun f x : ...
fun g x : ...
...
end = struct
local
structure C = SMLofNJ.Cont
in
...
fun f x = C.callcc (fn k => ... C.throw k ...)
fun g x = C.isolate ...
end
end
Тем не менее, иногда приоритет последнего определения может использоваться для умышленного «переопределения» идентификатора (что, однако, не является перегрузкой ).
Историческая справка
Ранее, в Определении SML'90
, существовала возможность открытия в сигнатурах. Эта возможность подвергалась критике из-за ухудшения самодокументируемости (изучение
интерфейса
одного модуля при её использовании вынуждает обращаться к другому)
, и её упразднили в Ревизии языка SML'97.
Открытие
(
open
) принципиально отличается от
включения
(
include
), поскольку внутри сигнатуры каждый идентификатор должен быть единственен и правило затенения имён не выполняется, так что совпадение идентификатора из состава включаемой сигнатуры с имеющимся в новой приводит к ошибке компиляции.
В SML'90
существовал особый подвид сигнатуры —
abstraction
, а для обычных сигнатур была лишь одна форма сопоставления — прозрачная (
S : SS
). При ревизии языка в
1997 году
эта часть языка модулей была упрощена: взамен абстрактных сигнатур было введено тёмное (
англ.
opaque
) сопоставление с сигнатурой (
S :> SS
)
(в основе решения лежит исчисление просвечивающих сумм Харпера — Лилибриджа
).
Функторы
Функтор
(
functor
) представляет собой функцию над структурами
, то есть функцию, которая получает структуру на входе и строит новую структуру
. Иногда функтор наглядно рассматривают как «параметризованную структуру», то есть структуру, определение которой строится компилятором на основе некой другой структуры по заданным программистом правилам. Однако, ортодоксы утверждают, что о функторах следует мыслить именно как о своеобразных функциях
.
Сигнатура типа параметра функтора. Всевозможные структуры, которые могут быть сопоставимы с этой сигнатурой, играют роль значений, принадлежащих этому типу и передаваемых функтору для вычисления новых структур . Получаемая в результате применения функтора структура имеет свою сигнатуру (хотя, вообще говоря, она может и не отличаться от сигнатуры параметра).
играет рольОбщая форма определения функтора выглядит так:
functor F ( X : S1 ) : S2 = body
Примеры использования:
structure B1 = F (A1)
structure B2 = F (A2)
structure B3 = F (A3)
...
Функторы позволяют типобезопасным образом описывать самые разнообразные формы взаимосвязей между компонентами программ, решая широкий спектр проблем структурирования кода :
- Реализация обобщённых алгоритмов и управление зависимостями. Функторы позволяют объединять в программе крупные компоненты сходного поведения, но разной реализации и подменять их по мере необходимости. Это особенно полезно на этапе быстрого прототипирования , когда приходится тестировать систему по частям или симулировать поведение упрощённым образом (см., например, и ).
- Автоматическое расширение функциональности. Функторы избавляют от рутинной работы при необходимости реализации одной и той же функциональности для разных типов. Например, если требуется определять множества из элементов разных типов данных, то в ML достаточно определить функтор, порождающий структуру, определяющую множество, на основе структуры, определяющей тип одного элемента. В других языках такого рода задачи решаются при помощи порождающего программирования .
- Инстанцирование модулей с инкапсулированным изменяемым состоянием . Если структура инкапсулирует изменяемое состояние , и в программе требуется иметь несколько её экземпляров с независимыми состояниями, то функторы позволяют автоматизировать построение таких структур.
Эти возможности лучше всего иллюстрировать наглядными примерами
.Однако, некоторые программисты используют функторы вместо структур (то есть описывают функтор и определяют структуру как единственное его применение к заведомо известному параметру , а порой и функтор с пустым параметром). Такой подход на первый взгляд кажется излишеством, но на практике даёт два преимущества, способствующих повышению продуктивности разработчиков в крупных проектах :
- с одной стороны, правильность организации интерфейсов обеспечивается немедленно на этапе компиляции едва написанного модуля, а не по мере развития проекта (ибо зависимости структур друг от друга в этом случае контролируются механизмом проверки согласования типов , а не обнаруживаются при сборке)
- с другой стороны, структуры становятся «более независимы» друг от друга, так что их можно разрабатывать в произвольном порядке, и программисты в команде оказываются вольны работать в прямо противоположных направлениях ( ).
Главным недостатком такого подхода, помимо усложнения исходного кода, является необходимость интенсивного использования спецификации соиспользования
.Эквивалентность типов
, когда модули компонуются для создания новых, более сложных, возникает вопрос о согласовании абстрактных типов , экспортированных из этих модулей. Для решения этой задачи язык модулей ML предусматривает специальный механизм, позволяющий явно указать идентичность двух и более типов или структур:
Приsignature D = sig
structure A : C
structure B : C
sharing type A.t = B.t
end
Такая спецификация накладывает ограничение (
англ.
constraint
) на допустимое множество наборов подставимых структур, объявляя требование, что это должны быть структуры, которые разделяют (
англ.
share
) использование одной и той же спецификации (типа, сигнатуры или структуры). Таким образом, с сигнатурой
D
сопоставимы
только те
структуры, в которых идентификатор
t
означает
один и тот же
тип
. Поэтому такая спецификация носит название «
sharing constraint
».
Примечание — в русскоязычной литературе перевод этого термина не устоялся. Возможны такие варианты как « спецификация соиспользования » , « ограничение на разделение », а также смысловой перевод « требование разделяемости » или « требование совместного использования ». Встречается перевод « совместное использовани е ограничени я », являющийся смысловой ошибкой.
Семантически имеется две формы такой спецификации — одна для сигнатур и типов, одна для структур — но их синтаксис идентичен. Вторая форма ограничена более жёсткими требованиями: две структуры могут быть равны тогда и только тогда, когда они получены в результате вычисления одного и того же объявления структуры или применения одного и того же функтора
к равным аргументам .Спецификация соиспользования также используется для принудительного сужения диапазона типов, допустимых в некотором конкретном контексте использования «излишне абстрактной» для него сигнатуры, например:
functor Try (Gr: sig
type g
sharing type g = int
val e: g
val bullet: g * g -> g
val inv: g -> g
end) =
struct
val x = Gr.inv( Gr.bullet(7, 9) )
end
Здесь сигнатура параметра функтора накладывает особое требование на состав структуры, которая может быть фактически передана ему: используемый в ней
абстрактный тип
g
обязан представлять собой тип
int
. Случаи, когда в этом есть необходимость, встречаются довольно часто, поэтому в SML'97
для упрощения их описания и возможности использования именованных сигнатур была добавлена альтернативная конструкция для спецификации соиспользования:
where type
(в
OCaml
синтаксис
with type
):
signature GROUP =
sig
type g
val e : g
val bullet: g * g -> g
val inv: g -> g
end
functor Try (Gr: GROUP where type g = int) =
struct
val x = Gr.inv( Gr.bullet(7, 9) )
end
Обе конструкции имеют свои ограничения.
sharing
позволяет выразить равенство типов, не указывая конкретно их структуру. Конструкция может иметь произвольную
арность
:
signature S = sig
structure A : S
structure B : S
structure C : S
structure D : S
sharing type A.t = B.t = C.t = D.t
end
но позволяет ссылаться на абстрактные типы только непосредственно — т.е. недопустимо выражение вида
sharing type B.t = A.t * A.t
where type
является
унарной
и предназначена, напротив, для
конкретизации
абстрактного типа
известным типом (но не позволяет изменить структуру типа, который уже был конкретно задан).
В
OCaml
конструкция
sharing
не поддерживается, так что всегда следует использовать конструкцию
with type
. В
предполагается реализовать единую наиболее универсальную конструкцию.
Другим важным аспектом установления эквивалентности абстрактных типов является порождаемость функторов .
Standard ML использует порождающую семантику функторов — это значит, что каждое применение функтора к одной и той же структуре порождает новые определения типов, т.е. два одноимённых и идентичных по структуре типа, принадлежащие к разным структурам, не равны.
OCaml использует аппликативные функторы — это значит, что применение функтора к доказуемо равным аргументам автоматически порождает один и тот же результат. Это снижает необходимость использования спецификации соиспользования и оказывается особенно полезно при работе с функторами высшего порядка. Начиная с 4-й версии OCaml добавляет возможность делать функторы порождающими.
Расширения и диалекты
Функторы высшего порядка
Функтор получает на вход одну структуру, заданную сигнатурой. Для передачи нескольких структур необходимо построить дополнительную структуру-обёртку, включающую эти структуры, и описать соответствующую сигнатуру. Определение языка Standard ML для удобства предусматривает синтаксический сахар — несколько параметров могут быть переданы в виде кортежа , а построение охватывающей структуры и её сигнатуры компилятор осуществляет автоматически. Однако, ядро ML предусматривает функции высшего порядка , и следование аналогии с ними на уровне модулей означает введение каррированной формы функторов. Фактически, единственное, что требуется реализовать в языке для обеспечения этой возможности — поддержку описания функторов в сигнатурах . Это не принципиальное новшество (в отличие от модулей первого класса ) — нет ничего такого, что позволяли бы каррированные функторы, но не позволяли бы классические первого порядка — однако, их доступность заметно упрощает реализацию (а следовательно, и читабельность ) сложных многоуровневых иерархий компонентов .
Ярким примером, показывающим удобство использования функторов высшего порядка, является реализация полноценных монадических комбинаторов .
Потенциальная возможность реализации функторов высшего порядка была отмечена ещё в Комментариях к Определению SML'90 . Многие компиляторы Standard ML предоставляют ту или иную реализацию функторов высшего порядка в качестве экспериментального расширения . Ocaml реализует все виды модулей синтаксически однородным образом, так что использование функторов высшего порядка оказывается наиболее естественным.
Примечание — в русскоязычной литературе встречается путаница между « модулями высшего порядка » и « модулями первого класса » , что является семантической ошибкой.
Объектно-ориентированные возможности
Полноценная поддержка объектно-ориентированного программирования по Абади и Карделли (см. Объектно-ориентированное программирование#Классификация подвидов ООП ) означает поддержку одновременно:
- отношений подтипизации
- объектов
- объектных типов
- классов (генераторов объектов)
Всё это уже много лет обеспечивает параметрический полиморфизм , что делает язык ещё более выразительным. Разумеется, язык модулей в OCaml доработан для возможности включения объектов и классов в состав модулей.
. Более того, на эти возможности также распространяетсяЭти средства (возможно, распространённые на типы высших родо́в — см. подтипизация высшего порядка ) станут частью .
Модули первого класса
Проблема
Слабостью изначального языка модулей является отсутствие замкнутости с ядром языка: базовые типы и значения могут быть компонентами модулей, но модули не могут быть компонентами базовых типов и значений. В SML такое разделение языка на два слоя было произведено умышленно, поскольку это существенно упростило механизм проверки согласования типов . Однако, это делает невозможным динамическое связывание модулей, то есть следующее выражение оказывается недопустимым:
structure Map = if maxElems < 100 then BinTreeMap else HashTableMap (* не допустимо в классических ML! *)
Такой запрет позорит столь выразительную систему модулей, так как для любого объектно-ориентированного языка это было бы совершенно нормальным .
В действительности, язык модулей ML не обязан быть статичным (см. раздел ). Проблема состоит главным образом в статической проверке согласования типов , составляющей природу ML . Поддержка в ML самих по себе модулей первого класса не представляет проблемы для языка модулей первого порядка (не содержащего функторов), но именно сочетание модулей первого класса с модулями высшего порядка переводит язык «в иную реальность» , то есть открывает огромные возможности, но существенно усложняет как механизмы выведения и проверки согласования типов языка , так и его полнопрограммную оптимизацию . Идею первоклассных модулей на многие годы похоронили Харпер и Лилибридж , построив идеализированную версию языка модулей первого класса с помощью теории зависимых типов и доказав, что проверка согласования типов для этой модели неразрешима . Однако, со временем стали появляться альтернативные модели, использующие другие обоснования.
Пакеты
В конце
XX века
Клаудио Руссо предложил
простейший способ сделать модули
первоклассными
: дополнить список примитивных типов ядра языка типом «
пакет
» (
англ.
package
), представляющим собой пару
структура : сигнатура
, а список выражений ядра — операциями упаковки и распаковки. Иначе говоря, изменяется только ядро языка, а язык модулей остаётся неизменным
.
Упаковка структур в пакеты и последующая распаковка позволяет динамически привязывать к идентификаторам разные структуры (в том числе вычисленные посредством функторов). Простейший пример :
structure Map = unpack ( if maxElems < 100
then pack BinTreeMap : MAP
else pack HashTableMap : MAP ) : MAP
При распаковке пакета структура может подписываться другой сигнатурой, в том числе более бедной
.Явное присутствие сигнатуры в пакете снимает проблему выведения и согласования типов при динамической распаковке структуры. Это опровергает ранний тезис Харпера — Митчела о невозможности поднять структуры в ML до первоклассного уровня, не пожервовав разделением фаз компиляции и запуска и разрешимостью системы проверки согласования типов , поскольку в качестве обоснования, вместо зависимых типов первого порядка, используется расширение теории экзистенциальных типов второго порядка Митчела — Плоткина .
В таком виде первоклассные модули реализованы в Alice и в , начиная с 4-й версии.
1ML
Вдохновившись F-преобразованием конструкторы типов являются в действительности одной и той же примитивной конструкцией, и не проводится различий между записями , кортежами и структурами — внутреннее представление языка представляет собой плоскую . Это дало целую массу положительных результатов :
, Россберг внедрил операцию упаковки-распаковки модулей глубже в семантику языка, построив в результате монолитный язык, в котором функторы, функции и даже- доказательство надёжности языка становится намного проще, чем традиционно для языка модулей (не требуется использование теории зависимых типов );
- обеспечивается поддержка «материализованных» ( англ. reified ) типов в ядре языка, обеспечивающих языку выразительную силу на уровне систем с зависимыми типами (и опять же не требующих их наличия в метатеории);
- язык в целом получается одновременно выразительнее (позволяет более ёмко и точно описывать сложные системы) и проще (минималистичнее и единообразнее по своему составу).
Язык получил название « 1ML », что отражает одновременно поддержку истинно первоклассных модулей и объединение примитивов и модулей в едином языке (не разделённом на два слоя) .
Основой решения послужила идея Харпера — Митчела подразделять типы на «малые» и «большие». Россберг применил это разграничение к правилу включения механизма проверки согласования типов (лежащему в основе сопоставления структур с сигнатурами), обеспечив таким образом его разрешимость .
Предположительно, дальнейшая доработка 1ML способна также обеспечить достаточную выразительность для поддержки многих интересных моделей, реализация которых ранее считалась затруднительной: классов типов , аппликативных функторов , рекурсивных модулей и др. В частности, введение рядного полиморфизма в 1ML, вероятно, немедленно позволит выразить подтипизацию в ширину , что сохранит простоту метатеории при существенном расширении возможностей.
MixML
MixML — это язык модулей, построенный посредством соединения классического языка модулей ML МакКуина и формализации модели примесей ( англ. mix -ins ) Брачи и Кука ( Bracha & Cook ). Авторами MixML являются Россберг и Дрейер.
Основная идея MixML проста: структуры и сигнатуры соединяются в единое понятие модуля, объединяющее определения и спецификации, как прозрачные, так и абстрактные.
Это делает возможным определение произвольных графов зависимостей в программах, в том числе цикличных. В частности, это позволяет выстраивать в функторах не только прямую параметризацию (зависимость выхода от входа), но и рекурсивную (зависимость входа от выхода), сохраняя при этом поддержку раздельной компиляции (в отличие от множества частных моделей, расширяющих язык модулей ML поддержкой рекурсии).
MixML реализует единую унифицированную нотацию для традиционно парных моделей семантики (для структур и сигнатур раздельно) и большого числа раздельных механизмов классического языка модулей ML, таких как:
- наследования (включения) сигнатур
- спецификации соиспользования
- двух форм подписывания сигнатур (прозрачного и тёмного)
- применения функторов
Прочее
В различных моделях предлагаются также следующие расширения:
- локальные модули
- множество вариантов рекурсивной системы модулей, позволяющих формировать циклические графы зависимостей, наиболее выразительной из которых является система MixML (большинство остальных не предусматривает возможности раздельной компиляции)
- расширенная поддержка вложения модулей
- обобщённая нотация открытия структур
- различные варианты возможности ограничения соиспользования
- вложенные сигнатуры, в том числе абстрактные
- объявления инфиксных операторов с указанием ассоциативности и приоритета внутри сигнатур и требованием точного совпадения
Экосистема языка
Реализации и диалекты
Alice
Язык Alice является расширением Standard ML , включающим многие идеи проекта , а также развитые средства конкурентного программирования для разработки распределённых приложений, поддержку сильной динамической типизации и решатель ограничений . Разработан Андреасом Россбергом.
Язык модулей в Alice расширен до нотации компонентов ( англ. components ), реализующих модули первого класса в виде пакетов Руссо и дополнительно поддерживающих динамическую типизацию (но по тем же правилам статической семантики) и ленивую загрузку (т.е. поддерживаются будущные структуры и будущные сигнатуры — см. вызов по будущности ) . Порождаемость типов в Alice соблюдается, и при необходимости следует использовать спецификацию соиспользования . Наглядный пример, показывающий практическую полезность пакетов, поставляется в составе Alice : библиотека сериализации данных , позволяющая потокам обмениваться динамическими типами и данными.
В дополнение,
Alice
предоставляет
синтаксический сахар
— возможность свободно использовать круглые скобки в выражениях языка модулей, в том числе вместо традиционных «скобок»
struct...end
и
sig...end
:
val p = pack (val x = length) : (val x : 'a list -> int)
(* val p : package = package{|...|} *)
OCaml
В Ocaml синтаксис языка модулей выполнен однородным:
module type S = (* сигнатура *)
sig
...
module M : T (* вложенная структура *)
end
module X : S = (* структура *)
struct
...
end
module F (X : S) = (* параметризованная структура (функтор) *)
struct
...
end
module G (X : S) (Y : T) = (* каррированная параметризованная структура (функтор высшего порядка) *)
struct
...
end
Однако, в семантике имеется ряд отличий .
Начиная с версии 4, Ocaml поддерживает первоклассные модули в нотации, аналогичной пакетам Alice . Синтаксис по-прежнему однороден, то есть выглядит неотличимо от вложенных структур в сигнатурах.
С момента своего появляения Ocaml расширяет язык модулей классами и объектами .
Наиболее важные различия между Standard ML и Ocaml проявляются в семантике (см. раздел ).
Управление модулями
Для линкования программ на ML в принципе могут использоваться традиционные для большинства языков линковщики , такие как make . Однако, язык модулей SML значительно мощнее средств модульности других языков , а make его преимуществ не поддерживает, и тем более не пригоден для глобального анализа потока управления программ . Поэтому разные компиляторы предлагают свои системы управления модулями: Compilation Manager (CM) в и MLBasis System (MLB) в MLton . SML.NET имеет встроенную систему отслеживания зависимостей. MLton также включает конвертор файлов формата .cm в формат .mlb .
В большинстве реализаций используется раздельная компиляция, что обеспечивает малое время компиляции. Для поддержки раздельной компиляции в режиме
REPL
используется функция
use
, которая компилирует указанный файл и импортирует определения. Некоторые компиляторы (например,
MLton
) не поддерживают
REPL
, а потому не реализуют поддержку функции
use
. Другие (например,
Alice
), напротив, реализуют дополнительные возможности
динамической компиляции
и загрузки модулей в процессе исполнения программы.
Poly/ML
предоставляет функцию
PolyML.ifunctor
, которая позволяет отлаживать реализацию функтора интерактивно по частям.
Примеры программ
При своей простоте, язык модулей обладает выдающейся гибкостью и обеспечивает высокий уровень повторного использования кода , что иллюстрируется следующими примерами.
Управление разрядностью чисел
Традиционные
типы данных
, такие как
целые
(
int
и
word
),
вещественные
(
real
), символьные (
char
и
widechar
), строковые (
string
и
widestring
),
массивы
(
vector
и
array
) и прочие, реализуются в диалектах ML не в виде
примитивных типов
и встроенных операторов над ними, как в большинстве языков, а в виде
абстрактных типов данных
и соответствующих функций, входящих в состав сигнатур, соответственно,
INTEGER
,
WORD
,
REAL
,
CHAR
,
STRING
и так далее, предоставляемых в виде стандартных библиотек. Конкретные реализации языка могут предоставлять очень эффективные представления этих абстрактных типов (например,
MLton
представляет массивы и строки так же, как это делает язык
Си
).
Например:
signature INTEGER =
sig
eqtype int
val toLarge : int -> LargeInt.int
val fromLarge : LargeInt.int -> int
val toInt : int -> Int.int
val fromInt : Int.int -> int
val precision : Int.int option
val minInt : int option
val maxInt : int option
val ˜ : int -> int
val * : (int * int) -> int
val div : (int * int) -> int
val mod : (int * int) -> int
val quot : (int * int) -> int
val rem : (int * int) -> int
val + : (int * int) -> int
val - : (int * int) -> int
val compare : (int * int) -> order
val > : (int * int) -> bool
val >= : (int * int) -> bool
val < : (int * int) -> bool
val <= : (int * int) -> bool
val abs : int -> int
val min : (int * int) -> int
val max : (int * int) -> int
val sign : int -> Int.int
val sameSign : (int * int) -> bool
val fmt : StringCvt.radix -> int -> string
val toString : int -> string
val fromString : string -> int option
val scan : StringCvt.radix -> (char, 'a) StringCvt.reader -> 'a -> (int * 'a) option
end
C сигнатурой
INTEGER
могут быть сопоставимы структуры
Int8
,
Int16
,
Int32
,
Int64
, а также
IntInf
и многие другие. Аналогично, с сигнатурами
CHAR
/
STRING
могут быть сопоставимы структуры
Char
/
String
и
WideChar
/
WideString
(и, возможно, какие-то другие), и для каждого варианта функторы сгенерируют соответствующий стек ввода-вывода (
StreamIO
,
TextIO
).
При этом одни структуры скрывают под абстрактным определением традиционное машинное представление (например,
Int32
,
Int64
), другие —
битовые поля
(например,
Int1
), а структура
IntInf
реализует
длинную арифметику
. В то же время, библиотеки могут интенсивно пересекать связи по схеме
«
многие-ко-многим
»
: спецификация
SML Basis
определяет множество обязательных и опциональных модулей, надстроенных над реализующими «примитивные» типы: мономорфные массивы, их некопирующие срезы и так далее. Даже типы «строка» (
string
) и «подстрока» (
substring
) в спецификации
SML Basis
определяются как
Char.char vector
и
Char.char VectorSlice.slice
(или
WideChar.char vector
и
WideChar.char VectorSlice.slice
для
WideString
). Таким образом, для использования одних и те же алгоритмов с числами разной разрядности, достаточно явно передать функтору
соответствующую структуру (открытие
не изменит уже вычисленных структур).
Разные компиляторы предоставляют разные наборы реализованных структур. Наиболее богатый ассортимент предоставляет
MLton
: от
Int1
до
Int32
включительно и
Int64
, такой же набор для
Word
(беззнаковых целых), а также
IntInf
(реализованный посредством
GNU Multi-Precision Library
) и множество дополнительных, таких как
Int32Array
,
PackWord32Big
,
PackWord32Little
и прочее.
В большинстве реализаций по умолчанию на верхнем уровне (в глобальном окружении) открыта структура
Int32
(или
Int64
), то есть использование типа
int
и операции
+
по умолчанию означает использование типа
Int32.int
и операции
Int32.+
(или, соответственно,
Int64.int
и
Int64.+
). Кроме того, предоставляются идентификаторы
Int
и
LargeInt
, которые по умолчанию привязываются к определённым структурам (например,
LargeInt
обычно равна
IntInf
). Разные компиляторы, в зависимости от своей ориентированности, могут использовать по умолчанию разные привязки в глобальном окружении, и такая тонкость может влиять на портируемость программ между компиляторами. Например, константа
Int.maxInt
содержит значение наибольшего возможного целого, упакованное в
, и его необходимо извлекать либо
сопоставлением с образцом
, либо вызовом функции
valOf
. Для типов конечной размерности значение
Int
N
.maxInt
равно
SOME(m)
, и использование обоих способов извлечения равнозначно. Но
IntInf.maxInt
равно
NONE
, так что прямое обращение к содержимому через
valOf
породит
исключение
Option
. По умолчанию
IntInf
открыта в компиляторе
Poly/ML
, так как он ориентирован на задачи
числодробилки
.
Абстрактные множества
В составе библиотек
OCaml
есть модуль
Set
, предоставляющий функтор
Make
. С его помощью можно легко построить множество на основе заданного типа элемента:
module Int_set = Set.Make (struct
type t = int
let compare = compare
end)
Порождённый модуль целочисленных множеств имеет следующую сигнатуру, выведенную компилятором:
module Int_set :
sig
type elt = int
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val max_elt : t -> elt
val choose : t -> elt
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
end
Аналогичная функциональность входит в состав библиотек компилятора
SML/NJ
(
ListSetFn
). В
SML Basis
предусмотрен лишь элементарный инструментарий.
Основное предназначение использования зависимого модуля вместо простой структуры здесь состоит в том, чтобы функция сравнения указывалась
один
раз, и все функции над конкретным типизированным множеством использовали
одну и ту же
функцию сравнения над типом элементов этого множества, чтобы программист, таким образом, был защищён от своих собственных ошибок. Абстрактные множества можно было бы реализовать, передавая каждой функции над множеством функцию сравнения всякий раз (как это делается, например, в стандартной функции языка
Си
qsort
— см.
), однако, это не только повысило бы трудоёмкость работы с множествами, но и несло бы в себе риск перепутать требуемую функцию сравнения, внедрив в программу трудно обнаружимую ошибку (см.
дублирование кода
).
К сожалению , так исторически сложилось, что в OCaml для функции сравнения принята сигнатура, указывающая возвращаемое значение двухвариантного ( булева ) типа (а для возможности широкого использования библиотечных модулей соглашения такого рода следует соблюдать). Более мощным является принятое в SML Basis (а также в Haskell Prelude ) решение на основе трёхвариантного типа:
datatype order = LESS | EQUAL | GREATER
val compare: int * int -> order
Тестирование структур
При быстром прототипировании нередко есть необходимость тестировать систему по частям или симулировать поведение упрощённым образом (реализовывать так называемые «заглушки»). С этой задачей изящно справляются функторы.
Например, пусть имеется три различные реализации некой структуры данных , скажем, очереди :
signature QUEUE =
sig
type 'a t
exception E
val empty : 'a t
val enq : 'a t * 'a -> 'a t
val null : 'a t -> bool
val hd : 'a t -> 'a
val deq : 'a t -> 'a t
end
structure Queue1 :> QUEUE = struct
...
end
structure Queue2 :> QUEUE = struct
...
end
structure Queue3 :> QUEUE = struct
...
end
Во многих языках для из-за недостатка абстракции для их сравнения потребовалось бы создавать отдельные программы методом копирования-вставки . Функторы же позволяют абстрагировать тест от реализации и перебрать их в единой программе:
functor TestQueue (Q: QUEUE) =
struct
fun fromList I = foldl (fn (x,q) => Q.enq(q,x)) Q.empty I
fun toList q = if Q.null q then []
else Q.hd q :: toList (Q.deq q)
end
val ns = upto(1, 10000)
(* val ns = [1, 2, 3, 4, ...] : int list *)
structure TQ1 = TestQueue (Queue1)
val q1 = TQ1.fromList ns
val l1 = TQ1.toList q1
l1 = ns
(* true : bool *)
...
structure TQ2 = TestQueue (Queue2)
structure TQ3 = TestQueue (Queue3)
...
Далее можно выбрать между поиском в ширину и в глубину для каждой реализации, и всё это также в единой программе:
functor BreadthFirst (Q: QUEUE) =
struct
...
end
functor DepthFirst (Q: QUEUE) =
struct
...
end
structure BF_Q1 = BreadthFirst (Queue1)
structure BF_Q2 = BreadthFirst (Queue2)
structure BF_Q3 = BreadthFirst (Queue3)
structure DF_Q1 = DeapthFirst (Queue1)
structure DF_Q2 = DeapthFirst (Queue2)
structure DF_Q3 = DeapthFirst (Queue3)
...
В дальнейшем «лишние» реализации удалять не обязательно. Более того, полнопрограммно-оптимизирующие компиляторы, такие MLton , самостоятельно удалят их — см. удаление мёртвого кода .
Этот метод может использоваться и для измерения эффективности, но на практике гораздо удобнее (и достовернее) измерять её посредством профилировщика , встроенного в компилятор.
Глобальная типобезопасность зависимостей между компонентами, которую обеспечивает язык модулей, видна на примере ошибочной попытки применения функтора:
structure Wrong = BreadthFirst(List);
(*
> Error: unmatched type spec: t
> Error: unmatched exception spec: E
> Error: unmatched val spec: empty
> Error: unmatched val spec: enq
> Error: unmatched val spec: deq
*)
Монады и классы типов
Язык Haskell , являющийся наследником ML , не поддерживает язык модулей ML. Вместо этого, поддержка в нём обеспечивается (помимо тривиальной системы модулей, аналогичной применяемым в большинстве языков) посредством монад и классов типов . Первые выражают абстрактное поведение, в том числе моделируя изменяемое состояние в терминах ссылочной прозрачности ; вторые служат средством управления квантификацией переменных типа , реализуя ad-hoc-полиморфизм . Язык модулей ML позволяет реализовать обе идиомы .
Класс типов есть не что иное как интерфейс, описывающий набор операций, чей тип задаётся независимой абстрактной переменной типа , называемой параметром класса. Следовательно, естественным представлением класса в терминах языка модулей будет сигнатура, которая, помимо собственно требуемого набора операций, включает также спецификацию типа (представляющую параметр класса) :
signature EQ = sig
type t
val eq : t * t -> bool
end
Монада реализуется сигнатурой:
signature MONAD = sig
type 'a monad
val ret : 'a -> 'a monad
val bnd : 'a monad -> ('a -> 'b monad) -> 'b monad
end
Примеры её использования:
structure Option : MONAD = struct
type 'a monad = 'a option
fun ret x = SOME x
fun bnd (SOME x) k = k x
| bnd NONE k = NONE
end
signature REF = sig
type 'a ref
val ref : 'a -> 'a ref IO.monad
val ! : 'a ref -> 'a IO.monad
val := : 'a ref -> 'a -> unit IO.monad
end
Полноценные монадические комбинаторы особенно удобно реализовывать с использованием функторов высшего порядка :
(* First order *)
signature MONOID =
sig
type t
val e : t
val plus : t * t -> t
end
functor Prod (M : MONOID) (N : MONOID) =
struct
type t = M.t * N.t
val e = (M.e, N.e)
fun plus((x1,y1), (x2,y2)) = (M.plus(x1,x2), N.plus(y1,y2))
end
functor Square (M : MONOID) : MONOID = Prod M M
structure Plane = Square (type t = real val e = 0.0 val plus = Real.+)
val x = Plane.plus(Plane.e, (7.4,5.4))
(* Higher order *)
signature PROD = MONOID -> MONOID -> MONOID
functor Square (M : MONOID) (Prod : PROD) : MONOID = Prod M M
structure T = Square Plane Prod
val x = T.plus(T.e, T.e)
(* Transparently *)
signature PROD' =
fct M : MONOID -> fct N : MONOID -> MONOID where type t = M.t * N.t
functor Square' (M : MONOID) (Prod : PROD') : MONOID = Prod M M
structure T' = Square' Plane Prod
val x = T'.plus(T'.e, ((7.4,5.4), (3.0,1.7)))
Значения, индексированные типами
— это идиома , присущая всем ранним языкам семейства ML , предназначенная для реализации ad-hoc-полиморфизма ( перегрузки функций ) посредством параметрического полиморфизма . Классы типов , впервые появившиеся в Haskell , представляют собой поддержку значений, индексированных типами, на уровне языка (и как таковые легко реализуются в языке модулей ).
В простейшем виде эта идиома продемонстрирована в следующем примере на OCaml :
module type Arith = sig
type t
val (+) : t -> t -> t
val neg : t -> t
val zero : t
end
module Build_type (M: Arith) = struct
let typ x = { Type.
plus = M.(+);
neg = M.(-);
zero = M.zero;
}
end
let int = let module Z = Build_type(Int) in Z.typ
let int64 = let module Z = Build_type(Int64) in Z.typ
let int32 = let module Z = Build_type(Int32) in Z.typ
let native = let module Z = Build_type(Native_int) in Z.typ
let float = let module Z = Build_type(Float) in Z.typ
let complex = let module Z = Build_type(Complex) in Z.typ
Объектная модель
С помощью языка модулей можно построить простую объектную модель с динамической диспетчеризацией. Это пример интересен с учётом того, что SML не предоставляет никаких средств объектно-ориентированного программирования и не поддерживает .
Простейшую динамически диспетчеризируемую объектную модель можно легко построить в SML посредством записей . Тип записи, включающий функциональные значения , играет роль абстрактного класса , определяющего сигнатуру методов. Сокрытие внутреннего состояния и приватных методов этих объектов обеспечивает лексическая область видимости ML; таким образом, замыкания (ML-функции) могут играть роль конструкторов объектов этого класса. Такая реализация не позволяет строить сложные многоуровневые иерархии наследования (для этого требуется реализовывать подтипы, что делается посредством сложной реализации значений, индексированных типами и для чего существует несколько разных методов), но на практике её вполне достаточно для большинства задач при хорошем проектировании . Ниже рассмотрен вывод такой объектной модели на уровень модулей.
В качестве базы используются простейшие потоки данных:
signature ABSTRACT_STREAM = sig
type 'a t
val isEmpty: 'a t -> bool
val push: 'a * 'a t -> 'a t
val pop: 'a t -> ('a * 'a t) option
end
signature STREAM = sig
include ABSTRACT_STREAM
val empty : 'a t
end
structure Stack :> STREAM = struct
type 'a t = 'a list
val empty = []
val isEmpty = null
val push = op ::
val pop = List.getItem
end
structure Queue :> STREAM = struct
datatype 'a t = T of 'a list * 'a list
val empty = T ([], [])
val isEmpty = fn T ([], _) => true | _ => false
val normalize = fn ([], ys) => (rev ys, []) | q => q
fun push (y, T (xs, ys)) = T (normalize (xs, y::ys))
val pop = fn (T (x::xs, ys)) => SOME (x, T (normalize (xs, ys))) | _ => NONE
end
С помощью функторов можно реализовать обобщённые алгоритмы , манипулирующие потоками данных неизвестного внутреннего устройства и назначения:
functor StreamAlgs (ST : ABSTRACT_STREAM) =
struct
open ST
fun pushAll (xs, d) = foldl push d xs
fun popAll d = let
fun lp (xs, NONE) = rev xs
| lp (xs, SOME (x, d)) = lp (x::xs, pop d)
in
lp ([], pop d)
end
fun cp (from, to) = pushAll (popAll from, to)
end
Инстанцирование этого функтора структурами, сопоставимыми с сигнатурой
ABSTRACT_STREAM
, порождает функции, манипулирующие соответствующими потоками данных:
structure S = StreamAlgs (Stack)
structure Q = StreamAlgs (Queue)
S.popAll (S.pushAll ([1,2,3,4], Stack.empty))
(* результат: [4,3,2,1] *)
Q.popAll (Q.pushAll ([1,2,3,4], Queue.empty))
(* результат: [1,2,3,4] *)
Функтор
StreamAlgs
принимает параметр сигнатуры
ABSTRACT_STREAM
, а структуры
Stack
и
Queue
были подписаны сигнатурой
STREAM
, обогащающей
сигнатуру
ABSTRACT_STREAM
. Отсюда следует одна тонкость: при разработке желательно соблюдать принятые в стандартной библиотеке конкретного диалекта соглашения, с тем, чтобы шире использовать имеющиеся наработки, особенно стандартные функторы (в SML Basis'2004 их не так много, но в расширениях некоторых компиляторов и в
OCaml
есть очень интересные примеры).
Порождённые структуры содержат определение типа
ST.t
из параметра функтора, но это
разные
типы: всякое определение типа в ML порождает новый тип. Поэтому попытка смешанного их использования приводит к
ошибке согласования типов
. Например, следующая строка будет отвергнута компилятором:
val q = Q.push (1, Stack.empty)
Интерфейс класса потоков удобно определить в виде записи . По соображениям типобезопасности предпочтительно использовать не псевдоним типа, а конструирующую функцию , отображающую такую запись на объект класса:
structure Stream = struct
datatype 'a t =
I of { isEmpty : unit -> bool,
push : 'a -> 'a t,
pop : unit -> ('a * 'a t) option }
fun O m (I t) = m t
fun isEmpty t = O #isEmpty t ()
fun push (v, t) = O #push t v
fun pop t = O #pop t ()
end
Модуль
Stream
фактически реализует сигнатуру
ABSTRACT_STREAM
(
), но явное подписывание отложено на потом.
Для превращения потокового модуля в потоковый класс необходимо добавить к нему два именованных конструктора , что можно сделать посредством функтора и конструкции открытия :
functor StreamClass (D : STREAM) : STREAM = struct
open Stream
fun make d =
I { isEmpty = fn () => D.isEmpty d,
push = fn x => make (D.push (x, d)),
pop = fn () =>
case D.pop d of
NONE => NONE
| SOME (x, d) => SOME (x, make d) }
val empty =
I { isEmpty = fn () => true,
push = fn x => make (D.push (x, D.empty)),
pop = fn () => NONE }
end
Структура, порождаемая функтором
StreamClass
, включает в себя все компоненты структуры
Stream
(в том числе,
конструктор
I
), но они не видны извне, так как
результат
функтора подписан сигнатурой
STREAM
.
Наконец можно опечатать модуль
Stream
:
structure Stream : ABSTRACT_STREAM = Stream
В этом нет необходимости с точки зрения
типобезопасности
, поскольку и в прежнем виде модуль
Stream
не позволяет нарушить инкапсуляцию. Однако, сокрытие
конструктора
I
обеспечивает гарантию, что только функтор
StreamClass
может быть использован для создания подклассов
ABSTRACT_STREAM
.
Очевидные примеры использования:
structure StackClass = StreamClass (Stack)
structure QueueClass = StreamClass (Queue)
Но это ещё не всё. Поскольку выше определённый функтор
StreamAlgs
принимает на вход структуру типа
ABSTRACT_STREAM
, то его можно инстанцировать структурой
Stream
, реализующей абстрактный потоковый класс:
structure D = StreamAlgs (Stream)
Порождённый модуль
D
, как и модуль
Stream
, работает с любым классом, наследованным от
ABSTRACT_STREAM
, что можно воспринимать как динамическую диспетчеризацию:
D.popAll (D.pushAll ([1, 2, 3, 4], StackClass.empty))
(* результат: [4,3,2,1] *)
D.popAll (D.pushAll ([1, 2, 3, 4], QueueClass.empty))
(* результат: [1,2,3,4] *)
Ни
Stream
, ни
D
не содержат не только
изменяемого состояния
, но и каких-либо констант — только типы и функции — однако, будучи переданным через механизм параметров,
абстрактный класс
здесь фактически используется как
первоклассное значение
, а не служит лишь виртуальной сущностью, как во многих объектно-ориентированных языках.
О языке
Низкоуровневое представление и эффективность
Традиционно структуры представляются в компиляторе посредством записей , а функторы — функциями над такими записями . Однако, существуют альтернативные внутренние представления — например, семантика Харпера — Стоуна и 1ML .
Использование функторов как средства декомпозиции крупного проекта означает замедление доступа к вычисленным посредством их конечным компонентам программ, и для каждого уровня вложения потери умножаются, как и при использовании обычных функций вместо непосредственных значений. Полнопрограммно-оптимизирующие компиляторы ( MLton , MLKit , SML.NET ) раскрывают рамки модулей и строят конечные определения компонентов функторов с учётом особенностей фактически переданных структур, что устраняет потери производительности. MLKit, кроме этого, использует раскрытие модулей для вывода регионов, что позволяет использовать язык для разработки приложений реального времени . При этом раскрытие рамок модулей может осуществляться различными стратегиями: например, MLton выполняет « дефункторизацию программы », а MLKit — « статическую интерпретацию языка модулей ». Существует реализация опционального дефункторизатора для OCaml .
Обоснование семантики
Многие годы язык модулей ML на теоретико-типовом уровне рассматривался как приложение теории зависимых типов , и это позволило доработать язык и тщательно исследовать его свойства. В действительности, модули (даже в первоклассной роли) не являются « по-настоящему зависимыми »: сигнатура модуля может зависеть от типов , входящих в состав другого модуля, но не от входящих в него значений .
Соответствие Митчела — Плоткина
Сильные суммы Маккуина
|
Этот раздел
не завершён
.
|
Просвечивающие суммы Харпера — Лилибриджа
Роберт Харпер и Марк Лилибридж ( Mark Lillibridge ) построили исчисление просвечивающих сумм ( англ. translucent sums ) для формального обоснования языка модулей первого класса высшего порядка. Это исчисление применяется в семантике Харпера — Стоуна . Кроме того, его элементы стали частью ревизированного Определения SML (SML'97).
Семантика Харпера — Стоуна
Семантика Харпера — Стоуна (сокращённо « семантика Х-С », англ. HS semantics ) представляет собой интерпретацию SML в типизированной системе ( typed framework ). Последняя включает систему модулей, основанную на просвечивающих суммах Харпера — Лилибриджа (см. выше). Интерпретация теоретически элегантна, но поддерживает ложное впечатление, что ML-модули сложны в реализации: в ней используются одноэлементные рода́ , зависимые типы и непростая система эффектов .
F-преобразование Россберга — Руссо — Дрейера
Андреас Россберг, Клаудио Руссо и Дерек Дрейер совместно показали, что распространённое мнение о неоправданно высоком пороге вхождения для языка модулей является ложным. Они построили преобразование языка модулей в плоскую Систему F ω ( лямбда-исчисление второго порядка), показав тем самым, что язык модулей сам по себе в действительности является лишь особым случаем ( синтаксическим сахаром ) использования Системы F ω . В этом смысле основным преимуществом использования модулей по сравнению с работой непосредственно в Системе F ω оказывается значительная степень автоматизации многих сложных действий (согласование сигнатур с учётом обогащения, неявная упаковка/распаковка экзистенциалов , и др.).
« F-инговая семантика » ( F-ing semantics ), или F-преобразование, поддерживает в том числе Функторы высшего порядка и модули первого класса в форме пакетов Руссо. Доказательство надёжности F-преобразования было механизировано «локально-безымянным» ( Locally Nameless ) методом в Coq . Авторы подытожили проделанную работу как крайне болезненную и не рекомендуют впредь использовать данный метод . Достигнутые результаты в дальнейшем вдохновили Россберга на создание 1ML .
Критика и сравнение с альтернативами
Язык модулей ML является наиболее развитой системой модулей в языках программирования и продолжает развиваться. Он предоставляет возможности управления иерархией пространств имён (посредством структур ), тончайшей настройки интерфейсов (посредством сигнатур ), абстракцией на стороне клиента (посредством функторов ) и на стороне реализатора (посредством опечатывания ) .
Большинство языков не имеют ничего, сравнимого с функторами . Ближайшим аналогом функторов могут служить появившиеся позже них шаблоны классов C++ , но функторы намного проще в использовании , так как шаблоны C++ не только не обеспечивают типобезопасность , но и страдают от целого ряда других недостатков . Некоторые языки предоставляют макро-подсистемы , позволяющие автоматически порождать код и гибко управлять зависимостями времени компиляции ( Lisp , Си ), но зачастую эти макро-подсистемы являются неверифицируемой надстройкой над основным языком, позволяя произвольное переписывание программы строка-к-строке, что может повлечь массу проблем . Лишь в XXI веке были разработаны макро-подсистемы, являющиеся типобезопасными ( , Nemerle ), некоторые из которых доступны одновременно с функторами (MetaML , ).
Отличительным достоинством функторов является то, что они могут компилироваться и проходить проверку типов даже в случае, если в программе нет ни одной структуры, которая могла бы быть передана им в качестве фактического параметра . При этом, функторы описывают взаимодействие на уровне интерфейсов , а не реализаций , позволяя разрывать зависимости времени компиляции. Обычно платой за это является некоторое снижение производительности программ, но методы полнопрограммной оптимизации успешно решают эту проблему .
Язык модулей часто воспринимается как сложный для понимания, причина чего лежит в сложной математике, необходимой для его обоснования. Саймон Пейтон-Джонс уподобил функторы автомобилю Porsche за их « высокую мощь, но скудное её соотношение с ценой » . Сторонники ML не соглашаются с этой точкой зрения, утверждая, что язык модулей не сложнее в использовании/реализации/понимании, чем классы типов Хаскела или система классов Java с дженериками и , и в действительности это вопрос субъективных предпочтений .
При обнаружении компилятором ошибок в определениях модулей, выводимые сообщения об ошибках могут оказываться очень длинными, что в случае с функторами, особенно высшего порядка, может причинять особое неудобство. Поэтому блок определений типов и функций над ними следует оформлять в виде модуля лишь после его разработки по частям (для чего в большинстве реализаций предусмотрен режим REPL ). Некоторые реализации (например, Poly/ML ) предоставляют собственные расширения для решения этой проблемы. Другие (например, SML2c), наоборот, позволяют компилировать только программы уровня модулей.
История, философия, терминология
Идея языка модулей состоит в том, чтобы семантика программ повторяла семантику ядра ML ( англ. Core ML ), то есть зависимости между крупными компонентами программ формулировались подобно зависимостям мелкого уровня. Соответственно, структуры представляют собой «значения» уровня модулей ( англ. module-level values ); сигнатуры (называемые также « типами модулей » или « модулями-типами ») характеризуют «типы» значений уровня модулей ( module-level types ), а функторы — «функции» уровня модулей. Аналогия, однако, не тождественная: как содержание модулей, так и отношения между модулями могут быть сложнее, чем в ядре языка. Наиболее значимыми усложнениями в этом смысле являются включение подструктур в сигнатуры и ограничение на соиспользование . В Комментариях к Определению SML'90 была отмечена потенциальная возможность реализации функторов высшего порядка (аналогии с функциями высшего порядка ), но их реализации появились позже .
В первоначальном виде язык модулей предложен Дэвидом МакКуином ( англ. David MacQueen ) . В дальнейшем наиболее существенный вклад в теоретико-типовое обоснование и расширение языка модулей внесли многие учёные. Работы включают формализацию рекурсивных , вложенных, локальных модулей, модулей высшего порядка и первого класса , а также неоднократный пересмотр их обоснования с целью упрощения как самой модели, так и её опорной метатеории и доказательства её надёжности. Развитие языка модулей тесно пересекается с развитием ядра ML и отмечено десятками работ многих учёных, но можно выделить следующие ключевые вехи:
- 1984 — МакКуин — начальная идея .
- 1990 — Милнер, Харпер, МакКуин, Тофти — отдельная от ядра языка модель в составе Определения, доказательство её надёжности посредством так называемого порождающего пломбирования типов .
- 1994 — Аппель, МакКуин — раздельная компиляция .
- 1995 — Леруа — упрощение метатеории до прозрачных типов (не порождающих), аппликативные функторы .
- 1994 — Харпер, Лилибридж — теоретико-типовое обоснование с зависимыми типами .
- 1999—2000 — Руссо — упрощение метатеории до второго порядка, первоклассные модули в форме пакетов .
- 2000 — семантика Харпера — Стоуна .
- 2010 — Россберг, Руссо, Дрейер — упрощение метатеории до плоской Системы F , механизация доказательства её надёжности в Coq .
- 2015 — Россберг — 1ML , единая с ядром языка модель .
Другой диалект ML — язык Caml — изначально поддерживал язык модулей с рядом отличий . Впоследствии он развился до языка Objective Caml , дополнившего язык модулей подсистемой объектно-ориентированного программирования , органично развивающей идеи языка модулей . OCaml продолжал непрерывно эволюционировать и к середине 2010-х годов его язык модулей дополнился рядом экспериментальных возможностей. Отдельные реализации SML поддерживают некоторые из этих возможностей в качестве расширений. Наиболее значимым нововведением являются модули первого класса , поддерживаемые также языком Alice .
Применение
В различных языках
Семантика языка модулей совершенно не зависит от того факта, что ML является строгим языком — он может использоваться и в ленивых языках . Более того, были предложены частные реализации языка модулей поверх ядер семантически иных языков (например, Prolog и ).
Параметрическое наращивание языков
В 2000 году Ксавье Леруа (разработчик OCaml ) предложил реализацию обобщённой порождающей модели, позволяющей надстроить язык модулей ML над ядром произвольного (в достаточно широком диапазоне) языка со своей системой типов (например, Си ) . Эта модель реализована посредством самого языка модулей — в виде функтора , параметризованного данными о ядре языка и описанием его механизма проверки согласования типов .
Модули как основа для ядра языка
После трёх десятилетий эволюции языка модулей как надстройки над ядром языка, в 2015 году Андреас Россберг (разработчик Alice ) предложил вместо традиционного надстраивания языка модулей поверх ядра языка, использовать язык модулей в качестве промежуточного языка для представления конструкций ядра языка. Это делает модули истинно первоклассными значениями (не требующими упаковывания в пакеты) — см. .
Примечания
- ↑ .
- ↑ , 2.Typeful languages, с. 5.
- ↑ .
- ↑ .
- ↑ .
- ↑ .
- , с. 50.
- , 7.4 The intended signature for queues, с. 264.
- ↑ .
- ↑ .
- ↑ .
- ↑ . Дата обращения: 16 декабря 2014. 14 января 2016 года.
- , 2.22 Signatures, с. 62.
- , 2.19 Introduction to modules, с. 59.
- , 7.5 Signature constraints, с. 264.
- , с. 58.
- , с. 13.
-
↑
, 7.14 The
open
declaration, с. 299—305. - , с. 36.
- ↑ .
- , open in signatures, с. 17.
- ↑ , Reference guide to modules, с. 309.
- . Дата обращения: 18 декабря 2014. 18 декабря 2014 года.
- ↑ , Глава 9. Функторы.
- , с. 75-76.
- , 7.13 Fully-functorial programming, с. 294.
- , с. 77.
- ↑ , с. 77-78.
- .
- .
- ↑ .
- ↑ .
- , с. 235.
- ↑ .
- ↑ .
- .
- , с. 1-2.
- , с. 2.
- ↑ .
- ↑ .
- ↑ , с. 17.
- .
- , с. 14.
- ↑ , с. 3.
- , с. 13.
- .
- .
- .
- . Дата обращения: 22 января 2015. 2 января 2015 года.
- ↑ . Дата обращения: 28 января 2016. 29 января 2016 года.
- ↑ . Дата обращения: 15 января 2015. 27 июня 2020 года.
- ↑ , 7.8 Testing the queue structures, с. 274.
- ↑ .
- . Дата обращения: 22 января 2015. 21 апреля 2016 года.
- . Дата обращения: 18 декабря 2014. 21 января 2015 года.
- . Дата обращения: 21 января 2015. Архивировано из 7 января 2016 года.
- .
- .
- , 18. Module Specification, с. 398-410.
- .
- K. Czarnecki, J. O'Donnell, J. Striegnitz, W. Taha. . — University of Waterloo, University of Glasgow, Research Centre Julich, Rice University, 2004. 5 марта 2016 года.
- , Lack of macros, с. 9.
- Steven E. Ganz, Amr Sabry, . . — International Conference on Functional Programming, ACM Press, 2001. 23 сентября 2015 года.
- .
- Simon Peyton Jones . Wearing the hair shirt: a retrospective on Haskell. — POPL, 2003.
- ↑ .
- .
- , с. 1.
Литература
Учебники, руководства, справочники, использование
- Язык Standard ML
-
.
Introduction to Standard ML
(неопр.)
. — Carnegie Mellon University, 1986. — ISBN PA 15213-3891.
-
Перевод на русский язык:
Роберт Харпер. Введение в Стандартный ML (неопр.) . — Carnegie Mellon University, 1986. — 97 с. — ISBN PA 15213-3891.
-
Перевод на русский язык:
- Lawrence C. Paulson. ML for the Working Programmer (неопр.) . — 2nd. — Cambridge, Great Britain: Cambridge University Press, 1996. — 492 с. — ISBN 0-521-57050-6 (твёрдый переплёт), 0-521-56543-X (мягкий переплёт).
- Riccardo Pucella. ( (англ.) ) // (Last revised January 10, 2001). — Cornell University, 2001. (недоступная ссылка)
- Роберт Харпер. Programming in Standard ML (неопр.) / . — Draft: ver.1.2 of 11.02.2011. — Carnegie Mellon University, 2011. — 297 с.
- Язык OCaml
-
Minsky, Madhavapeddy, Hickey.
(неопр.)
. — O'Reilly Media, 2013. — 510 p. —
ISBN 9781449324766
.
-
Перевод на русский язык:
Мински, Мадхавапедди, Хикки. Программирование на языке OCaml (неопр.) . — ДМК, 2014. — 536 с. — (Функциональное программирование). — ISBN 978-5-97060-102-0 .
-
Перевод на русский язык:
- Язык модулей
- . (глава онлайн-версии книги «Développement d’applications avec Objective Caml by Emmanuel Chailloux, Pascal Manoury and Bruno Pagano»)
- Michael P. Fourman. ( (англ.) ). — 2010.
- (англ.) .
История, анализ, критика
- David MacQueen. (неопр.) . — LFP'84 Proceedings of the 1984 ACM Symposium on LISP and functional programming, 1984. — С. 198-207. — ISBN 0-89791-142-3 . — doi : .
- David MacQueen. ( (англ.) ) // POPL. — ACM, 1986.
- Robin Milner , Mads Tofte, Роберт Харпер. The Definition of Standard ML (неопр.) . — The MIT Press, 1990. — ISBN 0-262-63181-4 .
- Robin Milner , Mads Tofte. ( (англ.) ). — Universiry of Edinburg, University of Nigeria, 1991. 1 декабря 2014 года.
- . ( (англ.) ) // IFIP State-of-the-Art Reports. — New York: Springer-Verlag, 1991. — Вып. Formal Description of Programming Concepts . — С. 431–507 .
- Andrew W. Appel. ( (англ.) ). — Princeton University, revised version of CS-TR-364-92, 1992.
- Andrew Appel, David MacQueen. ( (англ.) ). — SIGPLAN 94-6/94, ACM 0-89791-662-x/94/006, 1994. — doi : .
- Robert Harper, Mark Lillibridge. (неопр.) . — POPL. — ACM Press, 1994. — ISBN CMU-CS-93-197. — doi : .
- Xavier Leroy . ( (англ.) ). — POPL, 1995.
- Mads Tofte. ( (англ.) ). — University of Copenhagen, 1996.
- Robin Milner , Mads Tofte, Robert Harper, David MacQueen. (неопр.) . — The MIT Press, 1997. — ISBN 9780262631815 .
- John C. Reynolds. . — Cambridge University Press, 1998. — ISBN 978-0-521-59414-1 (hardback), 978-0-521-10697-9 (paperback).
- Claudio Russo. ( (англ.) ) // Principles and Practice of Declarative Programming. — Principles and Practice of Declarative Programming, 1999.
- Claudio Russo. ( (англ.) ). — International Conference on Principles of Programming Languages, 2000.
- Xavier Leroy. ( (англ.) ) // vol.10, issue 3. — Journal of Functional Programming, 2000. — С. 269-303 .
- Derek Dreyer, Karl Crary, Robert Harper. ( (англ.) ) // CMU-CS-05-131. — POPL, 2003. — doi : .
- Derek Dreyer. ( (англ.) ) // CMU-CS-05-131. — Carnegie Mellon University, 2005.
- Andreas Rossberg. ( (англ.) ). — ICFP, 2006. — doi : .
- Stephen Weeks. ( (англ.) ). — 2006. 29 июня 2007 года.
- Derek Dreyer, Robert Harper. ( (англ.) ). — ACM SIGPLAN, 2007.
- Derek Dreyer, Andreas Rossberg. ( (англ.) ). — ICFP, 2008.
- Georg Neis, Derek Dreyer, Andreas Rossberg. ( (англ.) ) // ICFP. — ACM, 2009.
- Alain Frisch, Jacques Garrigue. ( (англ.) ). — 2010.
- Jeremy Yallop, Oleg Kiselyov. ( (англ.) ). — ACM SIGPLAN Workshop on ML, 2010.
- Andreas Rossberg, Claudio Russo, Derek Dreyer. ( (англ.) ). — TLDI, 2010.
- Andreas Rossberg. ( (англ.) ). — ICFP, 2015.
Ссылки
- Dwight VandenBerghe. (англ.) . Yale FLINT group (28 июля 1998). Дата обращения: 18 ноября 2016.
- Jens Olsson, Andreas Rossberg. (англ.) . Max-Planck-Institut für Softwaresysteme (18 января 2011). Дата обращения: 18 ноября 2016.
- .
- .
- .
- (фр.) . Calcul Statique des Applications de Modules Parametres. Julien Signoles. JFLA 2003. (2010). Дата обращения: 9 декабря 2014. Архивировано из 4 ноября 2015 года.
- Robert Harper. (англ.) (2011).
- Andreas Rossberg. (англ.) (2013).
- Andreas Rossberg. (англ.) .
- 2021-07-06
- 1