← На главную

Книга знакомит с типами и доказательствами в ATS

03.11.2026 19:25 · hackernews

Hongwei Xi опубликовал «Introduction to Programming in ATS» — учебник по языку, который сам автор характеризует как богатый и синтаксически, и по набору возможностей. Книга не ограничивается базовым синтаксисом: её задача — познакомить читателя с основными механизмами ATS и показать, как они используются в программах.

В начале рассматриваются функциональное программирование, простые типы и рекурсивно определяемые типы данных. Дальше идут параметрический полиморфизм, зависимые и линейные типы. Отдельная часть посвящена доказательству теорем, совмещению программирования с доказательствами — подходу PwTP — и программированию на основе шаблонов. В оглавлении также представлены взаимодействие с C, исключения и другие эффективные возможности, массивы, уточнение типов данных, система доказательств ATS/LF, views и viewtypes, а также ручное выделение и освобождение памяти.

Первый практический пример показывает минимальный шаблон программы из одного файла. В нём подключаются atspre_define.hats и atspre_staload.hats: эти директивы дают компилятору atsopt доступ к внешним библиотечным пакетам и определениям библиотечных функций. Точкой входа служит main0, а в шаблоне оставлено место для кода пользователя. Этот пример задаёт практический формат изложения: языковые конструкции сопровождаются работающими фрагментами программ.

Автор не требует от читателя формального знакомства с программированием, но прямо предупреждает, что книга будет трудной для человека без заметного практического опыта. Причина прежде всего в плотности материала и количестве тем: от обычных функций учебник переходит к типам, связывающим код с логическими свойствами, и к механизмам работы с ресурсами. Поэтому это скорее последовательное введение для подготовленного разработчика, чем лёгкий первый учебник по программированию. Книга распространяется как документация ATS; разрешается печатать её для личного использования. На сайте размещены отдельные HTML-страницы глав, между которыми можно переходить последовательно или выбирать нужную тему через оглавление.

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