Программирование с зависимыми типами

Кто-нибудь занимается описанием криптографических протоколов с помощью зависимых типов? Это было бы полезно, например, для верификации смартконтарктов.
Там возникают сложности, как описать знание/незнание ключа. Похоже, полноценного описания требуется использовать модальную логику - такие логики могут отображаться в системы типов?
Пока получается что-то вроде:

Хеш-функция

hash: Data -> CheckSum
hashProp1: (x:Data) -> (y:Data) -> (hash x = hash y) -> (x = y)
hashProp2: (rev: CheckSum -> Data) -> (p: (d: Data -> rev (hash d) = d)) -> Void

То есть значение хеш-функции однозначно идентифицирует аргемент, но обратной к ней не существует.

Симметричное шифрование

encode: Key -> Data -> Encrypted
decode: Key -> Encrypted -> Data
cryptProp1: (k: Key) -> (d: Encrypted) -> (encode k (decode k d)) = d
cryptProp2: (k: Key) -> (d: Data) -> (decode k (encode k d)) = d
cryptProt3: ((d:Data, e:Encrypt) -> (k: Key ** (encode k d = e))) -> Void
cryptProp4: (((d1:Data, e1:Encrypt) -> (d2:Data, e2:Encrypt) -> Either (k: Key -> encode k d1 = e1 -> encode k d2 = e2) (k: Key -> encode k d1 = e1 -> encode k d2 = e2 -> Void)

С электронной подписью пока не разобрался.

Есть вполне полезные языки, не поддерживаюшие HKT - Rust, Elm. Возможно ли (и осмысленно) в подобных языках делать поддержку зависимых типов? Например, Elm справедливо требует тотальности кода, но из-за этого приходится описывать и обрабатывать невозможные ситуации, например когда пользователь еще не залогинился, а уже разлогинивается. Зависимые типы позволяют описать невозможность такого события.

В брутальном [мета-]введении в Агду попался пример

data _≤_ : ℕ → ℕ → Set where
z≤n : ∀ {n} → zero ≤ n
s≤s : ∀ {n m} → n ≤ m → succ n ≤ succ m

sub₀ : (n m : ℕ) → m ≤ n → ℕ
sub₀ n zero (z≤n .{n}) = n
sub₀ .(succ n) .(succ m) (s≤s {m} {n} y) = sub₀ n m y

Не могу понять, как определение sub₀ раскрывается в case, а главное, почему так.

Тайна раскрыта
Агда матчит в том порядке, в котором написано в программе: по первой строчке выбирается паттерн с конструктором, соответствующая переменная раскрывается в case, и так далее.
Ошибка oxij в том, что по аргументам с точкой паттерн-матчить вообще нельзя

Приз "за лучшую подсказку" уходит к nivanych

https://www.youtube.com/channel/UCqm9psjm_czCS0EXCjr3A4w

http://homotopytypetheory.org/book/
http://homotopytypetheory.org/2013/06/20/the-hott-book/
http://golem.ph.utexas.edu/category/2013/06/the_hott_book.html

Теперь можно доказывать корректность императивных программ с помощью зависимых типов.

Пара хороших введений в Агду. Оставлю здесь, чтобы было куда ссылаться.

Peter Divianszky (Eötvös Loránd University, Department of General Computer Science)
https://people.inf.elte.hu/divip/AgdaTutorial/Index.html

Thorsten Altenkirch (School of Computer Science, the University of Nottingham)
http://www.cs.nott.ac.uk/~txa/g53cfr/

Подскажите, пожалуйста.
Вот у меня есть индуктивный предикат:

  Inductive last (a: A): list A -> Prop :=
  | last_one: last a (a :: nil)
  | last_many: forall (l: list A) (x: A), last a l -> last a (x :: l).

Очевидно^?, что last a nil быть не может. Как тогда доказать что-нибудь типа такого?

  Lemma last_nil: forall (a: A), last a nil -> False.

Спасибо.

Рассмотрим типизированные кортежи с именованными компонентами. Множество имён компонентов KS одно для всех кортежей, но кортеж может иметь не все компоненты. Есть функция typeof, которая отображает имя компонента на тип компонента. Множество функций с зависимым типом, у которых зависимость типа результата от значения аргумента задаётся typeof, и есть множество кортежей с компонентами из KS.

KS0 ⊆ KS ∧ KS1 ⊆ KS. Если истинно KS0 ⊆ KS1, то существует проекция, которая берёт кортеж с именами KS1 и возвращает кортеж с именами KS0. Проекция всего лишь выбрасывает те компоненты кортежа, имена которых ∈ KS1 и ∉ KS0, потому я назвал её проекцией. KS0 ⊆ KS1 можно превратить как каноническую инъекцию inj : KS0 → KS1. Тогда интуитивно это описывается как «инъекция превращается в проекцию». Если построить категорию (обозначим её (P KS)) из ЧУМ подмножеств KS, имею контравариантный функтор D : P KS → Set (и пучок).

Как доказать свойства D из свойств dependent product? typeof использовать не получится, вместо typeof имеем bundle для каждого KS0, KS0 ⊆ KS. pullback functor inj* должен отображать bundle для KS1 в bundle для KS0, bundle-ы разумеется связаны. Морфизм KS0→1 (назову его (final KS0)) (1 — это singleton, я работаю в Set) задаёт функтор Π (final KS0), который берёт bundle для KS0 и возвращает собственно множество кортежей с именами KS0.

Дальше затык. Информация по dependent product у меня очень скудная.

то бишь computer science. Здесь собирают подписи.