да, почему forall A. A | -A не годится, мне как раз понятно, но это же просто мотивация, от неё нужен ещё огромный шаг :)
Тут нужно сообразить, как теория типов изгоняет дух Де Моргана.
И что умного именно в том, что (Either A (A → ⊥)) → ⊥. Ок, A → ⊥ означает, что мы для любого типа можем построить функцию, которая виснет.
Отсюда получается, что (A → ⊥) → ⊥ было бы доказательством населённости типа A (A неопровержимо истинно), но это только если мы строим функцию, пользуясь только переданной A → ⊥, т.е. можем построить одно значение A, которое вбросим в функцию, а не строим новую виснущую функцию для этого типа (мы же можем построить такую функцию для любого типа). Вот тут вот одна заковыка - почему мы обязаны пользоваться переданной функцией.
Хм, или откуда получается, что мы не можем построить виснущую функцию для ненаселённого типа: ⊥ → ⊥
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2013-04-22 07:00 am (UTC)Тут нужно сообразить, как теория типов изгоняет дух Де Моргана.
И что умного именно в том, что (Either A (A → ⊥)) → ⊥. Ок, A → ⊥ означает, что мы для любого типа можем построить функцию, которая виснет.
Отсюда получается, что (A → ⊥) → ⊥ было бы доказательством населённости типа A (A неопровержимо истинно), но это только если мы строим функцию, пользуясь только переданной A → ⊥, т.е. можем построить одно значение A, которое вбросим в функцию, а не строим новую виснущую функцию для этого типа (мы же можем построить такую функцию для любого типа). Вот тут вот одна заковыка - почему мы обязаны пользоваться переданной функцией.
Хм, или откуда получается, что мы не можем построить виснущую функцию для ненаселённого типа: ⊥ → ⊥