Алгебраическая интерпретация полиморфизма

Так я понимаю основную алгебраическую интерпретацию типов:

Either a b ~ a + b
(a, b) ~ a * b
a -> b ~ b^a
()   ~ 1
Void ~ 0 -- from Data.Void

... и что эти соотношения верны для конкретных типов, таких как Bool, в отличие от полиморфных типов, таких как a. Я также знаю, как переводить подписи типов с полиморфными типами в их конкретные представления типов, просто переводя кодировку Черча в соответствии со следующим изоморфизмом:

(forall r. (a -> r) -> r) ~ a

Итак, если у меня есть :

id :: forall a. a -> a

, я знаю, что это не означает id ~ a^a, но это на самом деле означает:

id :: forall a. (() -> a) -> a
id ~ ()
   ~ 1

Аналогично:

pair :: forall r. (a -> b -> r) -> r
pair ~ ((a, b) -> r) - > r
     ~ (a, b)
     ~ a * b

Что подводит меня к моему вопросу. Какова «алгебраическая» интерпретация этого правила:

(forall r. (a -> r) -> r) ~ a

Для каждого изоморфизма конкретного типа я могу указать эквивалентное алгебраическое правило, такое как:

(a, (b, c)) ~ ((a, b), c)
a * (b * c) = (a * b) * c

a -> (b -> c) ~ (a, b) -> c
(c^b)^a = c^(b * a)

Но я не понимаю алгебраического равенства, аналогичного:

(forall r. (a -> r) -> r) ~ a