thedeemon | 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 означает ковариантность, на ней сейчас останавливаться не будем.

Как будет выглядеть функция определения длины списка типа list(int, n)? Можем ли мы просто вернуть n? Нифига. Нужно по-честному обойти весь список и подсчитать число элементов, ровно как в ML и родственниках. Потому что этот параметр n существует только во время компиляции, это статика, во время работы программы его нигде нет. Вот это очень важный для понимания момент. Как выразился

justbulat, "на типах вы можете сделать всё что угодно, при условии что этого никак нельзя будет наблюдать в окружающем мире. такой своеобразный кот шредингера".

Если в рантайме list(int,n) устроен просто как list int, то зачем эта n тогда вообще нужна? Чтобы логически связать между собой разные значения и выражения в программе и во время компиляции проверить выполнимость всех статических равенств и неравенств. Рассмотрим этот подход на примере, упомянутом в прошлом посте. По условию задачи нам нужно прочитать из текстового файла набор диапазонов IP адресов, и потом с его помощью фильтровать другие адреса. Нам понадобится функция, читающая из строки IP адрес и возвращающая его в виде unsigned int. Для строк в ATS есть несколько типов, отличающихся способом выделения памяти, но основной - это string n - строки длины n, живущие в управляемой куче и собираемые сборщиком мусора. ATS транслируется в Си, и там эти строки представлены обычными сишными строками - указателями char*. Наша функция будет пробегаться в цикле по строке, собирая из цифр октеты, а из них сам адрес. Кроме IP адреса она будет возвращать позицию, на которой закончился цикл, чтобы при чтении диапазона из двух адресов мы знали где в строке искать второй адрес. На псевдокоде в редуцированном до уровня ML синтаксисе ATS она выглядит так:

fn parseIP(s : string, start_pos : size_t): @(uint, size_t) = let
    fun loop(octet : uint, ip : uint, pos : size_t): @(uint, size_t) = 
      if s[pos]='\000' then @(ip * 256U + octet, pos) 
      else let val c = s[pos] in
        if c >= '0' && c <= '9' then loop(octet * 10U + uint_of_char c - 48U, ip, pos+1)
        else if c = '.' then loop(0U, ip*256U + octet, pos+1) 
        else @(ip*256U + octet, pos)
      end
in  
  loop(0U, 0U, start_pos)
end

Запись @(a,b) означает unboxed tuple - обычную структуру из двух безымянных полей. fn и fun - ключевые слова для задания функций, первое для нерекурсивных, второе для рекурсивных. Но вот беда: мы обращаемся за символами строки через s[pos], а [] определен так:

fun string_get_char_at {n:int} {i:nat | i < n} (str: string n, i: size_t i) :<> c1har
overload [] with string_get_char_at

В фигурных скобках тут описываются статические термы, и читается такое определение так: функция string_get_char_at для любого целого n и неотрицательного i, такого, что i < n, принимает на вход строку длины n и число i типа size_t и возвращает букву, отличную от нулевого символа, не производя никаких побочных эффектов. На отсутствие эффектов указывает :<>. В угловых скобках после : мы можем для функции явно описать такие сайд-эффекты, как оперирование ссылками на внешнюю память (ref), выбрасывание исключений (exn), возможное зацикливание (ntm) и пр. Можем не указывать, тогда просто будет :. Но если после : пустые угловые скобки, значит никаких эффектов нет и это доказано в теле функции. Тип c1har определен так:

stadef NUL = '\000'
typedef c1har = [c:char | c <> NUL] char c

stadef - определение статического (компайл-тайм) значения. Запись в квадратных скобках означает статический терм с квантором существования: всякое значение типа c1har представлено типом данных char, для которого существует такой символ "с" сорта char, отличный от нуля, служащий ему значением.

Итак, чтобы обратиться к некоторому символу строки по индексу, строка должна быть задана типом string n, индекс типом size_t i, а статические значения n и i должны быть связаны неравенством i < n. Поэтому тип нашей функции придется описать так:

fn parseIP {n:nat}{p0:nat | p0 <= n} (s : string n, start_pos : size_t p0): ...

nat - сорт неотрицательных целых, питерский вариант натуральных чисел.
Поскольку мы возвращаем позицию, где закончился парсинг IP адреса, то чтобы его использовать повторно на входе этой же функции для парсинга второго адреса в строке, нам надо возвращать не просто size_t, а size_t x, т.е. завести статический терм, означающий возвращаемое значение, и как-то связать его с термом, отвечающим за длину строки. В результате тип становится таким:

fn parseIP {n:nat}{p0:nat | p0 <= n} 
  (s : string n, start_pos : size_t p0): [endp:nat | endp <= n] @(uint, size_t endp)

Т.е. для любых натуральных n и p0, таких что p0 <= n, наша функция принимает строку длины n и стартовую позицию p0, и существует такое натуральное число endp, что endp <= n и наша функция возвращает пару из некоторого беззнакового целого (значение IP адреса) и позиции, равной endp. Аналогичные аннотации придется добавить к описанию типа внутренней функции-цикла.

Можем ли мы теперь использовать s[pos]? Еще нет, т.к. контракт на нее требует, чтобы индекс был строго меньше длины строки, а у нас p0 <= n. Тут нам пригодится функция из стандартной библиотеки:

fun string_is_at_end {n:int} {i:nat | i <= n} (str: string n, i: size_t i):<> bool (i == n)

Ее тип читается так: для любых целого n и натурального i, таких что i <= n, функция принимает строку длины n и индекс i и безо всяких сайд-эффектов возвращает булево значение, равное истине если i == n. Внутри она просто проверяет, находится ли в данной позиции нулевой символ. Если да, то действительно указанный индекс равен длине строки. Задействовав эту функцию, мы удовлетворим статическую проверку: если string_is_at_end(s, pos) вернет ложь, и мы знаем, что pos <= n, то в этой ветке программы pos < n, и можно наконец использовать s[pos]. Полный текст нашей функции выглядит так:

fn parseIP {n:nat}{p0:nat | p0 <= n} 
  (s : string n, start_pos : size_t p0): [endp:nat | endp <= n] @(uint, size_t endp) = let
    fun loop {pos : nat | pos <= n} .<n-pos>.
    (octet : uint, ip : uint, pos : size_t pos):<cloref0> [ep:nat | ep <= n] @(uint, size_t ep) = 
      if string_is_at_end(s, pos) then @(ip * 256U + octet, pos) 
      else let val c = s[pos] in
        if c >= '0' && c <= '9' then loop(octet * 10U + uint_of_char c - 48U, ip, pos+1)
        else if c = '.' then loop(0U, ip*256U + octet, pos+1) 
        else @(ip*256U + octet, pos)
      end
in  
  loop(0U, 0U, start_pos)
end

В ней осталась пара необъясненных WTF. Внутренняя функция-цикл помимо своих параметров использует строку s из внешней функции, поэтому это замыкание. <cloref0> в описании типа как раз говорит, что это создаваемое в куче (и собираемое сборщиком мусора) замыкание без сайд-эффектов. При трансляции в Си ATS заметит, что в замыкании всего один указатель, поэтому вместо создания записи в куче и ее собирания просто добавит в loop еще один параметр - указатель на строку. В функции loop хвостовая рекурсия, она будет развернута в goto и будет работать без пожирания стека.

А .<n-pos>. - это termination metric. Это выражение из статических натуральных термов, которое при каждом рекурсивном вызове функции обязано уменьшаться. Везде, где loop вызыает сама себя, длина строки n не изменяется, а параметр pos увеличивается на 1, поэтому величина n-pos с каждым вызовом уменьшается. Поскольку ни одно натуральное число не может уменьшаться бесконечно, указав такую метрику, мы доказываем, что функция loop завершается. Поскольку в ее типе мы явно указали отсутсвие сайд-эффектов, компилятор требует доказать отсутствие эффекта ntm - nontermination, поэтому эта метрика нужна.

Имея функцию парсинга одного адреса, можно легко сделать функцию парсинга пары адресов, разделенных запятой, как задано условием. Первая попытка:

        
typedef IPpair = @(uint, uint)

fn parseIPPair{n:nat}(s : string n): IPpair = let 
  val @(ip1, pos) = parseIP(s, 0) 
  val @(ip2, _) = parseIP(s, pos+1)
in 
  @(ip1, ip2) 
end

Фиг! Мы-то знаем, что в данных будет по два IP адреса в строке, но компилятор-то этого не знает. Он смотрит: parseIP возвращает позицию, которая меньше или равна длине строки, она сохраняется в pos. Теперь мы вызываем parseIP(s, pos+1) и получается, что во втором аргументе может возникнуть значение, которое на 1 больше длины строки, а контракт на функцию parseIP, описанный в ее типе, это запрещает. Действительно, у нас на входе могли оказаться некорректные данные с одним адресом в строке, и мы бы тут пытались обращаться за ее границы. Код с багами не компилируется! Придется исправить:

fn parseIPPair{n:nat}(s : string n): IPpair =
  let val @(ip1, pos) = parseIP(s, 0) in
    if string_is_at_end(s, pos) then @(ip1, 0U) 
    else let val @(ip2, _) = parseIP(s, pos+1) in @(ip1, ip2) end
  end

Из типа parseIP компилятор знает, что pos <= n, и если string_is_at_end(s, pos) вернула ложь, то pos <> n, а значит pos < n, следовательно pos+1 <= n и вызов parseIP(s, pos+1) легитимен.

Уфф. Продолжение следует...