субота, 26 жовтня 2013 р.

Dependent types. Don't need proofs

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

А что, если бы не было изоморфизма Карри-Ховарда? Никаких теорем, никаких доказательств, никаких HoTT и так далее. Но что бы тогда осталось? Вы не поверите! Осталась бы суть... а именно зависимые типы.

вівторок, 8 жовтня 2013 р.

Безопасный void* на Agda

В стандартной библиотеке Хаскеля есть тип Dynamic, который состоит из значения, тип которого как-бы утрачен, и тега, который представляется типом TypeRep. TypeRep — это по сути дерево из строк, среди которых есть имя пакета с версией, имя модуля, имя самого типа, и так для всех составляющих. Его можно использовать как уникальный идентификатор типа. Так он и используется в Dynamic, если TypeRep'ы одинаковы, unsafeCoerce'им.

Это конечно все очень удобно, но больно напоминает void*. По сути оно таким и является, даже похоже менее безопасным чем C++ RTTI (поскольку TypeRep можно задать самому, а к C++ typeid прямого доступа нет). Ну и как водится решил я написать такой TypeRep, который позволил бы безопасно делать то же. На Хаскеле сразу не получилось, по этому решил написать прототип на Агде. Круто:) на Агде пишем прототипы для Хаскеля. Заодно пришлось написать платформу для эмуляции Хаскельных type class'ов на Агде.