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

Uniqueness types in Agda

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

Преобразователи можно (и нужно) объединять: выход одного к входу другого. Конечно же сигнатуры (выход первого и вход второго) могут не совпадать или перекрываться, поэтому для тех имен, что совпадают типы должны совпадать тоже, для этого необходимо построить соответствующее доказательство.
Контекст представляется в виде полиморфного трехэлементного списка (Имя, Тип, Значение) и доказательства, что имена не повторяются. Может не самый удачный выбор, но рабочий.
Разработчик высокоуровневого API, использует существующее низкоуровневое API (на С, например, написанное) и обогащает его типами и вся ответственность за созданное ложится на него. Разработчик использует модули Values (основные определения и леммы), Context (парочка вспомогательных функций и обертка над Значениями, чтоб пользователь высокоуровневого API не мог добраться до содержимого Контекста вручную) и Transformer (преобразователь и соединитель преобразователей).
Пользователь высокоуровневого API при условии не использования модуля Context, может быть уверен, что он все делает безопасно. (Он конечно же может его использовать, но к чему тогда весь разговор, ему ничто не мешает на ассемблере писать). Это хороший способ разделения ответственности, главное что простой, всего одно правило.
Внешне выглядит очень даже симпатично. Поскольку на этапе компиляции постулированные функции не редуцируют (нету определения), то для выведения свойств нужно использовать дополнительные вещи. Для случая указателя на ячейку памяти в которой хранится сериализированное натуральное число, тип можно параметризировать натуральным числом "a" и дополнить доказательством, что если мы десериализируем бинарное значение в тип , то мы получим "a". Таким образом можно делать конкретные выводы о внешне императивной программе. Поскольку разыменование тоже низкоуровневое, то результат можно сохранять в типе Exact, и дальше в чистом мире снова перейти к значениям.
В первый оператор tr является преобразователем, не нуждающемся в аргументах, он вносит в контекст значение с именем "r" и типом Unique (Ref-ℕ i). Следующий оператор принимает и создает значение с именем "r", но изменяет тип на Unique (Ref-ℕ (suc i)). Третий создает значение "j" с типом Pure (Exact (suc i)). Ну и четвертый удаляет с контекста имя "r". Unique и Pure используются (пока?) просто как метки. Соединив все преобразователи в один получаем преобразователь, не принимающий ничего и возвращающий единственное значение типа Pure (Exact (suc i)). Функция extract принимает преобразователь именно такого вида, также аргумент должен быть завернут в тип Pure. Таким образом extract является чем-то вроде unsafePerformIO, но его можно сделать максимально safe с помощью типов преобразователей, ограничив способы их использования. Ведь всегда используя всякие unsafe штуки программист "знает", что он делает, а тут можно свои знания "закодировать" и проверить компилятором.
Ref-ℕ : ℕ → Set
Ref-ℕ a = Σ[ native ∶ nativeRef ℕ ] nativeGet-ℕ native ≡ a

data Exact {ℓ} {A : Set ℓ} : A → Set ℓ where
  exact : ∀ a → Exact a

tr : (n : ℕ) → Transformer! [] [(_ , Pure (Exact $ suc n))]
tr i = "r" := new i ⇒⟦ refl ⟧⇒
       "r" ++       ⇒⟦ refl ⟧⇒
       "j" := * "r" ⇒⟦ refl ⟧⇒
       free "r"

r : ∀ n → Exact (suc n)
r = extract ∘ tr

-- доказательство что "tr" действительно инкрементирует аргумент
getExact : ∀ {ℓ} {A : Set ℓ} {a : A} → Exact a → A
getExact (exact a) = a

≡-exact : ∀ {ℓ} {A : Set ℓ} {a : A} (e : Exact a) → getExact e ≡ a
≡-exact (exact a) = refl

p : ∀ n → getExact (extract $ tr n) ≡ suc n
p = ≡-exact ∘ extract ∘ tr
По ссылке можно посмотреть примеры (файлы *Test.agda). Использовались Agda 2.3.2 - 2.3.3 (на обоих должно работать) и stdlib-0.6 (НЕ dev версия, там кое-что изменилось).
Пока что дальнейший вектор развития не определен, есть еще много вопросов и замечаний, в том числе, удобность использования, безопасность и, самое главное, непротиворечивость.

2 коментарі:

  1. Интересно, конечно. По моим поверхностным впечатлениям, тут для счастья не хватает щепотки синтаксического метапрограммирования :) Ну, чтобы биндинги не строками, а идентификаторами хост-языка. Хотя с этим всё чуточку усложнилось бы: ведь пришлось бы ещё при аппликации функций к uniqueness-типизированным аргументам переименовывать соответствующий биндинг текущего контекста в имя аргумента функции, чтобы он правильно заиспользовался в её теле и т.д.

    ВідповістиВидалити
    Відповіді
    1. Агда еще развивается, и я думаю если моя идея окажется достаточно удачной, можно будет предложить некоторые изменения в сам язык (я думаю можно обойтись очень минимальными с использованием quote и quoteTerm).
      Если честно меня больше беспокоит необходимость вставлять доказательство равенства типов (там в примерах refl), тогда как типы хоть и undecidable но все же известны и с использованием рефлексии можно было бы это доказательство вывести автоматически.

      Видалити