Алгебраические типы как логика

Мостик к главной идее курса: структуры данных оказываются логическими связками.

Соответствие типы — логика: каждой конструкции типов отвечает логическая связка, а «обитаемость типа» — доказуемости утверждения.

Словарь перевода

Мы уже видели намёки: пара — это «и», сумма — «или». Соберём полный словарь — он и есть скелет соответствия Карри — Говарда, которое раскроем в следующем разделе.

Главная мысль: тип обитаем (имеет значение) тогда и только тогда, когда соответствующее утверждение доказуемо. Значение типа — это доказательство утверждения. Void необитаем — «ложь» недоказуема. Unit всегда обитаем — «истина» тривиальна.

Логические законы как функции

Логические тавтологии превращаются в полиморфные функции, которые можно написать. Закон «из A и B следует A» — это проекция пары. «Каррирование» (A и B -> C) = (A -> B -> C) — обычная функция. Если вы можете написать тотальную функцию данного типа, вы доказали соответствующую теорему.

A и B -> A          ~  fst : (A, B) -> A
A -> A или B        ~  Left : A -> Either A B
(A или B) -> C      ~  нужно обработать оба случая (паттерн-матч)
(A и B -> C)        ~  (A -> B -> C)   -- каррирование = логическая эквивалентность

Демонстрация: пишем доказательства как функции

Закодируем несколько логических законов как тотальные функции и убедимся, что они строятся. Раз функция написана и тотальна — теорема доказана.

# A и B -> A   (проекция = правило исключения конъюнкции)
def proj_left(pair):
    return pair[0]

# A -> (A или B)   (введение дизъюнкции слева)
def inl(a):
    return ("left", a)

# (A или B) -> C    при наличии A->C и B->C  (исключение дизъюнкции)
def either(on_left, on_right, s):
    if s[0] == "left":
        return on_left(s[1])
    return on_right(s[1])

print("proj_left ('a','b') :", proj_left(("a", "b")))     # доказали A и B -> A
print("inl 'a'             :", inl("a"))                   # доказали A -> A или B
print("either на left      :", either(str.upper, str.lower, ("left", "x")))
print("either на right     :", either(str.upper, str.lower, ("right", "Y")))

Вывод:

proj_left ('a','b') : a
inl 'a'             : ('left', 'a')
either на left      : X
either на right     : y

Каждая функция — конструктивное доказательство своей теоремы. Это и есть Карри — Говард в действии: программирование и доказательство — одно занятие.

Как работает под капотом

Соответствие держится на конструктивной (интуиционистской) логике: доказать «A или B» значит указать, какое именно — поэтому сумме отвечает дизъюнкция с явным тегом. Здесь же кроется граница: закон исключённого третьего A или (не A) в этой логике не доказуем без дополнительных аксиом, потому что нельзя для произвольного A построить значение типа Either A (A -> Void). Об этом — в разделе про Карри — Говарда.

Частые ошибки

• Ждать классическую логику. Соответствие даёт интуиционистскую логику: исключённое третье и двойное отрицание «бесплатно» не доказываются.
• Считать частичную функцию доказательством. Доказывает только тотальная функция; падение или зацикливание «доказывает» что угодно (как ложь).
• Путать значение и тип. Утверждение — это тип; доказательство — значение этого типа. Их легко перепутать на старте.

Итоги

• Произведение — конъюнкция, сумма — дизъюнкция, функция — импликация, Unit — истина, Void — ложь.
• Тип обитаем тогда и только тогда, когда утверждение доказуемо; значение = доказательство.
• Логические законы пишутся как тотальные полиморфные функции.
• Получается интуиционистская логика: исключённое третье даром не доказуемо.