Dependent types in half of D

[thedeemon]

Посмотрел тут свежее выступление одного из активных пильщиков Идриса: 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", программа быстренько компилируется и сразу запускается, отрабатывают сразу обе фазы, на первой из которых, как видно, у нас есть зависимые типы. Такое вот баловство.

Comments

[thedeemon.livejournal.com]

Где вы берете эти определения? Давайте возьмем тот же TAPL за основу, не будем тут придумывать чепухи.

Предполагать про лифтинг в SystemF - это и есть натягивание совы. Есть 1 и есть int, первое есть терм, второе тип. Есть интепретатор и есть компилятор, они оба сходятся, что 1 это терм. Но один из них умеет этот терм 1 отобразить в тип для второго обоих, например char[1]. Я рассматриваю не систему типов просто D (там завтипов нет), а систему типов интерпретируемого во время компиляции подмножества, это несколько отличающийся язык.

[valentin budaev (from livejournal.com)]

> Есть 1 и есть int, первое есть терм, второе тип.

С этим, конечно, никто не спорит. Речь идет о том что ваша "1" в соответствующих контекстах ведет себя в точности как тип, конечно не Int, а какой-нибудь Succ Zero.

То есть, понимаете, есть лямбда-исчисление, в нем нету списков или там чисел с булами, но они моделируются на лямбдах. В практически применимых языках у нас и инты и буллы и списки со всем остальным есть, для удобства, но при этом системы эквивалентны.

Потом мы берем и вводим лямбда-исчисление на уровне типов. И тут есть два варианта - либо оставить лямбду (как в хаскеле), и тогда для того чтобы написать что-либо нетривиальное надо быть мудаком, либо добавить туда все те же булы, инты, списки да и вообще всю копию нашего языка, на котором эта система типов хостится. В этом случае мы можем писать нетривиальные вещи и не быть мудаками - вот так вот сделали в D. Но так же как лямбда без интов эквивалентна лямбде с интами так и тут. Это эквивалентные системы, просто не надо кодировать типы руками.

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

Ага, понял. Но все равно не сходится - с точки зрения этого подмножества integer или bool - это значения, с-но на уровне типов там обычная типизированная лямбда.

[thedeemon.livejournal.com]

>Ага, понял. Но все равно не сходится - с точки зрения этого подмножества integer или bool - это значения, с-но на уровне типов там обычная типизированная лямбда.

Ура!
Там int и bool это и значения, и типы (т.к. использутся для "int sum = ..."). Ровно как и в Идрисе и подобных - там же тоже синтаксически только термы на самом деле, и терм : терм.
А вот что там (в CTFE подмножестве D) на уровне типов по-хорошему - вопрос мутный. Условный Идрис это или условный Питон - вот в чем вопрос.

[valentin budaev (from livejournal.com)]

> Там int и bool это и значения, и типы (т.к. использутся для "int sum = ...").

Ну так да, у вас же на уровне типов идет подмножество исходного языка, с-но, если в исходном типы есть - то и в этом будут. Получается, что на уровне типов мы имеем типы-значения и типы-типы (сорта), причем они совпадают в названиях, но не смешиваются, то есть это разные сущности. Смотрите ниже пример с лиспом, там динамический язык в компайлтайме по вашей логике зависимые типы имеет. Я при желании могу и в точности аналогичный D пример написать, лифтанув в 1-фазу ("компайлтайм" в терминологии Racket) типизированный диалект из 0-фазы, правда через костыль. Причем понятно же, что это тот же самый язык, что в 0-фазе, а раз он тот же самый - то и система типов та же самая, то есть простая типизированная лямбда. И в D таже логика, от того что вы язык "в компайлтайм лифтанули" он не стал другим языком (более выразительным).

[thedeemon.livejournal.com]

Коммент с примерами на рэкете куда-то пропал. В почте я вижу, а тут нет.

Ну вот мы и пришли к правильным вопросам, тут рядом уже обсуждавшимся.

[valentin budaev (from livejournal.com)]

Странно, я пост вижу, вот:
http://thedeemon.livejournal.com/102275.html?thread=1754499#t1754499

Здесь-то все просто, смотрите:
1. язык А есть подмножество языка В
2. если подмножество содержит фичу С, то надмножество содержит фичу С
3. язык А содержит зависимые типы
=> В содержит фичу С

значит, если на подмножестве D, доступном на уровне типов, есть зависимые типы, то они и в самом D есть

Вы согласны, как я понимаю, что это не так - значит неверна одна из трех посылок.

При этом, не противореча вашей логике, можно считать, что А = В (для D это не верно, вообще говоря, но можно сделать в Racket том же), тогда 1 и 2 становятся тавтологиями и единственным неверным утверждением может быть только 3.

Еще один момент. Допустим, у f действительно зависимый тип, допустим, это тип Х, как мне написать функцию g, которая будет принимать (или возвращать) функции типа Х и только их? Никак, потому что не получится записать этот Х, а значит его и нету.

[thedeemon.livejournal.com]

Увы, по ссылке мне ЖЖ показывает лишь наличие того коммента, но раскрыть его не дает.
http://stuff.thedeemon.com/lj/susp_cmnt.png
А без ссылки и наличия не видно.

На остальное позже отвечу. Тут уже первый пункт сомнителен - считать подмножеством или это разные языки просто.

[valentin budaev (from livejournal.com)]

Вот:

#lang typed/racket
(require (for-syntax racket 
                     racket/syntax))

(begin-for-syntax
  
  (define/contract (f x)
    (->i ([x boolean?]) 
         [result (x) (if x integer? string?)])
    (match x
      [#t 1]
      [#f "no"]))
  
  (define (f-proxy stx)
    (syntax-case stx ()
      [(_ arg) #`#,(f (syntax-local-eval #'arg))])))

(define-syntax f f-proxy)

(: x Integer)
(define x (f (< 1 5)))

(: y String)
(define y (f (> 1 5)))

здесь тайпчек, как и должно быть, в компайлтайме, аргументы f вычисляются в компайлтайме, выражение (f ...) в итоге тайпчекером рассматривается либо как имеющее тип Integer, либо как String (в зависимости от аргумента), если типы х и y местами поменять - тайпчекер даст ошибку типов, если выражение окажется не boolean? - contract blame, усли нарушится указанная в [result (x) (if x integer? string?)] семантика - contract blame, ессно это все в компайлтайме, при применении f к аргументу.

Вопрос: это получились зависимые типы? Но я-то точно знаю, что там динамика :)

[thedeemon.livejournal.com]

Я с Рэкетом не знаком, и тут не все конструкции понимаю.
Но один вопрос: почему проверяемое при компиляции "(: x Integer)" это динамика, а "x : Integer" в другом языке - статика?

[valentin budaev (from livejournal.com)]

> Я с Рэкетом не знаком, и тут не все конструкции понимаю.

На эти куски:
(define (f-proxy stx)
(syntax-case stx ()
[(_ arg) #`#,(f (syntax-local-eval #'arg))]))

и:
(define-syntax f f-proxy)

можете не обращать внимания, это просто обертка, чтобы выглядело как в ваших примерах, (begin-for-syntax exprs) - значит, exprs будут выполнены во время компиляции (на самом деле в +1 фазе относительно visite в enclosed module, а не при компиляции, но для нашего обсуждения эта разница в семантике некритична)

(define/contract (f args ...) contract exprs ...) - определяет функцию (lambda (args ...) exprs ...) с именем f и контрактом (есс-но проверяющимся при вызове ф-и, то есть для обычной (не в begin-for-syntax) функции это рантайм) contract. Остальное, полагаю, и так ясно.

> Но один вопрос: почему проверяемое при компиляции "(: x Integer)" это динамика, а "x : Integer" в другом языке - статика?

Не совсем понятен вопрос. (: x Integer) проверяется в компайлтайме тайпчекером, с-но _на уровне компайлтайме_ у нас динамика, если тайпчекер написан на динамике, и статика, если он написан на статике. В случае Racket тайпчекер - просто одна из библиотек, и он написаном на самом Racket (который динамический) и на том же Racket написан макрос f. Вопрос таокго, что такое (: x Integer) в D мне кажется совершенно неинтересным - ведь в D можно написать тайпчекер на чем угодно. Интерес представляет, на каком языке написана f (то самое "доступное при компиляции подмножество"). В Racket - это Racket (вот прям совсем в точности он же, на все 100%, по-этому вопросы типа "а является ли оно подмножеством или не подмножеством или еще что...." нас не волнуют), и этот язык совершенно точно динамический.

[thedeemon.livejournal.com]

Я ничего не понял. Какая разница на чем тайпчекер написан. Разница между динамическими и статическими типами отличается от разницы между динамической и статической проверкой типов, кстати.

[valentin budaev (from livejournal.com)]

> Какая разница на чем тайпчекер написан.

Он написан на "подмножестве языка, доступном при компиляции". Так что если мы обсуждаем "подмножество языка, доступное при компиляции", то мы обсуждаем язык, на котором написан тайпчекер.

> Разница между динамическими и статическими типами отличается от разницы между динамической и статической проверкой типов

Чем?

[udpn.livejournal.com]

Вот к моему удивлению, я сегодня с Валентином согласен. Совсем не зависимые типы это в D, а другая, в чём-то схожая система типов. В завтипизированных языках можно полагаться в типах на зависимости от термов, значение которых в компайл-тайме не известно. Собственно, ради работы такой ереси и нужны все эти пруфы с тотальностью. Я сейчас могу даже привести пример задачи, которую можно решить завтипами, но нельзя в D.

Программа должна вводить из консоли сначала число n, а затем два списка длины n из натуральных чисел, и искать их попарную сумму. Если мы захотим для подобного zip взять тип в духе

zip : {A, B, C : Set}{n : N} -> (A -> B -> C) -> List n A -> List n B -> List n C

то в завтипизированном языке мы сможем сначала построить доказательство того, что мы из консоли ввели ровно n чисел в каждом списке (потому что в противном случае мы вместо вычисления суммы писали юзеру диагностик какой-нибудь), а затем, используя эти пруфы, вызвать такую zip с заранее неизвестным n.

В D же ничего подобного построить нельзя, потому что это просто система с иерархией юниверсов, где 1 имеет тип Set n для некоторого ограниченного сверху числа n. Наличие иерархии юниверсов ещё не делает язык завтипизированным. У подобной системы, впрочем, есть определённая прелесть, например, я хорошо представляю как её компилировать (Set 0 в рантайм, остальное в компайлтайм), в отличие от завтипизированных языков, где для этого в Coq есть разделение на Set и Prop, а в Agda, если я правильно понял, proof irrelevance.

[thedeemon.livejournal.com]

Ну вот, еще один не понял вообще о каком языке идет речь.
Я нигде и не говорил, что в D есть зависимые типы.

[thedeemon.livejournal.com]

А с Валентином я тоже согласен, но по несколько другим пунктам, он лучше меня понял.

[zeit-raffer.livejournal.com]

Я, конечно, извиняюсь, что вклиниваюсь в вашу оживленную беседу, но зачем всерьёз разговаривать с юродивыми? После первых пары комментов уже всё с человеком было ясно...

[thedeemon.livejournal.com]

Да ладно, хороший человек и совершенно справедливо меня на чистую воду вывести старается. Да и не первый раз с ним беседуем.

[zeit-raffer.livejournal.com]

Ну я не в том смысле, чтобы классифицировать данного человека, меня больше интересует это как явление. Не так редко встречаются подобные ветки, иногда на 10, иногда на 100 комментов. Оба собеседника вполне высказывают свою позицию в первых двух комментах, а потом ходят по кругу, повторяя свои аргументы. Я видел много таких диалогов, но не видел еще ни разу, чтобы кто-то кого-то таким образом убедил. По правилам шахмат, многократное повторение позиции должно защитываться как ничья обоим соперникам. Могу я спросить, зачем они (и Вы сейчас) это делают(-ете)?

[thedeemon.livejournal.com]

Рекреационный спорт. :)