Функциональщина. Что выбрать?

>Сильно в профиль. Лямба-исчисление поддерживает декомпозицию от рождения, машина Тьюринга - нет.

Ты еще скажи, что лямбда абстракции на машине Тьюринга не эмулируются.

А вот не всякий applicative functor монада, например.

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

>По кой черт тебе сдался хаскель

мне? нет, прочитай ветку, как обычно пришел очередной фанатик хаскелла и начал проповедовать о новой sb.

Бестиповых языков не бывает.

Где реальная польза от статической типизации( даже с выводом и т.д.), кроме тривиальных и спец. случаев, если есть динамическая с объявлением типов? недостатки уже были приведены.

>нет, прочитай ветку, как обычно пришел очередной фанатик хаскелла и начал проповедовать о новой sb.

только в подтверждение своих слов представил что-то их сильно опровергающее.

>Где реальная польза от статической типизации

Это дисциплина Специальной Олимпиады.

недостатки уже были приведены.

Ткни носом, плииз.

>Это дисциплина Специальной Олимпиады.

Нет, не дисциплина в постановке «в данном случае лучше одно, а вот в данном случае лучше другое». Быдловские штампы из лукмоаров не нужны.

Ткни носом, плииз.

лень. где-то до прихода хаскелльной( это не хар-ка языка, а некоторых его проповедников) неадекватности в тред. умозрительно рассматривались боле-менее «большие» проекты, упоминались небольшие с необходимостью верификации.

Охотно просвещу, вот знания, по моему мнению которыми должен обладать средний программист (включая, но не ограничиваясь):

Математика:Дискретная математика, анализ, алгебра, теория чисел, теория вероятностей, основы лямбда исчисления, и его связь с языками программирования, логика первого порядка, теория автоматов.

Алгоримы:Элементарные структуры данных, иметь представление и о нетривиальных структурах данных, сортировка и поиск, динамическое программирование, алгоритмы работы с графами, теоретико-числовые, вероятностные, получисленные.

[Следующие два раздела включил как очень важные, но все же не обязательные. Однако могут потребоваться некоторые знания из них ,и иногда в совершенно неожиданных случаях.]

Разделы ИИ: поиск в пространствах состояний, удовлетворение ограничений, логический вывод, планирование-эти разделы очень важны, и обязательно пригодятся.

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

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

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

Что вспомнил, то и написал. Быть может чего-то забыл. С наступающим всех :)

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

Полиморфизм есть в любом +нормальном_ статически типизированном языке. (дисклейме: ни жаба. ни це/це++ нормлаьными языками не являются).

Где реальная польза от статической типизации( даже с выводом и т.д.),

автоотлов определённых классов ошибок. Автоподстановка нужной реализации интерфейса в зависимости от переданных данных. Проверка реализаций функции на соответствие спецификации, выраженной в типе функции, причём тем более полное, чем мощнее система типов (вплоть до строгого доказательства корректности). Спецификация интерфейса модуля.

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

>Полиморфизм есть в любом +нормальном_ статически типизированном языке. (дисклейме: ни жаба. ни це/це++ нормлаьными языками не являются).

там он тоже есть.

+нормальном_ статически типизированном языке

то есть только в хаскелле и ко?

автоотлов определённых классов ошибок.

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

причём тем более полное, чем мощнее система типов (вплоть до строгого доказательства корректности).

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

Теперь скажи мне, какая в принципе есть польза от динамики

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

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

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

P.S. все это уже было озвучено в ходе треда и является почти общеизвестными сведениями. но почему-то никто толком это оспорить не может.

> > А про троллинг почему молчишь?

А что должен сказать? В чём суть претензий?

Т.е. тебе не стыдно за свой троллинг здесь?

откуда взялся этот класс ошибок?

Всегда был.

почему прохождение компиляции принимается за отлов ошибки, а не ошибку в спецификации и наоборот?

Потому что одновременная синхронная ошибка и в спецификации и в реализации практически невероятна. Потому что спецификация должна быть ещё и внутренне согласована - если для какого-то выражения указан не тот тип и написана не та реализация, то практически наверняка вылезет ошибка типизации там, где это выражение используется.

и тем меньшая выразительность и возможность переработки.

Неверно.

отлови в статике деление на нуль. динамическая система может такое отловить

При компиляции - не может; только в некоторых очень простых случаях статический анализ подобное отлавливает (что не имеет отношения к системе типов).

В рантайме деление на нуль отловят все.

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

Интересно, что ты подразумеваешь под «динамическими возможностями»? Паттерн-матчинг не имеет отношения к «динамичности» системы типов.

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

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

> Охотно просвещу, вот знания, по моему мнению которыми

должен обладать средний программист

Поскольку, вероятно, вы у нас авторитет, то отвечу ссылкой на другого авторитета: http://www.williamspublishing.com/21-days.html. Питер Норвиг почему-то излагает совершенно другую точку зрения. Почему?

В большей части согласен с этой статьей-но вы видимо не допоняли- меня, если вам показалось, что мои слова ей противоречат. Я вовсе не призываю получать чисто академические знания. Но вот к чему я призываю,так это к тому, чтоб у всех действий, у каждой строчки кода были веские основания в виде знаний в вашей голове. Пишите, много и регулярно, но с полным осознанием что происходит, почему, как это на самом деле должно происходить, и почему вы отдаете предпочтение одному решению, а другое-отвергаете. Без фундаментальных знаний это невозможно. А если действительно, все так и происходит, то, чтож, отлично! (Видимо сам я вас тоже не понял, извините)

Цитата:

максимальный уровень производительности труда в определенной области не достигается автоматически как результат приобретения опыта

Видишь, даже твой «авторитет» считает, что одного опыта не хватает.

> Типичная история успеха Лиспа - эффектная и не особо относящаяся к обычной жизни :)

неприменимая в жизни простых рабов на галере? :)

> Видишь, даже твой «авторитет»

Судя по скобочкам вы подвергаете сомнению авторитет Питера? И после это ещё и обвиняете меня в тролинге?

что одного опыта не хватает.

Конечно, речь идёт об обучении (!) на основе собственного опыта, но это не имеет никакого отношению к получению теортетических знаний.

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

Это тролль, хватит его кормить

> Судя по скобочкам вы подвергаете сомнению авторитет Питера? И после это ещё и обвиняете меня в тролинге?

Какие скобочки? И не столько после, сколько до этого поста.

> Разве оно автоматическое? Автоматика заключается в том, что язык (или рантайм) должен сам определять, когда можно форкануть и сделать параллельно (при этом поиметь соответствующие накладные расходы), а когда этого делать не стоит.

«заденьги» вот:

http://www.revolution-computing.com/

Свободная реализация для того же pnum0.

> > Судя по скобочкам вы подвергаете сомнению авторитет Питера? И после это ещё и обвиняете меня в тролинге?

Какие скобочки? И не столько после, сколько до этого поста.

Буду конкретнее:

Вот твои слова:

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

Ссылка на пост: http://www.linux.org.ru/view-message.jsp?msgid=4377380&page=9#comment-4384117

Это очень толстый троллинг.

> Это очень толстый троллинг.

В чём заключается тролинг? Эта мысль является для вас новой? Что если вы не пишите что-то очень специфичное, то математика не нужна?

Какие скобочки?

Кавычки, вокруг слова авторитет относительно Питера. Вы таки отказываетесь признать в нём авторитета?

> Пишите, много и регулярно, но с полным осознанием что происходит,

почему, как это на самом деле должно происходить, и почему вы отдаете

предпочтение одному решению, а другое-отвергаете.

Думаю, что на самом деле происходит не так. Приведу пример из шахмат, не совсем то, но всё же тоже интеллектуальная деятельность. Так вот, ссылаясь на авторитет Ботвинника, в шахматах известно такое явление как «Врожденное позиционное понимание», например оно было ярко выраженно у Капабланки и Карпова, но его не было у Каспаров (и он много работал над устранение этого дефекта). Суть в том, что человеку, обладающему таким пониманием не нужно знать теорию (которая в шахматах есть), он смотрит на позицию и «видит» её: просто на интуитивном уровне даёт оценку позицию, понимает перспективы её развития и как нужно действовать, и всё это без каких-либо логических заключений. Тоже самое и в программировании, важна способность «видеть» код, которая позволяет принимать правильные решения без знания теоретических основ. Эту способность «видеть» можно развить путём критического анализа и рефакторинга собственного кода, сочетая это с изучение кода других людей. Теория это хорошо, но на её изучение требуется время, и не мало, и в большинстве случае лучше потратить это время на непосредственную работу с кодом, отдача будет значительно больше.

>>>Теперь скажи мне, какая в принципе есть польза от динамики

отлови в статике деление на нуль.

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

можно выносить работу с типами, как работу с тем, что под ними подразумевается, вплоть до изменения и обработку рантаймовых ошибок по типу( матрицы и вектора, как ещё один пример)

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

более гибкую систему восстановления после реальных ошибок.

Не даёт. Система обработки ошибок ортогональна типизации. При этом у тебя в любой момент может вывалиться ошибка, на которую ты не написал обработки. В правильной системе типов за привешиванием обработки ошибок проследят, в динамике - нет.

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

Паттерн-матчинг как раз к динамике/статике никакого отношения не имеет. Это не более чем своеобразный switch по применённому конструктору типа с биндингом переменных, он может быть и в статической типизации (и тогда он ограничен диспатчем по конструкторам одного типа) и в динамической (и тогда можно пользоваться им как удобным средством работы с RTTI ). В цацкеле реализован первый вариант. Динамические средства там есть (Data.Dynamic), но ими никто не пользуется.

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

Я одно время смотрел на баги в багзиле генты. Меня особенно убил баг, который лечился добавкой слова volatile. Так что с этих пор я убеждённый сторонник FP/Static Typing

P.S. все это уже было озвучено в ходе треда и является почти общеизвестными сведениями. но почему-то никто толком это оспорить не может

Эм, это всё были ошибочный заключения. Зачем оспаривать ошибочные заключения? Это имеет смысл, если есть надежда на вменяемость собеседника и какой-то профит от процесса. Ну а троллям как раз интересно довести человека до состояния бешеной болонки, благо это зачастую довольно просто.

>>Полиморфизм есть в любом +нормальном_ статически типизированном языке. (дисклейме: ни жаба. ни це/це++ нормлаьными языками не являются).

там он тоже есть.

Если ты про полиморфизм через виртуальные функции, то он немного неполноценен . Множественная диспетчеризация и всё такое. Если про плюсовые шаблоны - то таки да, там оно более - менее полноценно, но изрядно криво.

+нормальном_ статически типизированном языке

то есть только в хаскелле и ко?

Я знаю про два: цацкель и SML/OCaml . F# не смотрел, но по слухам он слизан с ML-образных, так что там тоже может быть. Про остальные просто не в курсе. Очень может быть, что есть более мейнстримные, но никакой уверенности не имею.

автоотлов определённых классов ошибок.

откуда взялся этот класс ошибок?

Описки и недосып были всегда, это неизбежно. Если они ловятся тайпчекером, то с чего бы от этого отказываться?

почему прохождение компиляции принимается за отлов ошибки, а не ошибку в спецификации и наоборот? ведь часть по может быть написана неправильно, а правильность неизвестна до получения результата, и даже может меняться в ходе эксплуатации. мне решительно неясно почему должно быть сразу правильно и навечно.

Корректность спецификации - совершенно отдельный разговор. Замечу, однако, что типизация вынуждает думать о типах, поэтому наблюдается некоторое принуждение к продумыванию спецификаций. И чем более выразительна система типов, тем больше принуждение.

Прохождение компиляции в статике гарантирует совместимость контрактов скомбинированных в выражении термов. Человек в состоянии удержать в голове до 7-9 объектов, если же включать в выражение больше элементов, то уследить за конрактами становится сложновато.

причём тем более полное, чем мощнее система типов (вплоть до строгого доказательства корректности).

и тем меньшая выразительность

Нет. См выше про полиморфизм, который без статики убог.

и возможность переработки.

Система типов позволяет эффективно следить за соблюдение конктрактов. При необходимости её можно заткнуть каким-нить undefined.

это уже не система типов, а больше система доказательств.

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

почему такое нужно в сразу в языке, а не в виде отдельного верификатора( например чтобы для риалтайма доказать время)?

Чтобы писать всё один раз, а не два. Потому что рассуждение идёт о типах термов.

то что доказываем не зависит от системы типов,

Основа доказательства как раз в правильном typing и доказательстве совместимости типа терма с нужным типом. Есть альтернативы, но они сложнее, а тут есть достаточно развитый инструментарий. Не сказать чтоб широко распространённый, но он есть. В отличии от.

>> Типичная история успеха Лиспа - эффектная и не особо относящаяся к обычной жизни :)

неприменимая в жизни простых рабов на галере? :)

Наверное, к ней тоже неприменимая.

> Замечу, однако, что типизация вынуждает думать о типах, поэтому

наблюдается некоторое принуждение к продумыванию спецификаций.

И чем более выразительна система типов, тем больше принуждение.

Во-во, одна из ключевых проблем. На ранних этапах разработки, когда ещё не ясно что на самом деле пишется (как это обычно бывает), необходимо заниматься продумыванием спецификаций. Потом их переделывать, что выливается в постоянную борьбу с системой типов. Если бы мы имели в начале хорошо описанные и чёткие задачи, то возможно это и имело бы смысл (хотя то же под сомнение, учитывая наши собственные дефекты). Но в мире, когда х.з. что на самом деле пишется, нужна прежде всего гибкость и способность к коренной перестройки программы, способность легко варьировать свои идеи, а это плохо сочетается с «могучей» системой типов.

Т.е. получается, что ситема типов пытается сгладить наши дефекты, приводящие к ошибкам (разного рода опечаткам), за счёт требований, совершенно не учитывающий дефекты реального мира.

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

Это способ понять задачу.

Спасибо за разъяснение. Конечно я слышал об этом, но являюсь противником такой теории по большей части потому, что даже при выполнении всех нешобходимых условий развитие такой способности не гарантированно, и не известны условия, при которых она гарантированно достигается. В то же время мой подход более систематичен, и позволяет при правильном применении достигать стабильных результатов. Это две различных позиции, и вряд ли возможно суметь доказать превосходство одной из них в сиюминутном споре. На самом деле, мне не известно ни одной работы, в которой бы подобное сравнение проводилось, но в то же время видимо можно провести аналогию с двумя видами обучения интеллектуальных агентов-обучение с подкрепленим и обучение на основе знаний.

Насчет шахмат-тут спорить не стану. И метод «видения» позиции намного эффективнее рассуждений о каждой из них. Возможно это связано с особенностями обработки информации мозгом. Поэтому думаю у шахматах так важно развить эту способность.

Вообще было приятно побеседовать.

> Это способ понять задачу.

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

Ох... а вот я иногда начинаю решение таких задач(когда еще не совсем ясно, что получится в результате) как раз с описания типов. После чего большая часть кода как-бы сама логичным образом ложится.

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

Кстати, вот про полиморфизм тут почему-то не слышат. А зря.

> Но в мире, когда х.з. что на самом деле пишется, нужна прежде всего гибкость и способность к коренной перестройки программы, способность легко варьировать свои идеи, а это плохо сочетается с «могучей» системой типов.

Каким образом? Или по-твоему лучше маскировать ошибки/ловить их на этапе выполнения?

Попробуй детальнее продумывать то, что ты собираешься написать ;)

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

Это способ понять задачу.

наиболее разумный способ понять задачу это максимально быстро выпустить первую версию и дать пользователям

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

> Кстати, вот про полиморфизм тут почему-то не слышат. А зря.

Что с ним не так?

С ним всё так.

> Статическая типизация по крайней мере гарантирует, что у тебя _в программе_ понимание задачи однозначное, а не шизофреническое.

А вот это статическая типизация никак не может гарантировать, только в каких-то конкретных случаях.

>> Статическая типизация по крайней мере гарантирует, что у тебя _в программе_ понимание задачи однозначное, а не шизофреническое.

А вот это статическая типизация никак не может гарантировать, только в каких-то конкретных случаях.

На уровне ЯП? Может. А вообще, серебряной пули не существует.

Судя по скобочкам вы подвергаете сомнению авторитет Питера? И после это ещё и обвиняете меня в тролинге?

Вот для этого, в частности, хорошо фундаментальное образование. Приучает критически относиться к любым «авторитетам».

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

Иногда можно, я как-то демонстрировал. Даже на жабе можно (на плюсах нельзя).

Не, ну если индуктивно матрицы/векторы определять, то наверно можно. Только это неинтересно - оно в основном нужно в численных приложениях, а там такой подход чересчур неэффективен.

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

Когда спецификация меняется за пару секунд - это, конечно, очень тяжело.

гибкость и способность к коренной перестройки программы, способность легко варьировать свои идеи, а это плохо сочетается с «могучей» системой типов.

Очень хорошо сочетается, если система типов действительно могучая.

Ты же не видел ни одной могучей системы типов, убогая типизация C++ - всё, что ты знаешь.

Не холивара окаянного ради...:)

Не, ну если индуктивно матрицы/векторы определять, то наверно можно. Только это неинтересно - оно в основном нужно в численных приложениях, а там такой подход чересчур неэффективен.

Эффективность можно повысить.

Скажем, простейшие индуктивные вектора с длиной в типе:

data Nil a = Nil
data Cons lst a = Cons a (lst a)
test :: Cons (Cons (Cons (Cons (Cons Nil)))) Integer
test = Cons 1 $ Cons 2 $ Cons 3 $ Cons 4 $ Cons 5 Nil

newtype S a = S a
data E lst a = E (lst a) (lst a)
data O lst a = O a (lst a) (lst a)
test :: O (E S) Integer
test = O 1 (E (S 2) (S 3)) (E (S 4) (S 5))

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

Чтобы не раздувать холивор, то кратко, ответы известными фактами.

Этот класс ошибок в динамике ортогонален типизации, это ошибка логики и ловится системой арифметики, а позднее отрабатывается в системе обработки ошибок.

Код должен отражать концепцию задачи, а не языка. Боттом ап( различные фреймоврки и т.д.) + dsl практически повсеместно. Тип в концепции задачи: ненулевое целое.

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

Делает код монолитом, изменения слишком дороги, если нам понадобилось особое представление, например, разряженных матриц.

Не даёт. Система обработки ошибок ортогональна типизации.

Практически тоже, что и в первом случае. Если легче ошибку связать с типом, то почему бы и нет?

Боттом ап( различные фреймоврки и т.д.) + dsl практически повсеместно.

DSL и DSEL - традиционно одна из очень сильных сторон Хаскеля.

Тип в концепции задачи: ненулевое целое.

Увы, системы типов, позволяющие отследить подобное (а они таки существуют) не слишком удобны на практике, в первую очередь, за счёт отсутствующего вывода типов. Возможно, Coq-овские тактики или что-то в этом роде сумеют его заменить. Со временем. А пока остаётся что в статически типизированных языках, что в динамически типизированных, отслеживать подобное в рантайме.

Делает код монолитом, изменения слишком дороги, если нам понадобилось особое представление, например, разряженных матриц.

Классическое Хаскельное решение - классы типов. В класс выносится интерфейс, который требуется от матриц, для различных представлений делаются свои реализации. То, что от представления не зависит (выражается через функции интерфейса) работает полиморфно.

Если легче ошибку связать с типом, то почему бы и нет?

Если легче - то конечно да.

>есть вполне себе конкретная теорема, устанавливающая изоморфизм между доказательством и программами.

с другой стороны на практике безошибочных программ нет(ну пусть будет почти).

Система типов позволяет эффективно следить за соблюдение конктрактов.

как уже было сказано, то гарантий нужности и корректности контрактов нет.

При необходимости её можно заткнуть каким-нить undefined.

Это даст надёжную динамич. типизацию? И какова будет её поддержка со стороны стат. языка?

Корректность спецификации - совершенно отдельный разговор. Замечу, однако, что типизация вынуждает думать о типах, поэтому наблюдается некоторое принуждение к продумыванию спецификаций. И чем более выразительна система типов, тем больше принуждение.

В теории это даст хорошую программу, но это не учитывает время и изменения программы. Что ставит под сомнение увлечение типами, вместо получения быстрого результата( про это есть статьи с историями успеха крупных продуктов, про хаскелль и ко - в основном применение в узких нишах, и как доп. инструменты, причём всё это небольших размеров).

> Когда спецификация меняется за пару секунд

Скажем так, спецификаций просто нет.

Ты же не видел ни одной могучей системы типов

Я потратил на Haskell около двух месяцев, после чего переключился на Common Lisp. Так что имею определённое представление. Но я не обнаружил там возможностей для «утиной типизации», что просто ужасно... Плохо смотрел?

>Я потратил на Haskell около двух месяцев, после чего переключился на Common Lisp. Так что имею определённое представление. Но я не обнаружил там возможностей для «утиной типизации», что просто ужасно... Плохо смотрел?

Ыыыыы... =)

Скажем так, спецификаций просто нет.

Система типов Хаскеля и есть такая спецификация.

Так что с утиной типизацией? Я вот вспомнил, что застрял именно на этом. Возможно или нет?

Система типов Хаскеля и есть такая спецификация.

Насколько я понимаю, столь «могучая» типизация, как и ленивые вычисления, по крайней мере у меня создалось такое впечатление после прочтения SICP, была придумана для того, что бы обеспечить применимость функционального подхода с точки зрения производительности. Это возможно из-за ФП, но сами по себе имеют ценность только для ФП. Т.е. первичным является всё таки функциональный подход. Тут же после прочтения топика может создатся впечатление, что главное достоинство Haskell в системе типов... Меня это как бы смущает. Зачем тогда говорить о ФП? а не о языках с «мощной системой статической типизации»?