12/03/2021, Alexander Tchitchigin¶
https://hal.inria.fr/hal-01499946/document “A modular module system”, Xavier Leroy
Утверждение, что (ML-style) система модулей не зависит от “базового” языка программирования, и может быть реализована почти для любого, а не только ML, широко известно и озвучивалось в литературе. Данная статья приводит конструктивное доказательство этого тезиса, реализуя такую (слегка упрощённую) систему модулей, в виде, явно параметризованном относительно синтаксиса и системы типов базового языка.
Несмотря на ряд упрощений по сравнению с системой модулей того же Standard ML, представленная модельная система содержит (и корректно реализует) все базовые возможности, включая структурную типизацию модулей, абстрактные типы, функторы, зависимость (типа) результата функтора от (типа) аргумента а также равенства между (абстрактными) типами.
All in all, module type matching resembles subtyping in a functional language with records, with some extra complications due to the dependencies in functor types and signatures.
Статья составлена в духе Literate Programming, перемежая пояснительный текст и реальный рабочий код на языке OCaml. Реализация системы модулей ML с помощью системы модулей ML отсылает к традиции метациркулярных интерпретаторов Лисп. Леруа выражает надежду, что такой способ представления материала не только не запутает читателя, но и дополнительно прояснит связь конкретного и абстрактного синтаксиса как и практическую полезность (и даже необходимость) всех возможностей представленной системы. (По-видимому, метациркулярность системы не оставила Лисперов равнодушными, что привело к появлению реализации MiniML с полноценной системой модулей на Scheme: http://wiki.call-cc.org/eggref/4/miniML 😊)
Для иллюстрации приводятся два примера “надстраивания” реализованной системы модулей над “упрощённым C” в качестве императивного (процедурного) базового языка и Mini-ML в качестве функционального, приближенного к используемым на практике, в частности, реализующего типы высших порядков (Higher-Kinded Types).
Кратко обсуждаются вопросы (модульной) компиляции таких модулей. Упоминаются три основных варианта: компиляция самих модулей в виде структур данных, а функторов — в виде (полиморфных) функций, специализация функторов для всех применений в духе C++ templates и полное стирание модулей во время компиляции (аналогично девиртуализации вызовов методов в ООП). Но за деталями интересующиеся читатели отсылаются к соответствующим публикациям.
В заключительной части Леруа обсуждает ряд расширений модельной системы модулей — как реализованных на практике, так и не до конца проработанных даже в теории — но уже без фактической реализации.
Таким образом, статья представляет собой практическое введение в ML-style системы модулей и связанные вопросы, полезное как для пользователей таких систем, так и для авторов языков программирования, желающих реализовать собственную систему модулей. 😊
#leroy #modules #classic #ocaml #sml
13/02/2021, Alexander Tchitchigin¶
https://grosskurth.ca/bib/1997/cardelli.pdf “Program Fragments, Linking, and Modularization” Luca Cardelli.
Статья поднимает вопрос корректности раздельной компиляции и линковки, и потому — я считаю — обязательна к прочтению для всех авторов языков программирования! 😃
Уже во введении на простейшем примере создания воображаемой программы, состоящей всего из двух модулей, разрабатываемых независимо, автор иллюстрирует, наверное, все проблемы, при этом возникающие. Между делом Карделли упоминает публичные репозитории артефактов (типа Maven Central или Nuget. Напомню, что статья опубликована в 1996 году!). Многие из обозначенных проблем линковки раздельно скомпилированных модулей до сих пор не решены ни в мейнстримных, ни в исследовательских языках.
В качестве основного результата Карделли предлагает, вероятно, первую формальную модель раздельной компиляции и последующей линковки, позволяющую строго рассмотреть вопрос о корректности этих процессов. Корректность в этом смысле приведённой простейшей системы модулей для просто типизированного лямбда-исчисления (в качестве модельного языка) формально доказывается. Автор, конечно же, указывает на необходимость расширения модели как в сторону более развитых языков (параметрический полиморфизм, ООП), так и в сторону более сложных систем модулей (параметризованные модули, “функторы” в духе Standard ML, первоклассные модули). Существуют ли такие работы, непосредственно продолжающие это исследование, мне не известно.
Однако, в качестве related work и дальнейшего чтения могу указать на работы по формализации (и доказательству корректности) раздельной компиляции для языка C в рамках проекта CompCert.