Язык модулей ML

Язык модулей ML *

Система модулей, имеющая аппликативную семантику.

Язык модулей состоит из трёх видов модулей:

• структура (реализация сигнатуры, имплементаторы или пакеты)
• сигнатура (описание структуры, интерфейсы или спецификации пакетов)
• функтор

Идея состоит в назначении типа целому фрагменту кода.

Отношения между сигнатурами и структурами выстраиваются по схеме «многие-ко-многим», а не «многие-к-одному» или «один-к-одному». Сигнатура может описывать множество разных структур, а структура может соответствовать многим разным сигнатурам.

В ООП, абстракция обеспечивается посредством классов, которые совмещают в одной концепции сразу ряд возможностей, что затрудняет их формализацию. В отличие от классов, язык модулей ML полностью фокусируется на абстракции, предоставляя обширный спектр её форм и обеспечивая надёжную формальную базу. Он предоставляет возможности управления иерархией пространств имён, настройки интерфейсов, абстракцией на стороне реализатора и на стороне клиента.

Функторы являются функциями над структурами, то есть вычисляют новые структуры на основе уже вычисленных, естественно, в соответствии с определёнными сигнатурами.

При этом соблюдаются два требования:

• полная статическая типобезопасность зависимостей между компонентами разных модулей;
• возможность раздельной компиляции модулей (в том числе функторов, в том числе, если в программе нет ни одной структуры, которая могла бы быть передана данному функтору в качестве параметра).

Существуют полнопрограммно-оптимизирующие компиляторы, раскрывающие рамки модулей для значительного повышения быстродействия программ.

Окружение (environment) в ядре ML (Core ML) представляет собой коллекцию определений (типов, в том числе функциональных, и значений, в том числе функциональных и исключительных). Окружение имеет лексическую область видимости.

Структура (structure) представляет собой «материализованное» окружение, превращённое в значение, которым можно манипулировать.

Основным средством определения структур являются инкапсулированные объявления, то есть объявления, заключённые в синтаксические скобки struct...end

«Значением» этого инкапсулированного объявления является структура. Чтобы это значение использовать, необходимо назначить ему идентификатор.

Доступ к компонентам структуры может осуществляться посредством составных (или квалифицированных) имён.

Сигнатура (signature) представляет собой перечисление описаний элементов структуры, то есть интерфейс структуры. Каждый элемент этого перечисления называется спецификацией. Если в сигнатуре для значения x специфицирован тип t, то в структуре идентификатор x должен связываться со значением типа t. Можно понимать сигнатуру как своего рода «тип» структуры, но сигнатура не является типом в строгом понимании, так как тип представляет собой множество значений, а «значение сигнатуры» может содержать типы (которые в ML значениями не являются). Каждый идентификатор в сигнатуре должен быть единственен. Правило лексического затенения имён в сигнатурах не соблюдается, поэтому порядок их перечисления значения не имеет, но типы должны быть объявлены до их использования, поэтому традиционно их помещают в начало сигнатуры. Определение сигнатуры записывается в синтаксических скобках sig...end

Основным свойством сигнантур является то, что структуры могут сопоставляться (match) с ними. Структура является сопоставимой с данной сигнатурой, если она содержит как минимум перечисленные в сигнатуре типы, значения и вложенные структуры. Существуют две формы сопоставления структур с сигнатурами: прозрачное (transparent) и тёмное (opaque). Обобщённо возможность выбирать форму подписывания называется свойством полупрозрачности (translucency) сигнатур.

Разработчик может определить сигнатуру, описывающую разнообразные потоки данных (структуры данных с последовательным доступом), и назначить ей идентификатор. Собственная сигнатура структуры может обогащать (enrich) сигнатуру, с которой производится сопоставление. Одна структура в разных контекстах может сопоставляться с разными сигнатурами, а одна сигнатура может служить интерфейсом для разных структур. Сигнатура определяет класс структур. Разный «вид извне» для одной структуры, с разной степенью абстракции, можно обеспечить посредством нескольких сигнатур с разным набором спецификаций. Порядок следования объявлений не имеет значения и не влияет на сопоставимость структур с сигнатурами. Структуры могут вкладываться друг в друга. Естественно, сигнатуры позволяют описывать вложенные структуры. Сигнатуры можно включать (include S) друг в друга, последовательно обогащая интерфейс. Структуру можно открыть (open S). Это можно рассматривать как синтаксический сахар, служащий для удобства использования инкапсулированных в модуле определений.(Исчисление просвечивающих сумм Харпера — Лилибриджа ?)

Функтор (functor) представляет собой функцию над структурами, то есть функцию, которая получает структуру на входе и строит новую структуру. Иногда функтор наглядно рассматривают как «параметризованную структуру», то есть структуру, определение которой строится компилятором на основе некой другой структуры по заданным программистом правилам.

Сигнатура играет роль типа параметра функтора. Всевозможные структуры, которые могут быть сопоставимы с этой сигнатурой, играют роль значений, принадлежащих этому типу и передаваемых функтору для вычисления новых структур. Получаемая в результате применения функтора структура имеет свою сигнатуру (хотя, вообще говоря, она может и не отличаться от сигнатуры параметра).

Функторы позволяют типобезопасным образом описывать самые разнообразные формы взаимосвязей между компонентами программ. Реализуют обобщённые алгоритмы и управление зависимостями, что особенно полезно на этапе быстрого прототипирования. Автоматически расширяют функциональность, избавляют от рутинной работы при необходимости реализации одной и той же функциональности для разных типов. Например, если требуется определять множества из элементов разных типов данных, то в ML достаточно определить функтор, порождающий структуру, определяющую множество, на основе структуры, определяющей тип одного элемента. В других языках такого рода задачи решаются при помощи порождающего программирования. Инстанцируют модули с инкапсулированным изменяемым состоянием. Если структура инкапсулирует изменяемое состояние, и в программе требуется иметь несколько её экземпляров с независимыми состояниями, то функторы позволяют автоматизировать построение таких структур.

Некоторые программисты используют функторы вместо структур (то есть описывают функтор и определяют структуру как единственное его применение к заведомо известному параметру, а порой и функтор с пустым параметром). Такой подход на первый взгляд кажется излишеством, но на практике даёт два преимущества, способствующих повышению продуктивности разработчиков в крупных проектах.

Когда модули компонуются для создания новых, более сложных, возникает вопрос о согласовании абстрактных типов, экспортированных из этих модулей. Для решения этой задачи язык модулей ML предусматривает специальный механизм, позволяющий явно указать идентичность двух и более типов или структур («sharing constraint»).

Функторы высшего порядка

Для передачи нескольких структур необходимо построить дополнительную структуру-обёртку, включающую эти структуры, и описать соответствующую сигнатуру. Определение языка Standard ML для удобства предусматривает синтаксический сахар — несколько параметров могут быть переданы в виде кортежа, а построение охватывающей структуры и её сигнатуры компилятор осуществляет автоматически. Ядро ML предусматривает функции высшего порядка, и следование аналогии с ними на уровне модулей означает введение каррированной формы функторов. Фактически, единственное, что требуется реализовать в языке для обеспечения этой возможности — поддержку описания функторов в сигнатурах. Примером, показывающим удобство использования функторов высшего порядка, является реализация полноценных монадических комбинаторов. Поддержка отношений подтипизации, объектов, объектных типов и генераторов объектов означает, фактически, более «чистую» реализацию ООП, а возможности параметрического полиморфизма делает язык ещё более выразительным.

Язык модулей ML не обязан быть статичным! Есть проблема в статической проверке согласования типов, составляющей природу ML. Харпер и Лилибридж, построив идеализированную версию языка модулей первого класса с помощью теории зависимых типов и доказав, что проверка согласования типов для этой модели неразрешима, похоронили идею полнопрограммной оптимизации механизмов выведения и проверки согласования типов. Однако, со временем стали появляться альтернативные модели, использующие другие обоснования. Клаудио Руссо предложил простейший способ сделать модули первоклассными: дополнить список примитивных типов ядра языка типом «пакет» (package), представляющим собой пару (структура : сигнатура), а список выражений ядра — операциями упаковки и распаковки. Иначе говоря, изменяется только ядро языка, а язык модулей остаётся неизменным. Упаковка структур в пакеты и последующая распаковка позволяет динамически привязывать к идентификаторам разные структуры (в том числе вычисленные посредством функторов). При распаковке пакета структура может подписываться другой сигнатурой, в том числе более бедной. Явное присутствие сигнатуры в пакете снимает проблему выведения и согласования типов при динамической распаковке структуры. Это опровергает ранний тезис Харпера — Митчела о невозможности поднять структуры в ML до первоклассного уровня, не пожервовав разделением фаз компиляции и запуска и разрешимостью системы проверки согласования типов, поскольку в качестве обоснования, вместо зависимых типов первого порядка, используется расширение теории экзистенциальных типов второго порядка Митчела — Плоткина.

Вдохновившись F-преобразованием, Россберг внедрил операцию упаковки-распаковки модулей глубже в семантику языка, построив в результате монолитный язык, в котором функторы, функции и даже конструкторы типов являются в действительности одной и той же примитивной конструкцией, и не проводится различий между записями, кортежами и структурами — внутреннее представление языка представляет собой плоскую Систему Fω. Доказательство надёжности языка становится намного проще, чем традиционно для языка модулей (не требуется использование теории зависимых типов), обеспечивается поддержка «материализованных» (reified) типов в ядре языка, обеспечивающих языку выразительную силу на уровне систем с зависимыми типами (и опять же не требующих их наличия в метатеории), язык в целом получается одновременно выразительнее (позволяет более ёмко и точно описывать сложные системы) и проще (минималистичнее и единообразнее по своему составу). Язык получил название «1ML».

MixML — это язык модулей, построенный посредством соединения классического языка модулей ML МакКуина и формализации модели примесей (mix-ins) Брачи и Кука (Bracha & Cook). Авторами MixML являются Россберг и Дрейер.

Основная идея MixML проста: структуры и сигнатуры соединяются в единое понятие модуля, объединяющее определения и спецификации, как прозрачные, так и абстрактные.

Это делает возможным определение произвольных графов зависимостей в программах, в том числе цикличных. В частности, это позволяет выстраивать в функторах не только прямую параметризацию (зависимость выхода от входа), но и рекурсивную (зависимость входа от выхода), сохраняя при этом поддержку раздельной компиляции (в отличие от множества частных моделей, расширяющих язык модулей ML поддержкой рекурсии).

MixML реализует единую унифицированную нотацию для традиционно парных моделей семантики (для структур и сигнатур раздельно) и большого числа раздельных механизмов классического языка модулей ML, таких как:

• наследования (включения) сигнатур
• спецификации соиспользования
• двух форм подписывания сигнатур (прозрачного и тёмного)
• применения функторов

При своей простоте, язык модулей обладает выдающейся гибкостью и обеспечивает высокий уровень повторного использования кода.

Alice (Mozart/Oz), Ocaml – типичные представители. Haskell, являющийся наследником ML, не поддерживает язык модулей ML (монады и типы классов, первые выражают абстрактное поведение, в том числе моделируя изменяемое состояние в терминах ссылочной прозрачности; вторые служат средством управления квантификацией переменных типа, реализуя ad-hoc-полиморфизм). Класс типов есть не что иное как интерфейс, описывающий набор операций, чей тип задаётся независимой абстрактной переменной типа, называемой параметром класса. Следовательно, естественным представлением класса в терминах языка модулей будет сигнатура, которая, помимо собственно требуемого набора операций, включает также спецификацию типа (представляющую параметр класса).. Монада реализуется сигнатурой..Полноценные монадические комбинаторы особенно удобно реализовывать с использованием функторов высшего порядка.

С помощью языка модулей можно построить простую объектную модель с динамической диспетчеризацией.

Традиционно структуры представляются в компиляторе посредством записей, а функторы — функциями над такими записями. Однако, существуют альтернативные внутренние представления — например, семантика Харпера — Стоуна и 1ML.. Многие годы язык модулей ML на теоретико-типовом уровне рассматривался как приложение теории зависимых типов, и это позволило доработать язык и тщательно исследовать его свойства. В действительности, модули (даже в первоклассной роли) не являются «по-настоящему зависимыми»: сигнатура модуля может зависеть от типов, входящих в состав другого модуля, но не от входящих в него значений.

Некоторые языки предоставляют макро-подсистемы, позволяющие автоматически порождать код и гибко управлять зависимостями времени компиляции (Lisp, Си), но зачастую эти макро-подсистемы являются неверифицируемой надстройкой над основным языком, позволяя произвольное переписывание программы строка-к-строке.

Nemerle, MetaML *

Идея языка модулей состоит в том, чтобы крупномасштабная семантика программ повторяла семантику ядра ML (Core ML), то есть зависимости между крупными компонентами программ формулировались подобно зависимостям мелкого уровня. Соответственно, структуры представляют собой «значения» уровня модулей (module-level values); сигнатуры (называемые также «типами модулей» или «модулями-типами») характеризуют «типы» значений уровня модулей (module-level types), а функторы — «функции» уровня модулей. Аналогия, однако, не тождественная: как содержание модулей, так и отношения между модулями могут быть сложнее, чем в ядре языка.

Леруа — упрощение метатеории до прозрачных типов (не порождающих), аппликативные функторы. предложил реализацию обобщённой порождающей модели, позволяющей надстроить язык модулей ML над ядром произвольного (в достаточно широком диапазоне) языка со своей системой типов. Милнер, Харпер, МакКуин, Тофти — отдельная от ядра языка модель в составе Определения, доказательство её надёжности посредством так называемого порождающего пломбирования типов.

Семантика языка модулей совершенно не зависит от того факта, что ML является строгим языком — он может использоваться и в ленивых языках. Были предложены частные реализации языка модулей поверх ядер семантически иных языков (например, Prolog и Signal).