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

А все что динамическое, это не типы в принципе

Советую прочитать секцию 1.1 в "Types and Programming Languages" Пирса

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

тут и так накидали уже, на двух языках

Эти хаскеллисты такие снобы. Не дают другим причаститься к лагерю ФПшников, динамические ЯП не считают за ЯП, и говорят, что там типов нет...

есть там типы

точнее тип

😜

поскольку сейчас ФП-фичи той или иной степени костыльности во всех языках - определять принадлежность как ФЯ по минимуму - это значит все языки как ФЯ определить

поскольку сейчас ФП-фичи той или иной степени костыльности во всех языках - определять принадлежность как ФЯ по минимуму - это значит все языки как ФЯ определить

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

Или со скалистами, которые пишут на Скале как на Джаве, но из-за самого факта использования Скалы считают себя функциональщиками?

эрлангистов скоро не будет - не будет и проблемы

В то же время, когда JS-разработчики, композируя функции, даже не догадываются, что делают ФП?

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

а зачем с ними что-то делать?

а зачем с ними что-то делать?

Чтобы мифы не распространяли.

В то же время, когда JS-разработчики, композируя функции, даже не догадываются, что делают ФП?

мне нормально писать на жеесе помогла схема

😀

ты начал делать call/cc в js?

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

и стараюсь писать функции без стейта через мапы и функторы

Эти хаскеллисты такие снобы. Не дают другим причаститься к лагерю ФПшников, динамические ЯП не считают за ЯП, и говорят, что там типов нет...

Да и Haskell не ФП чо уж там. Та логическая система которую задаёт Haskell своей системой типов очевидно противоречива, поэтому о каких гарантиях и типах может идти речь, если язык разрешает писать лапшу.

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

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

не пруфассистант. все эти потуги в сторону "тотальности" в хаскеле - это как ФП на C++

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

да, но это не важно

да, но это не важно

Ну, вообще есть Прокопов, который отказался от Эрланга в пользу Кложи, хотя и неизвестно, это разовый случай или тенденция.

Да и Haskell не ФП чо уж там. Та логическая система которую задаёт Haskell своей системой типов очевидно противоречива, поэтому о каких гарантиях и типах может идти речь, если язык разрешает писать лапшу.

Но ФП не про гарантии...

кложа на графике падает быстрее эрланга

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

И приводил пример Erlang'а в котором у вас типов нет, но гарантии они какие-то да дают.

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

И приводил пример Erlang'а в котором у вас типов нет, но гарантии они какие-то да дают.

Разве гарантия == гарантия в рантайме? Такая гарантия не очень полезна. Гарантии от тестов даже поболе будут

т.е. типы и "гарантии" совсем не одно и то же. типы в статике для генерации кода, а гарантии - это как повезет (чаще всего никак не повезет)

Разве гарантия == гарантия в рантайме? Такая гарантия не очень полезна. Гарантии от тестов даже поболе будут

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

Только она не про типы

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

Проверки в рантайме это assertions

И их можно писать в тридцать раз более интересные, чем Int /= Bool

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

Если падает в рантайме, то полезности в этом чуть. Хотя, Эрланг с его шапкозакидательской философией "let it crash" подталкивает разработчиков к толерантному отношению к падениям

Проверки в рантайме это assertions

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

И вот мой взгляд на проблему "динамического ФП" ФП - это парадигма, где функции (в правильном, математическом определении функции) это first-class values. При должном желании, писать в ФП-стиле можно на любом языке с подпрограммами, потому что избегать сайд-эффектов никто не запрещает. Но называться ФП-языком может только язык, который активно способствует такому стилю, т.е. статически запрещает сайд-эффекты

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

Они проеверяют инварианты

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

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

Я не знаю как можно просто закрыть глаза на это колоссальное различие и свалить две фундаментально разные вещи в одну кучу из-за поверхностной схожести

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

они не предназначены для одного и того же, не основаны на одном и том же, ничего общего кроме слова "типы" в названии у них нет

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

А статические типы без полиморфизма это хуже, чем отсутствие типов

они не предназначены для одного и того же, не основаны на одном и том же, ничего общего кроме слова "типы" в названии у них нет

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

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

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

но пересечение по функциональности притянуть можно - только вот с ассертами у "динамических" "типов" пересечение получше

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

У нас есть соответствие Карри-Говарда, поэтому вполне себе эквивалентно.

У нас есть соответствие Карри-Говарда, поэтому вполне себе эквивалентно.

Ничего там не эквивалентно, сейчас скажу какой кусок HoTT book читать

понятия множества и типа разные

Секция 1.1, "Type theory versus set theory"

Если что, то это общие соображения и они не про HoTT, это по сути кусок предисловия скорее

типы классифицируют термы, а не значения, как процитировано выше из пирса - это синтаксическое явление, какие там значения-то?

Ничего там не эквивалентно, сейчас скажу какой кусок HoTT book читать

А можно для тех, кто не в теме, эквивалентность и идентичность - это эквивалентные или идентичные понятия?

я уж не говорю, что тайпчек различает вообще не населенные типы

А можно для тех, кто не в теме, эквивалентность и идентичность - это эквивалентные или идентичные понятия?

отличный троллинг

Спасибо, я стараюсь 😊

типы классифицируют термы, а не значения, как процитировано выше из пирса - это синтаксическое явление, какие там значения-то?

А т.е. типы это синтаксические теги, которые проверяются во время компиляции?

ну да, можно так сказать

Интересно. Получается в динамических языках проверяются теги, в статических тоже проверяются теги, но в другой момент времени и это СОВЕРШЕННО разные теги, а ещё одни можно называть типами, а другие нет.

да, именно так

проверяются разные вещи, в разное время - видите, все разное

В общем я всё понял: спасибо. Это абсолютно одинаковые понятия.

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

и думаю какое бы выбрать

вроде 1 лучше всего?

В общем я всё понял: спасибо. Это абсолютно одинаковые понятия.

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

более того синтаксис яп, и инструкции процессора и инструкции байткод процессора это одно и тоже

Господи, ну как с людьми разговаривать, попробую как с тупыми тогда Есть три буквы, Т И П. Мы какие-то явления называем этими тремя буквами, а какие-то не называем. Похожи они или нет. Вот приду я к биологу, он мне покажет, мол, вот это К О Ш К А, а вот это С О Б А К А. А я ему начну: посмотри, придурок, это же одно и то же. Четыре лапы, шершавый язык, ушки, и звуки издает. На меня посмотрят как на дебила, возможно, не поняв, какой deep connection я сделал.

Ну что вы такие нетолерантные к чужому мнению

И вот у слова Т И П в computer science тоже есть класс явлений, которые им называются, и те, которые им не называются. Даже если похожи. Если в рантайме — всё, не тип

потому что нас люди читают

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