stdray: (Default)
stdray ([personal profile] stdray) wrote2012-10-08 04:23 am

очень плохая ссылка

про мифический хаскель (линк).

Блин, аж до тошноты. Атд есть динамическая типизация. Типы нужны, чтобы узнать какое количество памяти надо выделить. Метки типов. Типов пустых туплов. Классы типов — это АлгТД. Классы типов - недокостыль. Система типов — это лишь инструмент для разметки памяти под данные и связи кода с данными. Статическая типизация: это когда в исходнике if есть (в том или ином виде: ПМ, overloading и т.д.), а в генеренном коде if-а нет? Боксирование...

Как всякие морготные фильмы ужасов. Когда кровь, кишки, слизь какая-то, глаз выпал, и кто-то постоянно нападает из-за угла. Смотреть противно, но все равно смотришь. Даже не уверен, что мне интересен конец истории. Смотришь и плющит. Эмоции как-никак, хоть и негативные.

[identity profile] isorecursive.livejournal.com 2012-10-18 04:00 pm (UTC)(link)
> не очень понимаю, какое отношение он имеет к обсуждаемому вопросу
Там соответствия более дерзкие, и менее очевидные:
Тип <->Теорема
Терм типа <-> Доказательство
Функция <-> Импликация
Аппликация функции <-> Модус поненс
Логическое И <-> Тупл
Логическое ИЛИ <-> Either
> мы каждый раз будем доказывать, что ента единственная бессмысленная теорема верна. Мне это не кажется хоть сколько-нибудь интересным.
Да, именно поэтому никто и не использует динамическую типизацию для этих вещей.
Edited 2012-10-18 16:05 (UTC)