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

[stdray]

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

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

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

Comments

[isorecursive.livejournal.com]

> Вопрос, что мы знаем в compile time. В случае с атд знаем про сам тип, а так же тип функций-конструкторов. В случае с динамикой, такой информации нет.
Почему же нет? Можно представить, что в динамике у нас в компайл-тайме достоверно известно: все термы одного и того же типа - одного из таких вот Т, которые мы можем объявлять в хаскеле показанным выше образом. А типы конструкторов можно вывести из стандарта данного динамического языка (они там будут называться "элементарные типы" и "определённые пользователем типы" и прочее в таком духе).

> какая там ветка сопоставится, имхо, такого же уровня вопрос, как в случае с сопоставление элементарных типов (интов каких или булов), но для них почему-то никакой речи о динамической типизации не идет.
Не понял, о чём речь.

> это принципиально разные вещи, на мой взгляд
Наверное, соответствия Карри-Говарда тебе тоже не понравятся.

[stdray.livejournal.com]

>Можно представить, что в динамике у нас в компайл-тайме достоверно известно: все термы одного и того же типа
Согласен. (1)

>А типы конструкторов можно вывести из стандарта данного динамического языка
Можно. Статический анализ никто не отменял. Но по факту, динамика на то и динамика, что в компайл-тайм ничего подобного не известно.

>Не понял, о чём речь.
Я просто провел аналогию, что есть тип и его значения мы можем как-то различать. В одном случае (атд) говорят о динамической типизации, в другом (инт, бул) - просто про условный оператор.

>Наверное, соответствия Карри-Говарда тебе тоже не понравятся.
Я его не до конца понимаю, потому не могу говорить, нравится мне или нет, как не очень понимаю, какое отношение он имеет к обсуждаемому вопросу. Там что-то про типы и доказательство их существования. Если трактовать динамику описанным выше образом (см. 1), мы каждый раз будем доказывать (или не доказывать, что являет собой какие-то взаимоисключающие параграфы), что ентот единственный тип не пуст. Мне это не кажется хоть сколько-нибудь интересным. Хотя, опять же, у меня нет пониманию, потому, может, я бред несу.

[isorecursive.livejournal.com]

> не очень понимаю, какое отношение он имеет к обсуждаемому вопросу
Там соответствия более дерзкие, и менее очевидные:
Тип <->Теорема
Терм типа <-> Доказательство
Функция <-> Импликация
Аппликация функции <-> Модус поненс
Логическое И <-> Тупл
Логическое ИЛИ <-> Either
> мы каждый раз будем доказывать, что ента единственная бессмысленная теорема верна. Мне это не кажется хоть сколько-нибудь интересным.
Да, именно поэтому никто и не использует динамическую типизацию для этих вещей.