> не очень понимаю, какое отношение он имеет к обсуждаемому вопросу Там соответствия более дерзкие, и менее очевидные: Тип <->Теорема Терм типа <-> Доказательство Функция <-> Импликация Аппликация функции <-> Модус поненс Логическое И <-> Тупл Логическое ИЛИ <-> Either > мы каждый раз будем доказывать, что ента единственная бессмысленная теорема верна. Мне это не кажется хоть сколько-нибудь интересным. Да, именно поэтому никто и не использует динамическую типизацию для этих вещей.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
(no subject)
Date: 2012-10-18 04:00 pm (UTC)Там соответствия более дерзкие, и менее очевидные:
Тип <->Теорема
Терм типа <-> Доказательство
Функция <-> Импликация
Аппликация функции <-> Модус поненс
Логическое И <-> Тупл
Логическое ИЛИ <-> Either
> мы каждый раз будем доказывать, что ента единственная бессмысленная теорема верна. Мне это не кажется хоть сколько-нибудь интересным.
Да, именно поэтому никто и не использует динамическую типизацию для этих вещей.