Curry-Howard: типы как высказывания, программы как доказательства

Тимофей Ильич · архивариус

Вот она, страница двести три. Слева подпись «вывод», справа «типизация», а дерево одно, и черты у них общие. Я сначала решил, что Арбенина сэкономила бумагу. Потом сравнил по буквам: где в выводе «допустим A», в типизации «x имеет тип A». Где «применим правило к посылке», там «применим функцию к аргументу». Это одно и то же дерево, или я на старости лет вижу то, чего нет?

Тимофей Ильич видит то, что есть. В прошлом уроке таблица BHK сказала, что доказательство $A\to B$ это способ превратить доказательство A в доказательство B. В блоке «Допуск» поручение с ярлыком $A\to B$ это функция, которая берёт улику вида A и возвращает улику вида B. Слово «способ» и слово «функция» описывают одну вещь.

Это наблюдение называют соответствием Карри-Говарда. Хаскелл Карри заметил его для простых случаев в 1930-х, Уильям Говард описал его целиком в 1969 году. В TAPL ему посвящён раздел 9.4. Сегодня ты прочтёшь страницу двести три целиком.