Аргумент кардинальности на самом деле не работает с полиморфными c типами (см. Ответ @ chi).
Но сам изоморфизм можно интуитивно объяснить следующим образом:
Тип forall r. (a -> r) -> r
означает ", если вы дадите мне функцию, которая преобразует a
в r
, я могу вернуть вам r
. О, и я могу сделать это для любого возможного r
"
Единственный способ выполнить такое обещание - тайно иметь a
в моей руке ,
Поскольку я обещаю сделать это для любого возможного r
, это означает, что я ничего не могу знать о самом r
, в том числе о том, как построить его значение. И единственное, что у меня есть, это функция a -> r
, которую вы мне даете. И единственный способ вызвать такую функцию - дать ей a
.
Это означает, что если я даю такое обещание, у меня уже в тайне должно быть a
за моей спиной.
Для более формального объяснения напомним, что «isomorphi c» в простых терминах означает «может быть однозначно преобразован туда и обратно без потерь». Вот к чему приводит аргумент кардинальности: если у вас одинаковое количество вещей, вы всегда можете организовать пару между ними.
И в своем вопросе вы уже показываете две конверсии: cont
конвертирует одну Кстати, unCont
преобразует другой. И вы можете тривиально показать, что cont . unCont = unCont . cont = id
. Следовательно, типы изоморфны c.
Хотя показание существования двух преобразований является более формальным, я считаю, что не всегда достаточно получить интуицию о том, что два типа действительно "своего рода одно и то же" отсюда и интуитивное объяснение, которое я дал выше.