compile-time abstract nonsense in D
Oct. 5th, 2012 05:04 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
thedeemonДопустим, захотелось нам на обед монад. Монада - это troika из (эндо-)функтора и пары естественных преобразований, такие что.. Постойте, а что такое функтор? Это отображение объектов и стрелок категории в объекты и стрелки другой (или той же самой) категории, но не любое, а для которого выполнены определенные законы - сохранение identity морфизмов и сохранение композиций:
Identity: fmap id ≡ id
Composition: fmap (f ∘ g) ≡ fmap f ∘ fmap g
И по сути у нас в функторе два отображения - одно для объектов, второе для стрелок. В привычном нам применении этого дела в программировании первое отображение становится конструктором типов: всякому типу T оно сопоставляет тип F(T), например из Int делает List[Int]. Второе отображение становится функцией fmap с типом вроде (A -> B) -> (F(A) -> F(B)). Функциональные языки позволяют определить эти отображения, но вот проверку выполнения необходимых законов приходится делать в уме - компилятор этим не занимается.
А вот в D, с его умением выполнять код при компиляции, это сделать можно попытаться, хотя бы некоторое приближение.
Для примера опишем функтор "список", который внутри будет представлен массивом. Напомню, что передача статических параметров (например, типов), которая в иных языках заключается в угловые или квадратные скобки, в D заключается в !(), и если параметр один, то скобки можно опустить, оставив один восклицательный знак. Таким образом, List[Int] в D записывается как List!(int) или List!int.
struct тут используется не для описания структуры данных, а для группировки нескольких определений.
tmap - это первое отображение функтора: оно маппит объекты категории в другие объекты, т.е. одни типы данных в другие, в данном случае из типа T делается массив T[]. Реализовано это как eponymous template, компилятор tmap!(T) будет внутри раскрывать в T[]. Нам пригодится также функция unit, которая из конкретного значения некоторого типа T делает конкретное значение типа tmap!(T), в данном случае из значения х делается массив [x] с единственным элементом. Второе отображение функтора - стрелки в стрелки - т.е. для нас функции в функции. По-хорошему, оно должно возвращать функцию, но создание замыканий в compile-time в D не работает, поэтому мы ее подвергнем каррингу:
(A -> B) -> (F(A) -> F(B)) эквивалентно
(A -> B) -> F(A) -> F(B) эквивалентно
((A -> B), F(A)) -> F(B)
Т.е. fmap будет брать функцию типа A -> B и значение типа F(A) (т.е. список/массив из А) и возвращать F(B) (список/массив из В). Внутри она создает массив той же длины, что и аргумент, и заполняет его, применяя поэлементно переданную функцию f к элементам входного массива.
Теперь самое интересное. Я хочу в коде удостовериться, что переданная структура действительно описывает функтор. D позволяет навешивать на типы-аргументы весьма сложные проверки. Вот так будет выглядеть использование:
Эта функция не скомпилируется, если предикат isFunctor!(F) не вернет истину. Как он устроен?
Переданная структура F обязана содержать нужные функции (отображения) и они должны удовлетворять двум условиям сохранения. hasMember - предикат из стандартной библиотеки, простой compile time reflection. А вот проверки выполнения законов опишем мы:
Мы не можем физически проверить, сохраняется ли identity у всех-всех объектов категории (то бишь типов), но можно протестировать выполнение на нескольких, и поскольку они выбраны случайно, надеяться, что этой проверки будет достаточно. Т.е. это не полноценное доказательство, это юнит-тестинг, от которого зависит успешность компиляции. Опишем id - identity морфизм, возвращающий аргумент без изменений. Функция test берет значение х некоторого типа T, получает его образ fx типа F(T) (для этого и нужна была функция unit), дальше строит образ стрелки id c помощью fmap и тут же применяет его к fx. Если функтор правильный и identity отображает в identity, то в результат должен быть равен исходному fx. Имея такую функцию, мы ее запускаем с несколькими разными типами. Если везде истина, то весь предикат idCheck возвращает true, в противном случае мы можем вернуть false, но я сделал иначе: сразу прерываю компиляцию с осмысленным сообщением.
Аналогично делаем тест сохранения композиции:
Берем с потолка пару функций, берем образ некоторого значения, и сравниваем результаты применения к нему образа композиции исходных функций и композиции образов. Опять же, это лишь тест, не доказательство, но без его прохождения код не скомпилируется.
В таком виде все компилируется и работает успешно. Теперь, если в реализации fmap для списка например создавать массив чуть длиннее исходного:
auto bs = new B[n+1];
то получим при компиляции ошибку:
Вот тут полный текст программы с двумя различными функторами, к которым применяется единожды описанный предикат isFunctor.
Identity: fmap id ≡ id
Composition: fmap (f ∘ g) ≡ fmap f ∘ fmap g
И по сути у нас в функторе два отображения - одно для объектов, второе для стрелок. В привычном нам применении этого дела в программировании первое отображение становится конструктором типов: всякому типу T оно сопоставляет тип F(T), например из Int делает List[Int]. Второе отображение становится функцией fmap с типом вроде (A -> B) -> (F(A) -> F(B)). Функциональные языки позволяют определить эти отображения, но вот проверку выполнения необходимых законов приходится делать в уме - компилятор этим не занимается.
А вот в D, с его умением выполнять код при компиляции, это сделать можно попытаться, хотя бы некоторое приближение.
Для примера опишем функтор "список", который внутри будет представлен массивом. Напомню, что передача статических параметров (например, типов), которая в иных языках заключается в угловые или квадратные скобки, в D заключается в !(), и если параметр один, то скобки можно опустить, оставив один восклицательный знак. Таким образом, List[Int] в D записывается как List!(int) или List!int.
struct List { template tmap(T) { alias T[] tmap; } static tmap!T unit(T)(T x) { return [x]; } static tmap!B fmap(A,B, alias f)(tmap!A as) { auto n = as.length; auto bs = new B[n]; foreach(i; 0..n) bs[i] = f(as[i]); return bs; } }
struct тут используется не для описания структуры данных, а для группировки нескольких определений.
tmap - это первое отображение функтора: оно маппит объекты категории в другие объекты, т.е. одни типы данных в другие, в данном случае из типа T делается массив T[]. Реализовано это как eponymous template, компилятор tmap!(T) будет внутри раскрывать в T[]. Нам пригодится также функция unit, которая из конкретного значения некоторого типа T делает конкретное значение типа tmap!(T), в данном случае из значения х делается массив [x] с единственным элементом. Второе отображение функтора - стрелки в стрелки - т.е. для нас функции в функции. По-хорошему, оно должно возвращать функцию, но создание замыканий в compile-time в D не работает, поэтому мы ее подвергнем каррингу:
(A -> B) -> (F(A) -> F(B)) эквивалентно
(A -> B) -> F(A) -> F(B) эквивалентно
((A -> B), F(A)) -> F(B)
Т.е. fmap будет брать функцию типа A -> B и значение типа F(A) (т.е. список/массив из А) и возвращать F(B) (список/массив из В). Внутри она создает массив той же длины, что и аргумент, и заполняет его, применяя поэлементно переданную функцию f к элементам входного массива.
Теперь самое интересное. Я хочу в коде удостовериться, что переданная структура действительно описывает функтор. D позволяет навешивать на типы-аргументы весьма сложные проверки. Вот так будет выглядеть использование:
void useFunctor(F)() if (isFunctor!(F)) { writeln(F.stringof ~ " is ok"); // do something using F }
Эта функция не скомпилируется, если предикат isFunctor!(F) не вернет истину. Как он устроен?
template isFunctor(F) { enum isFunctor = hasMember!(F, "tmap") && hasMember!(F, "fmap") && hasMember!(F, "unit") && idCheck!(F) && compCheck!(F); }
Переданная структура F обязана содержать нужные функции (отображения) и они должны удовлетворять двум условиям сохранения. hasMember - предикат из стандартной библиотеки, простой compile time reflection. А вот проверки выполнения законов опишем мы:
//Identity: fmap id ≡ id template idCheck(F) { T id(T)(T x) { return x; } bool test(T)(T x) { auto fx = F.unit!T(x); auto fid_fx = F.fmap!(T,T, id!T)(fx); return fid_fx == fx; } static if (test(1) && test("abc") && test(2.0) && test(false)) enum idCheck = true; else static assert(0, F.stringof ~ " identity check failed"); }
Мы не можем физически проверить, сохраняется ли identity у всех-всех объектов категории (то бишь типов), но можно протестировать выполнение на нескольких, и поскольку они выбраны случайно, надеяться, что этой проверки будет достаточно. Т.е. это не полноценное доказательство, это юнит-тестинг, от которого зависит успешность компиляции. Опишем id - identity морфизм, возвращающий аргумент без изменений. Функция test берет значение х некоторого типа T, получает его образ fx типа F(T) (для этого и нужна была функция unit), дальше строит образ стрелки id c помощью fmap и тут же применяет его к fx. Если функтор правильный и identity отображает в identity, то в результат должен быть равен исходному fx. Имея такую функцию, мы ее запускаем с несколькими разными типами. Если везде истина, то весь предикат idCheck возвращает true, в противном случае мы можем вернуть false, но я сделал иначе: сразу прерываю компиляцию с осмысленным сообщением.
Аналогично делаем тест сохранения композиции:
//Composition: fmap (f ∘ g) ≡ fmap f ∘ fmap g template compCheck(F) { bool g(int x) { return x < 10; } string f(bool x) { return to!string(x); } bool test(int x) { auto fx = F.unit!int(x); auto left = F.fmap!(int, string, compose!(f,g))( fx ); auto right = compose!( F.fmap!(bool, string, f), F.fmap!(int, bool, g) )(fx); return left == right; } enum compCheck = test(1) && test(11); }
Берем с потолка пару функций, берем образ некоторого значения, и сравниваем результаты применения к нему образа композиции исходных функций и композиции образов. Опять же, это лишь тест, не доказательство, но без его прохождения код не скомпилируется.
В таком виде все компилируется и работает успешно. Теперь, если в реализации fmap для списка например создавать массив чуть длиннее исходного:
auto bs = new B[n+1];
то получим при компиляции ошибку:
Вот тут полный текст программы с двумя различными функторами, к которым применяется единожды описанный предикат isFunctor.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2012-10-05 12:19 pm (UTC)Следует отметить, что не существует препятствий для написания модульных тестов в haskell например.
no subject
Date: 2012-10-05 12:35 pm (UTC)no subject
Date: 2012-10-05 01:59 pm (UTC)no subject
Date: 2012-10-05 04:03 pm (UTC)А может "если такой-то код компиляется успешно, объявить то-то, а если нет - то объявить другое"?
no subject
Date: 2012-10-05 08:25 pm (UTC)no subject
Date: 2012-10-06 05:28 am (UTC)И тесты, и доказательства.
Хотя и доказательствам надо ещё научиться.
Но таки замечу, что называть агду "хацкелём на стероидах", это большая ошибка. Это очень другой язык. И попытки писать на нём "как на хаскеле" не получатся. По крайней мере, будет непросто и неудобно.
no subject
Date: 2012-10-06 10:34 am (UTC)Возможно наоборот легче будет, я имею ввиду писать на Хаскеле как на Агда?
no subject
Date: 2012-10-06 10:36 am (UTC)Это довольно разные языки, несмотря на некоторое внешнее сходство.
no subject
Date: 2012-10-06 04:32 pm (UTC)http://hackage.haskell.org/packages/archive/pkg-list.html#cat:testing
Тесты рядом с кодом.
no subject
Date: 2012-10-05 12:31 pm (UTC)Можно будет посмотреть. А какой-то спект задач, где D исключительно хорош, за время знакомства с ним нарисовался? Или это такой прентендент на мейстрим, который просто не взлетел?
no subject
Date: 2012-10-05 12:44 pm (UTC)Есть еще Mono-D для MonoDevelop, он покруче, как говорят.
Насчет где исключительно хорош - не знаю. Возможно, такой ниши и нет вовсе. Имхо, как замена перла/питона/руби/окамла для вспомогательных задач и небольших проектов (вроде обработчика логов и генератора картинок из недавнего поста) может пойти. Что-то очень большое или критичное я не буду советовать на нем делать, т.к. грабли все еще возможны, да и необходимость регулярно адаптировать codebase под изменения в языке в большом проекте будет минусом.
no subject
Date: 2012-10-05 04:37 pm (UTC)no subject
Date: 2012-10-05 06:13 pm (UTC)no subject
Date: 2012-10-05 06:47 pm (UTC)no subject
Date: 2012-10-06 04:29 am (UTC)no subject
Date: 2012-10-06 04:45 am (UTC)no subject
Date: 2012-10-06 05:12 am (UTC)no subject
Date: 2012-10-06 05:11 am (UTC)no subject
Date: 2012-10-06 09:34 am (UTC)no subject
Date: 2012-10-07 10:39 am (UTC)no subject
Date: 2012-10-06 05:30 am (UTC)no subject
Date: 2012-10-06 10:29 am (UTC)no subject
Date: 2012-10-06 11:11 am (UTC)no subject
Date: 2012-10-06 11:51 am (UTC)А что бы вы посоветовали посмотреть? Может у вас примеры кода есть? Это же этакий IO с доказательствами, если я правильно понял?
no subject
Date: 2012-10-06 02:41 pm (UTC)Идея в том, что к данным приклеиваются доказательства выполненности нужных свойств (состояния), причем эти доказательства работают в линейной логике: если функция принимает такое доказательство на вход, она его съедает, и больше им пользоваться нельзя, а можно только тем, что она вернет. Сохранить доказательство о старом состоянии тоже нельзя, т.к. они в силу линейности своей не размножаемые.
Например, см. про работу с памятью и файлами здесь:
http://thedeemon.livejournal.com/41388.html
Или кое-что здесь:
http://www.bluishcoder.co.nz/2012/08/30/safer-handling-of-c-memory-in-ats.html
http://www.bluishcoder.co.nz/2010/11/23/more-on-type-safety-using-c-and-ats.html
http://www.bluishcoder.co.nz/2010/06/02/safer-c-code-using-ats.html
no subject
Date: 2012-10-06 02:59 pm (UTC)no subject
Date: 2012-10-06 02:18 pm (UTC)это сильно, иметь юнит-тест, который для одного и того же кода то проходит, то фейлится.
no subject
Date: 2012-10-06 02:46 pm (UTC)Тут ситуация как с обычным юнит-тестом, но если он не пройдет, то основной код не скомпилится.
no subject
Date: 2012-10-06 04:49 pm (UTC)случайно - это с помощью random(), или
в первом случае - то, что я сказал, во втором - сам понимаешь.
no subject
Date: 2012-10-06 05:48 pm (UTC)no subject
Date: 2013-02-28 02:32 pm (UTC)