Изоморфизм Карри-Ховарда

Я поискал в Интернете, и я не могу найти никаких объяснений ЧИ, которые не вырождались бы быстро в лекцию по теории логики, которая резко выше моего понимания. (Эти люди говорят так, как будто «интуиционистское исчисление высказываний» — это фраза, которая на самом деле что-то значитдля нормальных людей!)

Грубо говоря, CHI утверждает, что типы — это теоремы, а программы — доказательства этих теорем. Но что, черт возьми, означает даже ??

Пока что я понял следующее:

• Рассмотрим id :: x -> x. "учитывая, что X истинно, мы можем заключить, что X истинно". Мне кажется разумной теоремой.

• Теперь рассмотрим foo :: x -> y. Как скажет вам любой программист на Haskell , это невозможно. Вы не можете написать эту функцию. (Ну, во всяком случае, без обмана.) Читать как теорему, она гласит: «Учитывая, что любое X истинно, мы можем заключить, что любое Y истинно». Это, очевидно, ерунда. , точно, ты не могу написать эту функцию.

• В более общем смысле аргументы функции можно рассматривать как «то, что считается истинным», а тип результата можно рассматривать как «то, что истинно, если предположить, что все остальные вещи верны». Если есть аргумент функции, скажем, x -> y, мы можем принять это как предположение, что истинность X подразумевает, что Y должно быть истинным.

• Например, (.) :: (y -> z) -> (x -> y) -> x -> zможно понимать как «предполагая, что Y подразумевает Z, что X подразумевает Y, и что X истинно, мы можем сделать вывод, что Z истинно». Что кажется мне логически разумным.

Теперь, что, черт возьми, означает Int -> Int?? o_O

Единственный разумный ответ, который я могу дать, таков: если у вас есть функция X -> Y -> Z, то сигнатура типа говорит: «Предположим, что возможно создать значение типа X, а другое — типа Y, то можно построить значение типа Z". И тело функции точно описывает, как вы это сделаете.

Это кажется логичным, но не очень интересным. Так что очевидно, что это должно быть что-то большее, чем это...