Почему в алгебраических типах данных, если я могу определить специальные функции «от» и «до» для двух типов, эти два типа можно считать равными?

Термин, который автор использует, чтобы не «упоминать теорию категорий или продвинутую математику», — это количество элементов. Он определяет два типа как ===-равные друг другу, если они имеют одинаковую мощность, то есть, если существует столько же возможных значений одного, сколько и другого.

Потому что, если два типа имеют одинаковую мощность, между ними существует изоморфизм. Mul () Bool может быть другого типа, чем Bool, но членов одного типа ровно столько же, сколько и другого, и можно тривиально определить функцию, которая будет переходить от одного к другому или от другого к одному. (Не то, чтобы был только один такой изоморфизм — дело в том, что вы могли бы выбрать любой.)

Это не лучший подход. В принципе, он отлично работает для конечных множеств, но вводит неприятные побочные эффекты для бесконечных множеств, таких как Add Int Int === Int. Тем не менее, для базового описания сложения и умножения типов он, кажется, годится.

Неформально говоря, когда две математические структуры A,B имеют две "хорошие" функции from,to, удовлетворяющие from . to == id и to . from == id, структуры A,B называются изоморфными.

Фактическое определение «хорошей» функции зависит от типа имеющейся структуры (и иногда разные определения «хорошей» приводят к различным понятиям изоморфизма).

Идея изоморфных структур заключается в том, что они «работают» примерно одинаково. Например, рассмотрим структуру A, созданную логическими значениями True,False с &&,|| в качестве операций. Пусть тогда структура B состоит из двух натуральных1,0 с min,max в качестве операций. Это разные структуры, но они имеют одни и те же правила. Например, True && x == x и 1 `min` x == x для всех x. A и B изоморфны: функция to будет отображать True в 1 и False в 0, а from будет выполнять противоположное отображение.

(Обратите внимание, что хотя мы могли бы сопоставить True с 0 и False с 1, и мы все равно получили бы from . to == id и его двойник, это сопоставление не будет считаться «хорошим», поскольку оно не сохранит структуру: например, to (True && x) == to x еще to (True && x) == to True `min` to x == 0 `min` to x == 0 .)

Другой пример в другой постановке: пусть A — это круг на плоскости, а B — это квадрат на этой плоскости. Затем можно определить непрерывные сопоставления to,from между ними. Это можно сделать с любыми двумя «замкнутыми петлями», грубо говоря, которые можно назвать изоморфными. Вместо этого окружность и фигура «восьмерка» не допускают таких непрерывных отображений: самопересекающаяся точка в «восьмерке» не может быть отображена в любую точку окружности непрерывным образом (грубо говоря, от нее отходят четыре «пути»). , а точки в окружности имеют только два таких «пути»).

Аналогичным образом в Haskell типы называются изоморфными, когда между ними существуют две определяемые в Haskell функции from,to, удовлетворяющие приведенным выше правилам. Здесь «хорошая» функция просто означает, что ее можно определить в Haskell. Связанный веб-блог показывает несколько таких изоморфных типов. Вот еще один пример с использованием рекурсивных типов:

List1 a = Add Unit (Mul a (List1 a))
List2 a = Add Unit (Add a (Mul a (Mul a (List2 a))))

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

Другой пример:

Tree a = Add Unit (Mul a (Mul (Tree a) (Tree a)))

Вы можете доказать, что тип Tree Unit изоморфен List1 (Tree Unit), используя алгебраические законы, найденные в блоге. Ниже = обозначает изоморфизм.

List1 (Tree Unit)
-- definition of List1 a
= Add Unit (Mul (Tree Unit) (List1 (Tree Unit))) 
-- by inductive hypothesis, the inner `List1 (Tree Unit)` is isomorphic to `Tree Unit`
= Add Unit (Mul (Tree Unit) (Tree Unit))
-- definition of Tree a
= Tree Unit

Приведенный выше набросок доказательства индуцирует функцию to следующим образом.

data Add a b = InL a | InR b
data Mul a b = P a b
type Unit = ()
newtype List1 a = List1 (Add Unit (Mul a (List1 a)))
newtype Tree a  = Tree  (Add Unit (Mul a (Mul (Tree a) (Tree a))))

to :: List1 (Tree Unit) -> Tree Unit
to (List1 (InL ())) = Tree (InL ())
to (List1 (InR (P t ts))) = Tree (InR (P () (P t (to ts))))

Обратите внимание, как рекурсивный вызов играет роль индуктивной гипотезы в доказательстве.

Написание from оставлено в качестве упражнения :-P

Почему в алгебраических типах данных, если я могу определить специальные функции from и to для двух типов, эти два типа можно считать равными?

Что ж, здесь лучше использовать термин не "равный", а скорее изоморфный. Дело в том, что когда два типа изоморфны, они в принципе взаимозаменяемы друг с другом; любая программа, написанная в терминах A, в принципе может быть написана в терминах B, без изменения смысла программы. Предположим, у вас есть:

from :: A -> B
to   :: B -> A

и эти две функции составляют изоморфизм, то есть:

to (from a) == a
from (to b) == b

Теперь, если у вас есть функция, которая принимает A в качестве аргумента, вы можете, например, написать аналог, который вместо этого принимает B в качестве аргумента:

foo :: B -> Something
foo = originalFoo . from
    where originalFoo :: A -> Something
          originalFoo a = ...

И для любой функции, которая производит A, вы можете сделать это аналогичным образом:

bar :: Something -> B
bar = to . originalBar
    where originalBar :: Something -> A
          originalBar something = ...

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