Показ дописів із міткою type representation. Показати всі дописи
Показ дописів із міткою type representation. Показати всі дописи

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

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

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

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