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

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

>> Algol 6[08], Pascal - родом из 60-х и статически типизированы.

Дык, тогда это не было стремление к оптимизации, просто по другому то вообще сделать не могли :)

Доо. Лисп, если что, в 1959 изобрели. Позже подтянулись всякие Icon, Smalltalk и прочие Prolog'и.

Ну и по сути, та проверка типов весьма существенно отличается от используемой в ML, Haskell и т.д.

facepalm.svgz

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

Раскажи это гуглу у которого только прототипы на Python а продакшн на C++, а также Oraclу, посоветуй переписать Oracle DB на Ruby

>Почему не 60-х?

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

Статическая типизация была придумана для получения более надежных программ.

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

>Значимость статической типизации сильно преувеличена. Особенно адептами ф.я.

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

Твоя упоротость меня вдохновляет даже =). Если в лисп нету фичи Х - фича Х - херня. Если в языке X нету фичи Y, но Y есть в лисп, то X - херня. Словом все, что не лисп - херня.

А между делом то статическая типизация ловит очень многое.

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

Тут надо понимать, что в С и С++ уж и так очень много возможностей выстрелть себе в ногу. Там все-таки не такая строгая типизация, как в ML или Haskell. Ну и главное. А представьте себе, что в Си не было бы проверки типов при компиляции? Это же был бы вообще мрак. По любому чиху сегфолт =)

>> Почему не 60-х?

потом появляется С

Си появляется именно «потом», в 1972. А статически типизированные языки - в 60-х (Алгол 60, к примеру).

Статическая типизация была придумана для получения более надежных программ.

почему, пруф есть?

Ну нифига себе. Тебе то, что 2*2 == 4, тоже надо доказывать? Ну а вообще - почитай требования к Аде. Или хоть в Вики загляни, там сказано, что «static typing is a limited form of program verification». Это всё имеет прямое отношение к надежности.

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

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

Пока ничто не подтверждает вашу версию.

Это не «версия», это факт :D

> А представьте себе, что в Си не было бы проверки типов при компиляции? Это же был бы вообще мрак. По любому чиху сегфолт =)

А между прочим, так и было :) Ранние диалекты Си почти ничего не проверяли. Потом появился lint, потом - ANSI C.

>Раскажи это гуглу у которого только прототипы на Python а продакшн на C++, а также Oraclу, посоветуй переписать Oracle DB на Ruby

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

> А представьте себе, что в Си не было бы проверки типов при компиляции? Это же был бы вообще мрак. По любому чиху сегфолт =)

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

>А статически типизированные языки - в 60-х (Алгол 60, к примеру).

И что это доказывает?

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

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

static typing is a limited form of program verification

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

>а также Oraclу, посоветуй переписать Oracle DB на Ruby

Интерфейс с RDBMS, кстати, обычно динамический - гоняются туда-сюда рекордсеты в виде массивов вариантов.

>> А статически типизированные языки - в 60-х (Алгол 60, к примеру).

И что это доказывает?

Это вообще-то был вопрос: «почему ты не упомянул о слабом железе 60-х». Вероятно, потому, что тогда твоя фраза о статической типизации выглядела бы еще более нелепо?

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

И эта наивная реализация дико тормозит

Ты говорил о простоте реализации компиляторовБ а не о тормозах. И, как мне объяснили в соседнем треде, компилятор Lisp 1.5 в машкод был уже в начале 60-х, так что простота реализации компилятора к делу не относится.

static typing is a limited form of program verification

да, верификация - это соответствие формальным критериям,

Бгг.

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

Как скажешь %)

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

вообще-то непосредственное

>Или хоть в Вики загляни, там сказано, что «static typing is a limited form of program verification». Это всё имеет прямое отношение к надежности.

Наверно надо разделять чего мы хотим достигнуть - исключить из скомпилированного кода проверки меток типов в run-time или проверить в compile-time использование инстансов типа на соответствие контрактам. Первое как раз ослабляет надежность из-за потенциального сокрытия ошибок.

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

vala тем более. А ещё более феерично отнесение её к «скриптоте»

> Наверно надо разделять чего мы хотим достигнуть - исключить из скомпилированного кода проверки меток типов в run-time или проверить в compile-time использование инстансов типа на соответствие контрактам.

Естественно, второе.

> Ну что я могу сказать? Значит ты нихрена ничего не писал.

Не, ну как оценивать, для кого-то - наверное. http://github.com/archimag - там есть три форка чужих проектов (gentoo-lisp-overlay, hunchentoot и colorize), а остальное - это мой open source код за последний год (чуть больше) (ранее open source не писал). Примерно 10 000 строк кода. Open Source я пишу в свободное от основной работы время (за небольшими исключениями, когда этот код критичен для основного).

Я активно пишу около 8 лет. Пару лет назад прикидывал, что получается около 30 000 строк в код. Это, конечно, не самая впечатляющая цифра (доводилось читать и про 100 000 строк в код). И да, в этом году будет пожалуй меньше...

А сколько написал ты? Хочу узнать, на что стоит ориентироваться.

>почему ты не упомянул о слабом железе 60-х

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

Ты говорил о простоте реализации компиляторовБ а не о тормозах. И, как мне объяснили в соседнем треде, компилятор Lisp 1.5 в машкод был уже в начале 60-х, так что простота реализации компилятора к делу не относится.

дело не в простоте, а в простоте и одновременно скорости.

Бгг.

всё ясно. хотя даже в вике такое же определение дано.

Как скажешь %)

Значит возражений на счёт несвязанности статической типизации и надёжности больше нет?

>> Наверно надо разделять чего мы хотим достигнуть - исключить из скомпилированного кода проверки меток типов в run-time или проверить в compile-time использование инстансов типа на соответствие контрактам.

Естественно, второе.

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

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

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

И что же это за принципы? Сommon Lisp намного лучше и, тем более, пригоднее для реальной разработки.

>>> static typing is a limited form of program verification

Бгг.

всё ясно. хотя даже в вике такое же определение дано.

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

почему ты не упомянул о слабом железе 60-х

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

Ага, IBM360 - исследовательское железо, да. Или IBM7090, на которой был компилятор Лиспа.

Как скажешь %)

Значит возражений на счёт несвязанности статической типизации и надёжности больше нет?

Значит, спорить с тобой смысла нет. Почитаешь про историю Ады - приходи снова.

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

И что же это за принципы? Сommon Lisp намного лучше и, тем более, пригоднее для реальной разработки.

> И что же это за принципы? Сommon Lisp намного лучше и,

тем более, пригоднее для реальной разработки.

Автор просил ФП, Scheme ещё как-то в эту категорию попадает, а CL уже никак...

>>> Наверно надо разделять чего мы хотим достигнуть - исключить из скомпилированного кода проверки меток типов в run-time или проверить в compile-time использование инстансов типа на соответствие контрактам.

Естественно, второе.

Второе во-первых не исключает динамической типизации

Не исключает, конечно. Делает почти ненужной, но не исключает.

не покрывает несколько значительных категорий ошибок.

«There is no silver bullet» (c)

>Автор просил ФП, Scheme ещё как-то в эту категорию попадает, а CL уже никак...

Почему? Тем более, CL часто и учат в составе курса ФП.

> Почему?
Ну, никому же не приходит в голову относить, например, Python к ФП. В Common Lisp больше «императивных» возможностей, чем во многих «традиционно-императивных» языках (типа Java, C#, C++ и т.п.). А поддержка ФП весьма ограниченна: декомпозиция на основе потоков данных может применяться только для небольших задач, ибо слишком много съест ресурсов.

Тем более, CL часто и учат в составе курса ФП.

Где? Наши «вузы» просьба не приводить, там вообще глупостей хватает.

>Да тебе вообще многие неочевидные вещи ясны... а «бгг» относилось к тому, что под «формальный критерий» можно подвести что угодно.

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

Ага, IBM360 - исследовательское железо, да. Или IBM7090, на которой был компилятор Лиспа.

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

Почитаешь про историю Ады - приходи снова.

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

>Естественно, второе.

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

> Кто тут подводит под формальный критерий надёжности статическую проверку типов?

Статическая проверка типов - один из _методов достижения_ надежности. А «формальный критерий надежности» - это какое-нибудь MTBF.

Почитаешь про историю Ады - приходи снова.

И что там нужно вычитать, своими словами никак это не сформулировать?

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

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

>А поддержка ФП весьма ограниченна: декомпозиция на основе потоков данных может применяться только для небольших задач, ибо слишком много съест ресурсов.

Как-то утверждение после двоеточия не раскрывает утверждения перед ним. И оба они спорные.

> простое условие: избежать деления на нуль путём только статической типизации. С нетерпением ждём решения задачи.

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

>Статическая проверка типов - один из _методов достижения_ надежности.

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

Я уже сказал, что статическая проверка типов гарантирует остуствие их на этапе выполнения.

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

В Common Lisp больше «императивных» возможностей, чем во многих «традиционно-императивных» языках

а Haskell вообще - лучший императивный ЯП в мире

> Я вот помню читал где-то, что ошибки типов - составляют очень небольшой процент от всех ошибок.

Если бы ты еще вспомнил, к какому языку это относилось.

Я уже сказал, что статическая проверка типов гарантирует остуствие их на этапе выполнения.

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

Чтобы это было аргументом _для тебя_. Но доказывать тебе я ничего не собираюсь - ты как быдто на другом языке говоришь.

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

Прекрасно, доказывай. А я лично считаю, что совпаденние типов параметров процедур с типами аргументов всегда корректно с точки зрения приложения. И доказывать столь очевидные вещи не стану.

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

Какие? Какой ценой? Что будет если эти условия будут противоречить другим частям по? А они будут в общем случае, обязательно будут без дополнительно анализа человеком. Это доказано, в отличии от повышения надёжности статической проверкой типов. Какие последствия для большого написанного кода будет иметь исправление этих ошибок?

Нет, мне действительно интересно послушать мнение эксперта.

>А я лично считаю, что совпаденние типов параметров процедур с типами аргументов всегда корректно с точки зрения приложения. И доказывать столь очевидные вещи не стану.

правильно, лучше не позориться.

int a = 0; int b = 1; int c = b/a;

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

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

> Нет, мне действительно интересно послушать мнение эксперта.

Было бы тебе интересно чужое мнение (тем более - мнение экспертов), ты бы прочитал хотя бы Ada Rationale.

А я лично считаю, что совпаденние типов параметров процедур с типами аргументов всегда корректно с точки зрения приложения. И доказывать столь очевидные вещи не стану.

правильно, лучше не позориться.

Перед тобой, что ли? Меня это так беспокоит, так беспокоит %)

int a = 0; int b = 1; int c = b/a;

Браво, ты нашел прореху в статической типизаци. Ну, и вывод-то какой?

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

То есть ловлю опечаток ты не отрицаешь? Ну хоть это. А дальше - читай литературу по системам типов. Впрочем, ты не станешь - ты уже знаешь все ответы :)

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

Есть ли какие данные о том, что программы на языках со статической проверкой типов являются более надёжными? И не надо отсылать к теории и каким-то там «научным работам». Это вопрос ведь сугубо практический: полмира уже пишет на языках с динамической проверкой типов, и популярность такого подхода продолжает расти.

Я, конечно, понимаю, что все идиоты, но всё же? Быдлокодинг хоронит светлую идею статической проверки типов?

фактически стоит выбирать между Haskell и Erlang.

А так как Erlang более объектный, чем функциональный, то, кроме Haskell, выбора считай нет.

>Ну, и вывод-то какой?

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

А дальше - читай литературу по системам типов.

не, я вот пересказываю как раз то, что написано в литературе.

Было бы тебе интересно чужое мнение

Ничем не подкреплённое мнение не интересно.

Я писал на разных языках, с разными подходами к проверке типов, и никакой особой разницы в количестве ошибок не заметил

Можно поинтересоваться списком «разных языков»?

Потому что именно в Хаскеле я начал понимать, что такое НАСТОЯЩАЯ статическая типизация.

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

То, что языки, специально предназначенные для массового программирования (Java, C#) и критических по надежности приложений (Ada), являются статически типизированными, ни на что не намекает?

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

Быдлокодинг хоронит светлую идею статической проверки типов?

Одно другого не исключает. Куча быдлокода пишется на статически типизированной Яве.

> tailgunner не прав. динамический язык может в рантайме ловить подобные ошибки при наличии декларации

Ыыыыы... ясное дело, он их ловит. Но в рантайме, мля. При том, что их можно ловить на этапе компиляции.

Было бы тебе интересно чужое мнение

Ничем не подкреплённое мнение не интересно.

Ты его не знаешь даже (для протокола - я не о своем мнении).

И что же это за принципы? Сommon Lisp намного лучше и, тем более, пригоднее для реальной разработки.

... а принципов нет ни там, ни там.

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

(шёпотом) зависимые типы.

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

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

>Потому что именно в Хаскеле я начал понимать, что такое НАСТОЯЩАЯ статическая типизация.

Давай угадаю, она делает все крутым и супер математичным?