Соответствие Карри — Ховарда

Вот мы и добрались до самого важного. Программа на языке, взявшем за основу λ-исчисление и решившем проблему зацикливания, — это теорема: её формулировка — тип, компиляция — проверка доказательства, а исполнение гарантированно возвращает результат обещанного типа. С императивными языками такое тоже возможно — корректность программ доказывают со времён логики Хоара, — но куда сложнее: там доказательство не сама программа, а отдельная надстройка из предусловий, постусловий и инвариантов.

Итак, программы, написанные на языках, базирующихся на λ-исчислении, проще доказывать, чем программы на других языках — не обязательно императивных, скажем, на Python. В этой главе мы рассмотрим соответствие Карри — Ховарда, мост между логикой и программированием: написать программу типа $\tau$ — то же самое, что доказать высказывание $\tau$. Заметил его Карри ещё в 1930-х — по типам комбинаторов, — а точную форму оно получило в рукописи Ховарда 1969 года.

Присмотримся к типам знакомых термов, читая стрелку как импликацию «из $A$ следует $B$». Тождественная функция оказывается доказательством тавтологии «из $A$ следует $A$»:

Комбинатор $\mathrm{K}$, отбрасывающий второй аргумент, — доказательство высказывания «если верно $A$, то $A$ следует из чего угодно»:

Комбинатор $\mathrm{S}$ тоже доказывает теорему — про раздачу посылки двум следствиям:

Приведём, пожалуй, таблицу соответствия:

Немного пояснений. Единичный тип $()$ — тип ровно с одним значением. Построить его значение можно всегда и тривиально, поэтому $\top \;$​${} \leftrightarrow\; ()$. А вот пустой тип $\mathtt{Void}$ — тип без единого значения: программу такого типа написать невозможно. Это и есть ложь: у $\bot$ нет доказательств.

«$\forall$ второго порядка → полиморфизм System F» (мы это ещё обсудим дальше). Квантор второго порядка пробегает по самим высказываниям (в мире типов — по типам): «для любого высказывания $A$ верно …». В программах это в точности параметрический полиморфизм: тип тождественной функции $\forall a.\; a$​${} \to a$ читается как теорема «для любого $A$: из $A$ следует $A$». System F — это λ-исчисление, где такая квантификация по типам встроена в язык; на нём основан полиморфизм Haskell.

«$\forall,\;\exists$ над объектами → зависимые типы». Кванторы первого порядка пробегают уже не по высказываниям, а по объектам — конкретным значениям: «для любого числа $n$ …», «существует список $x$, такой что …». Чтобы записать такое типом, тип должен зависеть от значения — это и есть зависимые типы. В самом Haskell $\forall$ есть только по типам, зато LiquidHaskell навешивает на типы логические предикаты — уточняющие типы: сигнатура $\mathtt{head'} : \{\,v : [a] \mid \mathtt{len}\;v$​${} > 0\,\}$​${} \to a$ читается как «для любого списка $v$, длина которого больше нуля …», а импликации между предикатами проверяет SMT-решатель. Квантор $\exists$ выражается уточнением результата: $\{\,v : \mathtt{Int} \mid \mathtt{even}\;v\,\}$ — предъявленное чётное число вместе с гарантией чётности. Подробнее — в главе «LiquidHaskell».

Мы возвращаемся к проблеме полноты по Тьюрингу. Неограниченная рекурсия $\mathtt{fix} : (A \to A)$​${} \to A$ в логическом прочтении — «если из $A$ следует $A$, то $A$ верно»: порочный круг, доказывающий что угодно. Поэтому языки-доказатели обязаны быть тотальными: проверка тотальности из прошлой главы — не перестраховка, а условие честности логики. На этом соответствии стоит пруф-ассистент Agda: спецификация записывается типом, программа этого типа и есть доказательство, а проверка доказательства — обычная проверка типов.