← На главную

Poly/ML разгоняет Isabelle и HOL

06.07.2026 22:28 · hackernews

Poly/ML — реализация языка Standard ML, которую изначально написали на экспериментальном языке Poly. С версии 4.0 она полностью совместима со стандартом ML97. Разработчики консервативны: не добавляют несовместимых расширений, только библиотечные — например, библиотеку тредов. Это делает Poly/ML надёжным выбором для крупных проектов вроде Isabelle и HOL.

Компилятор работает быстро. Есть интерфейс для вызова внешних функций (foreign function interface): можно загружать статические и динамические библиотеки и использовать их как Poly/ML-функции. Встроен символьный отладчик и отдельный интерфейс для программирования под Windows. Библиотека тредов даёт упрощённую версию Posix threads, адаптированную для Standard ML, — позволяет программам задействовать несколько ядер. Сборщик мусора тоже параллельный.

Документация по Basis-библиотеке включает глобальные значения, типы, структуры, сигнатуры и функторы. Более подробные материалы — на сайте SML Family. Poly/ML нативно поддерживает i386 (32 и 64 бита) и ARM (только 64 бита). На других архитектурах работает через интерпретатор байт-кода. Для вопросов и поддержки есть почтовая рассылка.

Читать оригинал →