#prog #ocaml #article

Статья о том, как закодировать полиморфизм высших сортов (higher-kinded polymorphism) в языке, который поддерживает лишь полиморфизм сортов первого порядка. Конкретно в этой статье — на примере выражения в OCaml примеров из Haskell.

С одной стороны, на мой взгляд, данный подход довольно сильно завязываются на фишки именно OCaml. С другой стороны, подобный эрзац-HKP на Rust уже делали.

#prog #ocaml #article

Не смотря на то, что исторически property-based testing применялось для тестирования чистых функций, технически ничто не мешает тестировать и функции с некоторыми побочными эффектами. Тем не менее, при переносе этого подхода на компиляторы возникает очевидная проблема: все сколько-нибудь полезные программы обладают побочными эффектами, и языки далеко не всегда определяют порядок вычислений достаточно точно, чтобы предсказать вывод обладающей побочными эффектами фрагмента программы исключительно по исходному коду. Одним из таких языков является OCaml: среди его реализаций есть как те, которые вычисляют порядок аргументов слева направо, так и те, которые вычисляют справа налево. Это делает генерацию исходных программ с целью тестирования несколько затруднительной, поскольку вывод даже корректно скомпилированной программы может зависеть от реализации.

В статье Effect-Driven QickChecking of Compilers авторы решили эту проблему, спроектировав генератор, который создаёт лишь программы, вывод которых не зависит от порядка вычислений. Сделали они это путём введения рудиментарной системы эффектов (попутно доказав её корректность) и архитектуры генератора, позволяющей на ранних этапах генерации отбрасывать альтернативы, которые бы привели к зависимости от конкретного порядка вычислений. Вместе с генератором они также спроектировали минификатор, позволяющий минифицировать программы с сохранением полезного свойства независимости (впрочем, это получилось скорее автоматически ввиду того, что это свойство было закодировано в эффектах, а элементарные операции минификации сохраняли тип).

Генератор получился достаточно ограниченным. Он генерирует только весьма узкое подмножество всех программ (в частности, никакого полиморфизма, ни по типам, не по эффектам), и, в частности, генерирует только программы, которые гарантированно завершаются. Вдобавок, введённая система эффектов отслеживает исключительно сам факт наличия побочного эффекта, но не его конкретную разновидность. Тем не менее, даже такое ограниченный инструмент оказался полезным на практике. Используя реализацию QuickCheck для OCaml для свойства "для любой программы, сгенерированной генератором, вывод этой программы при использовании двух разных компиляторов одинаков", авторы смогли обнаружить четыре новых бага, а также найти два уже ранее известных.

P. S.: единственное, что меня смущает — это лемма об ослаблении контекста типизации в разделе, в котором доказывается корректность системы типов с эффектами:

If
∆;Γ,(x : τ′),Γ′ ⊢ e : τ & φ and τ′′ ⊑ τ′
then
∆;Γ,(x : τ′′),Γ′ ⊢ e : τ & φ

или, если словами, произвольный тип внутри контекста типизации можно заменить на тип с более слабым эффектом. Лично мне это не кажется очевидным от слова совсем.

#prog #ocaml

Офигеть, Multicore OCaml таки вышел

discuss.ocaml.org/t/ocaml-5-0-0-is-out/10974

(thanks @covalue)

#prog #ocaml #article

Oxidizing OCaml (1, 2, 3) — серия из трёх статей, описывающая дополнения в OCaml, позволяющие добавить в язык некоторые из присущих Rust концептов — владение, лайфтаймы и уникальные ссылки — и таким образом привнести довольно конкретные преимущества для написания корректных и более экономно использующих ресурсы программ. Всё это — через систему аннотаций режимов (mode), ортогональных системе типов и друг другу и потому не влияющих на разрешимость вывода типов (для авторов предложенных изменений это важно).

Настоятельно советую прочитать оригинальные статьи, но что-то я перескажу и тут.

Первая статья: Oxidizing OCaml: Locality. В ней рассказывается про режим локальности значений. В отличие от полиморфных ссылок Rust, этот режим поддерживает лишь два возможных варианта: global (вариант по умолчанию) и local.

Времена жизней глобальных (global) значений могут жить независимо от исполнения различных функций. Как следствие, компилятор вынужден все подобные значения класть в кучу и делегировать управление временем их жизни рантаймовому сборщику мусора. На использование локальных (local) значений накладываются ограничение: именно, подобные значения не могут пережить функцию, в которой они находятся. В терминах escape analysis это значения, которые не escape текущую функцию. Так как подобные ограничения излишне строги, язык предоставляет возможность явно выделить local значение во внешнем регионе вместо текущего. Так как escape analysis — это не какая-то новая вещь, определить локальные значения возможно статически во время компиляции.

Введение этого режима даёт два преимущества.

Во-первых, локальные значения можно выделять на стеке — и в случае OCaml это несколько более существенное преимущество, поскольку стековый аллокатор не обязан использовать под стек ту же память, что и стек потока управления. Это позволяет достигнуть более высокой производительности, поскольку использование стекового аллокатора не триггерит использование сборщика мусора, а также естественный LIFO паттерн доступа к стековой памяти приводит к лучшей утилизации кеша процессора. Для сравнения, в текущей реализации OCaml сборщик мусора поколенческий, и для младшего поколения используется кольцевой буфер. Малая сборка мусора относительно дешёвая, но каждый объект, который переживает её, уходит в кучу для старых объектов, обход которой дороже. Вдобавок, использование кольцевого буфера повышает шанс, что аллокация новых значений приведёт в вымыванию из кеша старых значений.

Во-вторых, локальность позволяет строить более корректные API. В качестве примера в статье приводится функция Core_unix.with_file. Эта функция принимает на вход имя файла и коллбек. Семантика достаточно проста: функция открывает файл с указанным именем, отдаёт дескриптор коллбеку, после чего закрывает файл и возвращает результат вызова коллбека. Всё бы ничего, но OCaml — не чистый язык, а потому переданный коллбек может захватить внешнее изменяемое состояние и сохранить файловый дескриптор в нём. Попытка воспользоваться этим дескриптором приведёт в лучшем случае к ошибке, а в худшем — к взаимодействию с некоторым другим файлом, если дескриптор будет переиспользован. Локальность позволяет решить эту проблему. Указав режим аргумента коллбека, как local, мы наложили на коллбек требование, что аргумент не утечёт. Таким образом, мы можем быть уверены, что после завершения коллбека аргумент существует лишь в with_file, и потому его можно передать в close, не опасаясь ошибок.

Как вы могли заметить, local лишь накладывает ограничения на использование, а потому, по идее, можно передать global значение туда, где ожидается local значение. И действительно, на вариантах режима локальности есть отношение субтипизации: global является подтипом local.

Автор отмечает, что локальность с успехом используется на практике.

У читателя может возникнуть резонный вопрос: стоит ли добавление режимов уникальности (и линейности) добавленной сложности языка, особенно с учётом того, что в OCaml и так есть изменяемые поля? Это совершенно справедливый вопрос, и до недавнего времени перевес был бы не в сторону дополнительных фич. Однако релиз Multicore OCaml добавил в язык параллельность, и как следствие — потенциальные гонки данных. Конкретно в случае с OCaml это несколько меньшая проблема, чем в, скажем, C(++) и Rust, поскольку в модели памяти OCaml гонки данных не приводят к неопределённому поведению. С другой стороны, они всё ещё могут с легкостью привести к логическим ошибкам.

Третья статья: Oxidizing OCaml: Data Race Freedom. Как следует из названия, в этой статье рассказывается про API, который позволяет статически убедиться в отсутствии гонок данных в программах на OCaml. К сожалению, эта статья заметно сложнее предыдущих, поэтому вместо своего пересказа я пробегусь по ней тезисно.

Для того, чтобы дать подобные гарантии, вводится новый режим, с возможными значениями sync и nosync. Значения с первым режимом допускают конкуретный доступ на запись и потому могут быть безопасно разделены между доменами (термин OCaml для обозначения независимого потока исполнения, который могут исполняться параллельно). Режимом sync, очевидно, обладают неизменяемые значения. Также им обладают exclusive значения в силу своего инварианта. Все остальные значения являются unsync.

Наиболее простой способ избавиться от гонок данных — обернуть данные в мьютекс. В представленном API конструктор мьютекса принимает unique аргумент, что логично: невозможно защитить доступ к данным при помощи мьютекса, если можно получить к ним доступ в обход мьютекса (в Rust Mutex::new принимает аргумент по значению). (А ещё конструктор требует, чтобы аргумент был sync, и мне не особо понятно, почему).

Для доступа к содержимому мьютекса используется функция with_lock, в том же bracket стиле, что и with_file. Она захватывает мьютекс, вызывает переданную функцию на охраняемом значении, отпускает мьютекс и возвращает результат вызванной функции. Для обеспечения корректности она требует, чтобы переданный коллбек принимал аргумент в режиме local exclusive (то есть не более одного доступа за раз и аргумент не утекает), а сам коллбек принимается, как local.

Другой механизм, который вводится в статье — это капсулы, которые позволяют оперировать замкнутым графом unsync значений (без указателей наружу) и при этом предоставлять синхронизируемый доступ. Их реализация сильно полагается на фичи OCaml, а конкретно — первоклассные модули с экзистенциальными типами. Скрытие экзистенциального типа внутри первоклассного модуля позволяет добиться генеративности: каждый новый экземпляр капсулы получает свой отдельный внутренний экзистенциальный тип.

Этот тип используется для предоставления доступа к содержимому капсулы. Именно, доступ к содержимому капсулы происходит через связанный тип указателей (серьёзно, в статье так и называется Ptr). Для любых манипуляций с тем, на что этот указатель указывает, требуется связанный с капсулой ключ, и доступ к этому ключу является эксклюзивным. Так как каждая капсула получает свой собственный ключ, получить доступ к содержимому указателя капсулы можно лишь через ключ этой капсулы — иначе типы не совпадут. Потому вместо синхронизации доступа к графу объектов нужно синхронизировать лишь доступ к ключу. Так как ключ не хранит никаких данных, в рантайме он ничего не стоит, а защищающий его мьютекс вырождается в атомарное булево значение.

Этот тип синхронизации не имеет прямого аналога в Rust. Наиболее близкий API — это GhostCell, но в OCaml он гораздо удобнее. И ещё: тип Rc<T> не является Send (и Sync) в Rust, поскольку передача копии Rc в другой поток привела бы к возможности неатомарного доступа к счётчикам ссылок из разных потоков. С другой стороны, это не было бы проблемой, если бы весь связный граф из Rc можно было бы передать целиком из одного потока в другой — и, похоже, именно это в какой-то мере и можно сделать с предложенным в статье API.