В этой статье я попробую показать соотвествие между между математическими доказательствами и программами, а так же попытаюсь ненавязчиво ввести читателя в синтаксис Agda.

#agda

И да, эта статья тоже будет типо DRAFT и я ее буду дополнять.

Соответствие Карри-Ховарда устанавливает соответствие между типизированным лямбда исчислением и интуиционистской логикой. Типы соответствуют высказываниям. Если мы построим значение определённого типа, то мы так же докажем высказываение соответствующее этому типу. Поскольку типы являются высказываниями, а значения являются доказательствами, конструкторы для типа соответствуют правилам вывода для соответствующего предположения.

В таблице ниже соответствие представлено более наглядно:

Логические системы	Языки программирования
Высказывание	Тип
Доказательство высказывания P	Терм(выражение) типа P
Утверждение P доказуемо	Тип P обитаем(∃ p ∈ P)
Импликация P ⇒ Q	Функциональный тип P → Q
Конъюнкция P ∧ Q	Тип произведения(пары) P × Q
Дизъюнкция P ∨ Q	Тип суммы (размеченного объединения) P + Q
Истинная формула	Единичный тип (⊤)
Ложная формула	Пустой тип (⊥)
Квантор всеобщности ∀	Тип зависимого произведения (Π-тип)
Квантор существования ∃	Тип зависимой суммы (Σ-тип)

Модули

Определим модуль:

{-# OPTIONS --safe #-}
module CurryHoward where

Имя модуля на верхнем уровне должно соответствовать названию файла, а вложенные модули могут называться как угодно или даже не иметь названия. Тут так же могут быть указаны опции компилятора, например, очень частая опция —safe заставляет компилятор убедиться, что выключены другие опции, которые могут вызывать противоречия и отключает возможность делать постулаты, а так же проверяет, что все импорты тоже “безопасны”.

Единичный тип

Определим единичный тип как тип с одним конструктом:

data ⊤ : Set where 
    tt : ⊤ 

(подробнее про объявление типов)

Пустой тип

Определим пустой тип как тип без конструкторов:

data ⊥ : Set where 

Здесь же определим элиминатор пустоты

⊥-elim : ∀ {A : Set}  → ⊥ → A  
⊥-elim () -- это так называемый absurd pattern, который можно использовать когда нет ни одного значения которое можно было бы передать в эту функцию

(подробнее про Absurd Pattern)

Определим отрицание, отрицание для типа A будет означать функцию которая A в пустой тип ⊥

¬_ : Set → Set 
¬ A = ⊥

Функциональный тип как импликация

Определим функциональный тип и покажем, что он соотвествует импликации:

-- true ⇒ true 
f₁ : ⊤ → ⊤ 
f₁ tt = tt 

-- false ⇒ true 
f₂ : ⊥ → ⊤ 
f₂ _ = tt 

-- false ⇒ true можно так же доказать через элиминатор пустоты
f₂' : ⊥ → ⊤ 
f₂' x = ⊥-elim x 

-- false ⇒ false 
f₃ : ⊥ → ⊥ 
f₃ x = x 

-- true ⇒ false невозможно определить т.к. нет способа сконструировать пустой тип
-- f₄ : ⊤ → ⊥ 
-- f₄ = ？ 

-- ¬ true тоже невозможно определить т.к. нет способа сконструировать пустой тип
-- f₄' : ¬ ⊤ 
-- f₄' = ？ 

Ну и давайте на пример тавтологии A ⇒ (B ⇒ A) покажем как можно использовать явный и не явный полиморфизм

-- Явным образом
taut : (A B : Set) → A → (B → A) 
taut T₁ T₂ t₁ t₂ = t₁ 

-- Вызывать придется с явным указанием типов 
taut-ex : ⊥ → (⊥ → ⊥)
taut-ex = taut ⊥ ⊥ 

-- Эквивалентная запись 
taut₂ : (A : Set)(B : Set) → A → (B → A) 
taut₂ T₁ T₂ t₁ t₂ = t₁ 

-- Эквивалентная запись 
taut₃ : (A : Set) → (B : Set) → A → (B → A) 
taut₃ T₁ T₂ t₁ t₂ = t₁ 

-- Так же можно добавлять квантор всеобщности 
taut₄ : ∀ (A : Set) → (B : Set) → A → (B → A) 
taut₄ T₁ T₂ t₁ t₂ = t₁ 

-- Эквивалентная запись 
taut₅ : ∀ (A B : Set) → A → (B → A) 
taut₅ T₁ T₂ t₁ t₂ = t₁ 

-- Неявный образом
taut' : {A B : Set} → A → (B → A) 
taut' t₁ t₂ = t₁ 

-- Тогда типы можно передать или не передавать
taut'-ex₁ : ⊥ → (⊥ → ⊥)
taut'-ex₁ = taut' {⊥} {⊥} -- передаются неявные параметры в фигурных скобках, если нужно

-- Или передать один, причем можно указать какой
taut'-ex₂ : {A : Set} → A → (⊥ → A)
taut'-ex₂ = taut' {B = ⊥}

-- В целом можно делать все тоже самое, что и с круглыми скобками -- добавлять стрелочки и квантор всеобщности, и даже получать неявные параметры и использовать их в функции
taut'₂ : {A : Set} → ∀ {B : Set} → A → (B → A) 
taut'₂ {B = T₂} t₁ t₂ = t₁ --тут можно использовать T₂

-- Если совсем безумствовать, то с ума можно сходить очень по разному
taut'₃ : ∀ (A : Set) → {B : Set} → A → (B → A) 
taut'₃ T₁ t₁ t₂ = t₁ 

-- Вообще-то даже Set можно не писать, если писать ∀, но в таком общем коде лучше писать(можно смело писать, где из контекста понятен конкретный тип) 
-- т.к. там есть нюансы с вложенностью типов в типы
taut'₄ : ∀ A → ∀ {B} → A → (B → A) 
taut'₄ T₁ = λ t₁ t₂ → t₁ --а еще лямбды можно писать

(еще подробнее про объвление функций)

Тип произведения (пары)

Определим тип пары, который соотвествует коньюнкции

data _×_ (P : Set) (Q : Set) : Set where
    pair : P → Q → (P × Q)

И тогда можно показать, что

-- P ∧ Q ⇒ P
×-elim₁ : {P Q : Set} → (P × Q) → P
×-elim₁  (pair p _) = p

-- P ∧ Q ⇒ Q
×-elim₂ : {P Q : Set} → (P × Q) → Q
×-elim₂  (pair _ q) = q

Тип суммы

Определим тип суммы, который соотвествует дизъюнкции

data _+_ (P Q : Set) : Set where
   Left : P → P + Q
   Right : Q → P + Q

И тогда можно показать, что

+-elim : {A B C : Set} → (A → C) → (B → C) → (A + B) → C
+-elim ac bc (Left a) = ac a
+-elim ac bc (Right b) = bc b

Сигма тип(зависимая сумма)

А вот сейчас будет сложно. Во первых, потому что зависимые типы, во вторых, мы незаметно введем уровни для типов Set(в целом все что нужно знать это Set i имеет тип Set (i + 1), сделано так, чтобы обойти парадокс Рассела), а в третьих, сумма это теперь пара, т.е. фактически зависимая сумма это обобщение произведения, и понимайте это как хотите(если я сам это когда-нибудь осознаю обязательно расскажу).

open import Agda.Primitive

record Σ {i j} (A : Set i) (P : A → Set j) : Set (i ⊔ j) where 
  constructor _,_
  field
    fst : A    
    snd : P fst 

(подробнее про record'ы и про уровни)

В стандартной билиотеке есть еще несколько удобных синтаксисов для Σ-типа

Σ-syntax : ∀ {a}{b} (A : Set a) → (A → Set b) → Set (a ⊔ b)
Σ-syntax = Σ

syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B

∃ : ∀ {a}{b}{A : Set a} → (A → Set b) → Set (a ⊔ b)
∃ = Σ _

∃-syntax : ∀{a}{b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
∃-syntax = ∃

syntax ∃-syntax (λ x → B) = ∃[ x ] B

Фактически Σ-тип можно воспринимать как значение типа A и зависящий от этого значения предикат P. Например

-- Для любого типа B существует тип A такой, что существует функция B → A
Σ-ex : ∀ {B} → Σ Set (λ A → B → A)
Σ-ex = ⊤ , λ _ → tt

-- Или тоже самое используя синтаксис Σ
Σ-ex' : ∀ {B} → Σ[ A ∈ Set ] (B → A)
Σ-ex' = ⊤ , λ _ → tt

-- Или тоже самое используя синтаксис ∃
Σ-ex'' : ∀ {B} → ∃[ A ] (B → A)
Σ-ex'' = ⊤ , λ _ → tt

Пи тип(зависимое произведение)

Пи-тип, он же тип зависимой функции, он же тип зависимого произведения, можно использовать и без дополнительных определений т.к. фактически он зашит в Agda, но чисто формально его можно представить так:

Π : ∀ { n m }(A : Set n)(P : A → Set m) → Set(m ⊔ n)
Π A P = (x : A) → P x

Тип Π можно воспринимать как квантор всеобщности где для любого элемента типа A истинен предикат P. Например:

--Для любого типа существует функция из него в непустое множество
Π-ex : Π Set (λ A → A → ⊤)
Π-ex = λ _ _ → tt

Зависимые типы

Зависимые типы это одна из ключевых фишек Agda позволяющая конструировать функции в которых типы зависят от термов или даже типы от типов, данные типы можно воспринимать в том числе как предикаты или отношения, а их обитаемость как доказательства свойств термов.

Например, можно определить равенство Лейбница, когда x = y, если для любого предиката P: P x = P y.

_==_ : ∀ {A : Set} (x y : A) → Set₁
_==_ {A} x y = Π (A → Set) (λ p → (p x → p y))
-- определение эквивалентно ∀ (P : A → Set) → P x → P y

и тогда можно показать рефлексивность ==

refl-== : ∀ {A : Set}{x : A} → x == x
refl-== P Px = Px

На самом деле в Agda равенство термов и типов обычно определяется иначе, но кажется это хороший пример, чтобы показать как работают зависимые типы.

Вместо послесловия

Надеюсь было не слишком абстрактно, специально не хотелось вводить дополнительные типы, чтобы сконцентрироваться именно на соответствии логических операций и типов. Далее, возможно, хотелось бы разобрать такую штуку как Decidability т.к. иногда нужно с уровня типов опуститься на уровень термов, чтобы, например, факт обитаемости того или иного типа сопоставить с true и false, как это было в статье про лямбда исчисление в if_then_else

Используемые символы и их коды:

Символ	Код
→	\to
∧	\and
∨	\or
λ	\lambda
∣ ∈	\in
∃	\exists
×	\x
∣ ⊤	\top
⊥	\bot
∀	\forall
Π	\Pi
Σ	\Sigma
⇒	\=>
ₙ	\_n