четвер, 17 січня 2013 р.

Uniqueness types in Agda

Сразу линк. Данная реализация уникальных типов на Agda базируется на явном управлении контекстом. Каждый оператор рассматривается как преобразователь контекста (Transformer в коде). Преобразователь характеризуется сигнатурой (Types) входа (то, что он употребляет, consumes, и удаляет с контекста) и сигнатурой выхода (то, что добавляет в контекст).