Re[40]: [haskell] considered mainstream
От: thesz Россия http://thesz.livejournal.com
Дата: 10.03.09 15:50
Оценка: 4 (1)
T>>Так он и моложе. И ситуация другая.
FR>Так он и популярнее.

Так каких-то лет пять всего.

T>>И требования у тебя выше.

FR>Так к лучшему из функциональных языков же

Так к ещё не развернувшемуся в полную силу.

T>>То, что евангелист я, не означает, что ты не должен подтверждать свои соображения. "Вывод явно притянутый" нуждается в другом, непритянутом выводе.

FR>Притянутый потому что ты никак ни показал что именно из-за меньшей плотности ошибок переходят на Хаскель. Вот мне видится что из-за большей выразительности и большей гибкости языка по сравнению с ML.

Пример.

Внутреннее представление ghc типизировано. При желании можно включить проверку типов для него после каждого преобразования. Если преобразование неправильное, то проверка типов нам об этом сообщит. Эта фича позволила сэкономить разработчикам ghc много времени.

Итак, строго типизированные представления помогают.

Достаточно стандартным приёмом является и конструирование языка для своих внутренних нужд. Даже если это просто некое внутреннее представление.

Внутреннее представление есть у всех. Степень типизации, правда, разная.

Вот здесь показано, как пользоваться GADT, чтобы компилятор проверил правильность преобразований.

То есть, то, что ghc проверяет в рантайме, простому пользователю ghc доступно во время компиляции, хотя бы и для его нужд поменьше масштабом.

Это вынуждает этим пользоваться.

Это сокращает количество ошибок.

Всякого рода преобразования встречаются и в далёких от ЯП программах. В тех же оптимизаторах файловых систем, ведь файловая система и есть дерево с типами блоков, да ещё и хитро увязанных друг с другом.

Почему пишущие на C++ до сих пор не пользуются GADT, мне непонятно.

FR>>>http://elementy.ru/lib/430319

FR>>>

FR>>>Иными словами, при любом конечном наборе аксиом мы имеем бесконечное число истин, которые не могут быть доказаны с помощью этого набора.

T>>Что это означает?
FR>Это означает что универсальной покрывающей хотя бы большую часть решаемых задач системы типов не построить.

Поэтому нужна система типов, которую мы можем затачивать под наши конкретные цели. Система типов Хаскеля движется в этом направлении.

FR>Там же есть еще другой вывод, очень многие задачи вообще неприводимы и неупрощаемы


Essential complexity по Бруксу.

Такое встречается очень редко.
Yours truly, Serguey Zefirov (thesz NA mail TOCHKA ru)
 
Подождите ...
Wait...
Пока на собственное сообщение не было ответов, его можно удалить.