ATS и зависимые типы

For you, when one sees emptiness
In terms of the meaning of dependent origination,
Then being devoid of intrinsic existence and
Possessing valid functions do not contradict.

-- Дже Цонкапа, "Сборник цитат для привлечения внимания", Союзпечать, 1402 г. (src)

В нашем детском саду всякий слышал о зависимых типах, что они умеют параметризоваться не только другими типами (как List a), но и значениями. Классический пример, который все приводят (и обычно на этом останавливаются), - это список с длиной. В синтаксисе ATS он описывается так:

datatype list (a:t@ype+, int) =
| list_nil (a, 0) 
| {n:nat} list_cons (a, n+1) of (a, list (a, n))

Для удобства рядом определяют

#define :: list_cons
#define nil list_nil

После чего выражение 5::6::7::nil будет иметь тип list(int, 3).
Т.е. list - это конструктор типа с двумя аргументами. Но в отличие от иных языков, где его kind был бы чем-то вроде * -> * -> *, здесь вместо звездочек более конкретные и информативные сущности: сорта. Тут стоит сделать небольшое отступление. Обычно языки программирования содержат в себе два подъязыка: один оперирует объектами времени выполнения (числа, строки, структуры...) и описывает поведение программы, второй оперирует объектами времени компиляции (типы, модули, шаблоны в С++...). Динамика и статика. В ряде динамически-типизированных языков второй подъязык почти отсутствует, поэтому они называются scripting languages, не будучи достойными называться programming languages. В статически-типизированных языках мы привыкли во втором подъязыке оперировать в основном типами: применяем конструктор типов List к типу Int, получаем тип List Int. В ATS мир статических конструкций намного богаче, и не все из них являются типами данных. Например, утверждения (props). Возникает понятие сорта статического терма (конструкции). Так, type - сорт, к которому относятся все типы размером со слово (указатель), включая все boxed типы. t@ype - сорт, к которому относятся типы других размеров, например unboxed структуры, а также банальный тип int, ибо на 64-битной платформе его размер отличается от размера указателя. prop - сорт логических утверждений, view - сорт утверждений в линейной логике, viewtype - сорт для типов, с которыми связаны некоторые линейные утверждения... Сортов всяких много, плюс можно еще определять свои. Есть также сорта int и bool, к которым относятся статические целочисленные и булевы термы. Например, в типе list(int, 3) тройка - это не рантайм-значение типа int, которое будет где-то в памяти во время исполнения программы, а компайлтайм-значение (терм) сорта int, существующее только во время компиляции. Оба аргумента list здесь - статические термы, но разных сортов: первый терм имеет сорт t@ype, второй - сорт int. Именно это указано при описании datatype list(a:t@ype+, int). Плюс после t@ype означает ковариантность, на ней сейчас останавливаться не будем.
( Read more... )