thedeemon | Dependent types in half of D

Посмотрел тут свежее выступление одного из активных пильщиков Идриса: David Christiansen - Coding for Types: The Universe Patern in Idris. Он там рассказывает, что вот в языках с зависимыми типами у нас типы вроде как первоклассные, можно их как обычные значения создавать, передавать и использовать, но вот паттерн-матчить по ним не положено - это отнимет бесплатные теоремы (id может начать возвращать 42 для всех натуральных аргументов, например) и помешает стиранию этих типов из рантайма. Не положено (надо бы сказать "нельзя", но по крайней мере несколько версий назад кое-какой простой матчинг по типам там работал), но порой очень хочется. Для этого есть дизайн паттерн: The Universe Pattern, заключающийся в том, что для интересующего нас набора типов мы делаем тип данных, их кодирующий (аки AST), где хотим матчимся по нему, а когда нужны сами типы, то просто отображаем их из этой кодировки. Например, есть у нас таблички, где поля могут быть строками, целыми или вещественными числами. Описываем это алгебраиком:

data Column = TEXT | REAL | INTEGER

и сразу делаем отображение в "настоящие" типы:

interpCol : Column -> Type
interpCol TEXT -> String
interpCol REAL -> Double
interpCol INTEGER -> Integer

Надо превратить поле одного из этих типов в строку? Пожалуйста:

printCol : (c : Column) -> interpCol c -> String
printCol TEXT    x = x
printCol REAL    x = doubleToString x
printCol INTEGER x = intToString x

Тут функция с двумя аргументами, где тип второго зависит от значения первого, т.е. зависимые типы как они есть. Можно вызвать printCol TEXT "hi", а можно printCol INTEGER 77, но printCol TEXT 77 уже не скомпилируется, будет ошибка типов.

Похожим образом он описывает схему таблички и отображение ее в тип кортежа, подходящего под эту схему:

Table : Type
Table = List (String, Column)

interp : Table -> Type
interp tbl = HList (map (interpCol . snd) tbl)

Как пример, вот так конкретными значениями описывается схема и данные одной таблицы:

PeopleSchema : Table
PeopleSchema = [("Name", TEXT), ("Hamsters", INTEGER)]

People : List (interp PeopleSchema)
People = [["David", 1], ["Edwin", 0]]

В этой схеме два столбца, interp PeopleSchema нам возвращает HList [String, Integer] - это тип гетерогенного списка из ровно двух элементов, где первый - строка, а второй - целое. Каждый такой список содержит один кортеж таблицы, например, ["David", 1]. Тут мог бы быть обычный тупл, но Дэвид просто задействовал HList, определенный им в том же выступлении несколькими минутами раньше.

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

countHamsters : List (interp PeopleSchema) -> Integer
countHamsters []             = 0
countHamsters ([_, h] :: xs) = h + countHamsters xs 

printRow : (tbl : Table) -> interp tbl -> String
printRow [] [] = "" 
printRow ((_, t) :: vs) (x :: xs) = printCol t x ++ "\t" ++ printRow vx xs

Тут countHamsters работает с таблицами фиксированной схемы, а printRow превращает в строку кортеж из произвольной таблицы со схемой tbl : Table, такой кортеж представлен значением, тип которого получается вычислением interp tbl. Оба аргумента - списки (обычный и гетерогенный), для каждого столбца из одного списка берется значение типа Column, определяющее тип очередного столбца, оно вместе со значением самого столбца передается в printCol. Дальше уже все тривиально.

Ну, зависимыми типами в Идрисе никого не удивишь, а вот задумывались ли вы о том, что зависимые типы давно уже пробрались в мейнстрим и присутствуют в С++ и его младшем и более милом мне собрате D? Но не во всем языке, а в половине - той, что доступна в compile-time. Попробуем пример Дэвида переписать практически один в один на D. В начале у нас был тип данных Column и отображение его в настоящие типы. Пишем:

enum Column { TEXT, REAL, INTEGER }

template interpCol(Column col) { // Column -> Type
    static if (col==Column.INTEGER) alias interpCol = int;     else
    static if (col==Column.REAL)    alias interpCol = double;  else
    static if (col==Column.TEXT)    alias interpCol = string;
}

Дальше была функция printCol с зависимым типом (c : Column) -> interpCol c -> String.

string printCol(Column c, alias x)()    if (is(typeof(x) == interpCol!(c))) {
    static if (c==Column.TEXT) return x;
           else                return x.to!string;
}

Это уже полноценная функция с двумя аргументами, возвращающая строку. Как и в оригинале, первый аргумент - с типа Column, а вот тип второго аргумента может быть разным, и статическая проверка убеждается, что этот тип это именно interpCol!(c), прямо как в исходнике на Идрисе. Передашь не тот тип - не скомпилируется. Секретный соус тут - двойной набор круглых скобок после printCol: аргументы перечислены в первых, это компайл-тайм аргументы. static if тоже делает свою работу в компайл-тайме.

Теперь научимся описывать схему таблиц, соответствующие данные, и функции, работающие с такими таблицами. Для компайл-тайм списков в D есть родной тип TypeTuple, исходно был нужен для шаблонов с переменным числом параметров. Может содержать самые разные вещи - типы, числа, строки, структуры, шаблоны... Для него в стандартной библиотеке есть готовые списковые операции вроде map/filter и пр. Нам пригодится map, называется staticMap. У TypeTuple есть один нюанс - они автоматически сплющиваются (список из двух списков превращается в один длинный), чтобы этого избежать сделаем обертку:

struct List(Things...) { // compile-time HList
    alias contents = Things;
}

alias getType(x...) = typeof(x[0]);
alias listValueTypes(lst) = List!(staticMap!(getType, lst.contents));

Компайл-тайм функция listValueTypes будет превращать список значений в список их типов, она пригодится дальше для тайпчекинга. В оригинале на Идрисе столбцы схемы описывались туплами (String, Column), и нужное значение Column извлекалось ф-ей snd. Мы же заведем для такой пары отдельную структуру, где можно извлекать все по имени.

struct NC(string A, Column B) { // named column
    alias name = A;
    alias col = B;
}

alias columnType(nc) = interpCol!(nc.col);
alias interp(tbl) = List!(staticMap!(columnType, tbl.contents));

В качестве Table (схемы) будет выступать List, содержащий прозвольное количество таких вот описаний столбцов. Отобразить описание столбца из схемы в настоящий тип поможет ф-я columnType, а interp отобразит список описаний столбцов в список настоящих типов данных, это как в оригинале на Идрисе. Вот так будет выглядеть превращение в строку кортежа произвольной таблицы:

string printRow(tbl, xs)()    if (is(listValueTypes!xs == interp!tbl)) {
    string[tbl.contents.length] res;
    foreach(i, x; xs.contents)
        res[i] = printCol!(tbl.contents[i].col, x);
    return res[].join("\t");
}

Как и в оригинале, у функции два аргумента: схема tbl и кортеж, имеющий тип, получаемый применением ф-ии interp к tbl. Их соответствие проверяется вычислением listValueTypes!xs и interp!tbl и их сравнением. Внутри мы проходим в цикле по столбцам и аналогично вызываем printCol, передавая описание типа столбца и значение данного столбца. На разных итерациях цикла тип значения x будет разный, заметьте.

Описание конкретной таблицы про хомячков и подсчет их общего количества будет выглядеть так:

alias PeopleSchema = List!( NC!("Name", Column.TEXT), NC!("Hamsters", Column.INTEGER) );

int countHamsters(rows...)() {
    int sum = 0;
    foreach(r; rows) {
        static assert(is(listValueTypes!r == interp!PeopleSchema));
        sum += r.contents[1];
    }
    return sum;
}

Функция countHamsters получает список с кортежами. Тут я использовал встроенный гетерогенный список, и поскольку каждый элемент в нем может быть своего типа, чтобы проверить соответствие данных схеме, проверка типа внесена внутрь цикла. Там для каждого кортежа r вычисляется список типов его элементов и сравнивается с результатом отображения нашей конкретной схемы в типы. Запустим на конретных данных:

void main(string[] argv) {
    alias People = TypeTuple!( List!("David", 10), List!("Edwin", 11) );
    int n = countHamsters!People;
    string s = printRow!(PeopleSchema, People[0]);
    writeln("hamsters: ", n, ", first row: ", s);
}

Оно компилируется и при запуске выводит:
hamsters: 21, first row: David 10
Полный исходник, с компиляцией и выводом, тут.

Причем данные (в том числе схему) можно было не указывать в исходнике, а поместить в отдельный файл, который распарсить, средства для этого имеются. Поскольку вся интересная работа происходит в компайл-тайме, использовать это можно как в интерпретируемых языках: пишешь "rdmd program.d arguments", программа быстренько компилируется и сразу запускается, отрабатывают сразу обе фазы, на первой из которых, как видно, у нас есть зависимые типы. Такое вот баловство.

Threaded | Top-Level Comments Only

From:

valentin budaev (from livejournal.com)

> Ну, зависимыми типами в Идрисе никого не удивишь, а вот задумывались ли вы о том, что зависимые типы давно уже пробрались в мейнстрим и присутствуют в С++ и его младшем и более милом мне собрате D? Но не во всем языке, а в половине - той, что доступна в compile-time.

Так если ограничиться compile-time, то это не зависимые типы, а всего лишь операторы над типами (lambda-w, а не lambda-P). Это тогда надо говорить, что lambda-w - "зависимые типы, но только в компайлтайме"?

Edited Date: 2015-07-29 02:21 pm (UTC)

From:

Dependent types in half of D

Page Summary

Style Credit

Expand Cut Tags