Вся статья наполнена логическими ошибками. Раздел про апорию "Стадий" особенно, поэтому разберу его:
Если две колесницы движутся навстречу друг другу со скоростью, равной минимальной единице пространства за минимальную единицу времени, мимо третьей, неподвижной колесницы, то они пройдут расстояние, равное минимальной единице пространства за минимальную единицу времени относительно неподвижной колесницы и за половину минимальной единицы времени относительно друг друга. Таким образом, получится, что минимальная, то есть неделимая, единица времени делима, что абсурдно (равным образом, делимой окажется и минимальная, то есть неделимая единица пространства)
Раз из предположени о двух колесницах мы приходим к абсурду, значит оно ложно. То есть в дискретном мире не может быть двух колесниц едущих навстречу друг другу с такой скоростью.
Далее идёт аналогия с поездами и там закралось следующее утверждение:
Вы скажете, что это нормально, ведь поезд В тоже двигался, причем как бы на встречу поезду Г. Это значит, что в какой-то момент времени Г1 и В2 должны были сравняться
Нет, не значит. Эта предпосылка основана лишь на интуитивном понимании движения поездов/колесниц. Её верность в дискретном мире остаётся необоснованной, а раз с ней мы опять приходим к противоречию, то всё что следует из рассуждения в статье это: утверждение "Г1 и В2 должны были сравняться" ложно. Предположение о дискретности так и осталось неопровергнутым
При ну очень большом желании и ресурсах -- смайнить альтернативную цепочку длиннее основной. Но мне думается, имелось ввиду, что майнеры не будут включать транзакцию в блок, а не что майнеры удалят уже попавшую в блокчейн транзакцию
Разные данные, от научных по корреляции систем вознаграждения в мозгу с полом до личных, показывают, что социальные вопросы и ситуации девушкам обсуждать интересно и приятно.
С моим опытом совпадает лишь отчасти. Можно ссылку на исследование? Плюс, пока неясно как из того, что девушкам приятно обсуждать социальные вопросы следует, что с ними нужно обсуждать социальные вопросы
Сколько среди них девушек?
25% (2/8)
Сколько среди них девушек, вызывающих заодно романтически-физиологический интерес?
Прочитал художественную книжку с красивой историей — опыт, и можно обсудить своё отношение к героям и их поступкам.
А что может рассказать ваш средний задрот? Впечатляющий опыт похода на собеседование и решения литкод-задач? Опыт организации кубернетес-кластера? Опыт чтения книжки Софтваре Енгенеринг ат Гугле, с обсуждением своего отношения к монорепе и CI? Кулстори о том, как вы насиживали геморрой до трёх ночи за починкой бага?
Про интересность художественной литературы это же больше стереотип, разве нет? Я за всю жизнь, наверное, человек двух встречал, которым реально было бы интересно обсуждать художку. В моём кругу общения большая часть бесед это человек А угорел по Х и увлечённо рассказывает человеку Б, где Х варьируется от полиморфных вирусов до алгебраической топологии. У среднего задрота, вероятно, есть множество интересных тем для обсуждения. Понятно, не каждому расскажешь их во всей сложности, но в целом, мне кажется, это не является помехой в общении.
И как были ваши успехи в то время при общении на эти темы? Какие у вас были бы успехи, если бы вы общались только на эти темы?
У меня нет интересов за исключением математики и проги (и физики, но это было давно и неправда). Возможно, есть какой-то предварительный фильтр из-за которого мой опыт не является показательным, но, кмк, общение только на эти темы не является проблемой. Мне думается, гораздо больше влияет то, что эти интересы не способствуют социализации, а с малым кругом общения вероятность начать какие-то отношения сильно меньше.
На фронте, например, функции для плавной анимации вполне из физики.
Только программисту для реализации плавной анимации это всё знать не нужно. Открывается первый попавшийся сайт с кривыми Безье, и подбираются на глаз параметры. И это если забыть, что можно просто animation-timing-function: ease сделать
Шрифты с закорючками всё равно нужны (а то как их редактор рисует-то?)
У меня была проблема не столько с самими закорючками, сколько с их размещением. У юникода множество сабскриптов очень ограниченно. Например в агде уже не написать, потому что в юникоде нет символа .
Можно добавлять нужные, но отсутствующие в ваш редактор! Агде ж всё равно, она любой уникод жрёт.
Можешь привести какой-то пример? Я, кажется, не совсем понимаю что имеется ввиду
Утверждение-то истинное (на ФПМИ в 2021-м нужно было набрать 302 балла за три предмета, линк), но в контексте обсуждения почти бессмысленное: дипломы олимпиад тоже выдаются относительно других участников
Агда очень костыльная в этом плане. Во-первых набор символов сильно ограничен по сравнению с техом, во-вторых нужно искать шрифты поддерживающие закорючки. У Isabelle/HOL, насколько я знаю, в тексте обычные символы, а в редакторе они отображаются как закорючки. Такой подход, кмк, сильно лучше агдовского
Причём это не первая такая статья закинутая в чулан. Сейчас топ чулана это статья@Nurked годовой давности, твоя статья, статья про ковид, и статьи из 2012-го
значительная часть людей, кто мог бы проголосовать, статью банально не увидели
У вас 17к просмотров, это в три раза больше чем у топовой статьи в лучшем за сутки, и 79 голосов, это где-то как внизу первой страницы лучшего за неделю.
и пока статья из сектантских минусов выбиралась
37 плюсов, 42 минуса. Возможно, дело в качестве статьи, а не в "функционально-типовом сектанстве"
О каком, в таком случае, утраивании, учетверении и до бесконечности идёт речь? Вот исходник map, прямо из ghc-internal:
map :: (a -> b) -> [a] -> [b]
{-# NOINLINE [0] map #-}
-- We want the RULEs "map" and "map/coerce" to fire first.
-- map is recursive, so won't inline anyway,
-- but saying so is more explicit, and silences warnings
map _ [] = []
map f (x:xs) = f x : map f xs
Три строчки, одна из них это аннотация, которую на самом деле, можно выкинуть, и работает с любыми типами. В обычных языках у вас просто цикл по пришедшему массиву больше строчек займёт
дженерики — второй инструмент после АДТ и третий после автоматического вывода типов и четвертый после interface{}, который пытается вытащить пользователя из той ж..., куда загнали его типами
Дженерики (aka параметрический полиморфизм) и АДТ это часть системы типов, а не отдельный инструмент. Интерфейсы (aka классы типов) в хаскеле выражаются через дженерики и АДТ. При большом желании вы можете руками передавать структуры со всеми нужными методами, и не использовать классы типов, но зачем, если компилятор умеет делать эту работу за вас? Возможость опускать типы в коде это вообще синтаксический сахар, поэтому в чём тут проблема мне неясно
если легче читать с аннотациями, то вывод типов - это усложнение чтения.
Вывод типов не мешает наличию аннотаций. Он делает их проставление опциональным, и злоупотребление выводом действительно усложняет чтение кода. Это непротиворечивый набор утверждений.
с аннотациями читать сложнее. ибо аннотации в общем случае удваивают количество кода
Открыл кусок кода со своего пет-проекта. Аннотаций типов на девять строчек целых две:
а поскольку запрещают писать обобщённые функции, то утраивают или учетверяют и до бесконечности.
Вы с дженериками, шаблонами или интерфейсами не сталкивались? Они в мейнстриме лет 30 уже, в 2025-м году нужно постараться найти типизированный язык без чего-то из вышеперечисленного. Но если и правда не сталкивались, вот вам пример обобщённой функции в хаскеле:
ghci> :type map
map :: (a -> b) -> [a] -> [b]
ghci> map (\x -> x + 10) [1..3]
[11,12,13]
ghci> map (\x -> show x) [1..3]
["1","2","3"]
ghci> map (\x -> Just x) [1..3]
[Just 1,Just 2,Just 3]
ещё мучиться с построением АДТ (что компилятор мог бы делать самостоятельно).
Каким боком тут АДТ?
перенести на компилятор какой-то класс ошибок. причём эти ошибки возникали крайне редко (по сравнению с прочими ошибками)
Даже по вашему опросу (репрезентативность которого я ставлю под сомнение), 25% людей чаще сталкиваются с ошибками типов чем с логическими. Это точно крайне редкий класс ошибок?
дело не в безграмотности, а в том, что вы уводите контекст в сторону.
Вам по существу уже ответили: аннотации типов и безопасность системы типов это вещи никак не связанные. Причём, что характерно, говорить про аннотации типов вы начали. Хинди-Милнер это мимоходом, просто упомянул, что они даже в мощных системах типов далеко не всегда нужны.
и, кстати, приводя в пример автоматический вывод типа, вы сами себе противоречите. где-то выше вы заявляли, что типы повышают читабельность, что дескать посмотрел на выражение, увидел типы и вуаля "лучше понял" что здесь происходит.
Откройте какой-нибудь учебник по теории типов и посмотрите хотя бы Simply Typed Lambda Calculus.
Ибо если описывать типы абсолютно всего подряд, то программу Вы никогда не закончите.
Во-первых сложность описания типов не связана с надёжностью системы типов. Во-вторых type inference существует не первый год и есть в большинстве мейнстримных функциональных ЯП. Посмотрите алгоритм Хинди-Милнера и в каких языках он используется.
Где-то будете применять стандартные и вот в этом мсете ваша абсолютная заявка стала не абсолютной.
Буду применять стандартные что? И как от этого сломается надёжность системы типов?
ещё раз: ловят они не все ошибки, а убогий процент ошибок, который и без этого не превышал нескольких процентов от всех ошибок. ошибки с типами - мелочь. основные ошибки, которые совершает человек - это ошибки в логике, в стратегии
Вы ссылки на SF и plfa из комментария выше не открывали, верно? Мощные системы типов позволяют писать предикаты проверяемые на этапе компиляции и отлавливают, в том числе, ошибки в логике и стратегии.
Вы победили. положили на алтарь этой проблемы двукратное (минимум!) усложнение кода. Решили 1% возникающих проблем, усугубили 99% остальных проблем.
Как кратность усложнения кода считали? Откуда усугубление проблем взялось? Надеюсь, усложнение считалось не так же как удлинение, а то там нехорошо получилось, и код с типами короче вышел.
И, что характерно, когда Вам на это указывают, когда "на пальцах" разъясняют, когда показывают результаты опроса, вы делаете вид будто "всего этого нет", будто Вы - страус из того мультика.
Ваше объяснение "на пальцах" строится на полном незнании ни теории типов, ни современного ФП. Попробуйте выстроить линию аргументации в которой тезисы более стойкие чем "в ФП всё иммутабельное" и "типы не помогут если перепутать < и <=", которые, очевидно, ложные, о чём вам и в этом посте, и в соседних, не раз сказали.
Вы предложили вариант, который нет не устраняет - всего лишь минимизирует вероятность таких ошибок
Надёжные (sound) cистемы типов не минимизируют вероятность, они исключают ошибки типизации целиком.
И далее, сколько ваше решение стоит в эксплуатации? Много, очень много. А как часто такие ошибки возникали? Редко, очень редко.
Вы уж определитесь. "Много, очень много" стоит внедрение систем доказательств. После написания спецификации они ловят вообще все ошибки. Если же ошибки ловятся "редко, очень редко", то у вас система типов "слабая, очень слабая", а её внедрение, соответственно, "дешёвое, очень дешёвое".
и вы, не желая признавать уже свою ошибку, продолжаете настаивать на ещё большем усугублении ситуации
О какой ошибке речь? Я пока что всё что я утверждал это:
Системы типов позволяют проверять логические утверждения
При достаточном бюджете можно верифицировать все компоненты системы, что вы привели.
Где я утверждал, что кому-либо следует внедрять верификацию в свой проект?
Никак. Это утверждение является недоказуемым и неопровержимым в системе аксиом ZFC
Мнимая
Вся статья наполнена логическими ошибками. Раздел про апорию "Стадий" особенно, поэтому разберу его:
Раз из предположени о двух колесницах мы приходим к абсурду, значит оно ложно. То есть в дискретном мире не может быть двух колесниц едущих навстречу друг другу с такой скоростью.
Далее идёт аналогия с поездами и там закралось следующее утверждение:
Нет, не значит. Эта предпосылка основана лишь на интуитивном понимании движения поездов/колесниц. Её верность в дискретном мире остаётся необоснованной, а раз с ней мы опять приходим к противоречию, то всё что следует из рассуждения в статье это: утверждение "Г1 и В2 должны были сравняться" ложно. Предположение о дискретности так и осталось неопровергнутым
А откуда минус и куда комплексная часть делась?
При ну очень большом желании и ресурсах -- смайнить альтернативную цепочку длиннее основной. Но мне думается, имелось ввиду, что майнеры не будут включать транзакцию в блок, а не что майнеры удалят уже попавшую в блокчейн транзакцию
С моим опытом совпадает лишь отчасти. Можно ссылку на исследование? Плюс, пока неясно как из того, что девушкам приятно обсуждать социальные вопросы следует, что с ними нужно обсуждать социальные вопросы
25% (2/8)
Обе конвенционально красивые
Про интересность художественной литературы это же больше стереотип, разве нет? Я за всю жизнь, наверное, человек двух встречал, которым реально было бы интересно обсуждать художку. В моём кругу общения большая часть бесед это человек А угорел по Х и увлечённо рассказывает человеку Б, где Х варьируется от полиморфных вирусов до алгебраической топологии. У среднего задрота, вероятно, есть множество интересных тем для обсуждения. Понятно, не каждому расскажешь их во всей сложности, но в целом, мне кажется, это не является помехой в общении.
У меня нет интересов за исключением математики и проги (и физики, но это было давно и неправда). Возможно, есть какой-то предварительный фильтр из-за которого мой опыт не является показательным, но, кмк, общение только на эти темы не является проблемой. Мне думается, гораздо больше влияет то, что эти интересы не способствуют социализации, а с малым кругом общения вероятность начать какие-то отношения сильно меньше.
Да нет же, любой кто хоть раз видел promise-ы (также известные как future), асинхронные функции или
flatMapможет понять что такое монадаТолько программисту для реализации плавной анимации это всё знать не нужно. Открывается первый попавшийся сайт с кривыми Безье, и подбираются на глаз параметры. И это если забыть, что можно просто
animation-timing-function: easeсделатьУ меня была проблема не столько с самими закорючками, сколько с их размещением. У юникода множество сабскриптов очень ограниченно. Например
в агде уже не написать, потому что в юникоде нет символа 
.
Можешь привести какой-то пример? Я, кажется, не совсем понимаю что имеется ввиду
Утверждение-то истинное (на ФПМИ в 2021-м нужно было набрать 302 балла за три предмета, линк), но в контексте обсуждения почти бессмысленное: дипломы олимпиад тоже выдаются относительно других участников
Агда очень костыльная в этом плане. Во-первых набор символов сильно ограничен по сравнению с техом, во-вторых нужно искать шрифты поддерживающие закорючки. У Isabelle/HOL, насколько я знаю, в тексте обычные символы, а в редакторе они отображаются как закорючки. Такой подход, кмк, сильно лучше агдовского
Причём это не первая такая статья закинутая в чулан. Сейчас топ чулана это статья @Nurked годовой давности, твоя статья, статья про ковид, и статьи из 2012-го
А ещё есть механизмы построения саморегулируемого сообщества?
У вас 17к просмотров, это в три раза больше чем у топовой статьи в лучшем за сутки, и 79 голосов, это где-то как внизу первой страницы лучшего за неделю.
37 плюсов, 42 минуса. Возможно, дело в качестве статьи, а не в "функционально-типовом сектанстве"
О каком, в таком случае, утраивании, учетверении и до бесконечности идёт речь? Вот исходник map, прямо из ghc-internal:
Три строчки, одна из них это аннотация, которую на самом деле, можно выкинуть, и работает с любыми типами. В обычных языках у вас просто цикл по пришедшему массиву больше строчек займёт
Дженерики (aka параметрический полиморфизм) и АДТ это часть системы типов, а не отдельный инструмент. Интерфейсы (aka классы типов) в хаскеле выражаются через дженерики и АДТ. При большом желании вы можете руками передавать структуры со всеми нужными методами, и не использовать классы типов, но зачем, если компилятор умеет делать эту работу за вас? Возможость опускать типы в коде это вообще синтаксический сахар, поэтому в чём тут проблема мне неясно
Вывод типов не мешает наличию аннотаций. Он делает их проставление опциональным, и злоупотребление выводом действительно усложняет чтение кода. Это непротиворечивый набор утверждений.
Открыл кусок кода со своего пет-проекта. Аннотаций типов на девять строчек целых две:
Не похоже на удвоение.
Вы с дженериками, шаблонами или интерфейсами не сталкивались? Они в мейнстриме лет 30 уже, в 2025-м году нужно постараться найти типизированный язык без чего-то из вышеперечисленного. Но если и правда не сталкивались, вот вам пример обобщённой функции в хаскеле:
Каким боком тут АДТ?
Даже по вашему опросу (репрезентативность которого я ставлю под сомнение), 25% людей чаще сталкиваются с ошибками типов чем с логическими. Это точно крайне редкий класс ошибок?
Вам по существу уже ответили: аннотации типов и безопасность системы типов это вещи никак не связанные. Причём, что характерно, говорить про аннотации типов вы начали. Хинди-Милнер это мимоходом, просто упомянул, что они даже в мощных системах типов далеко не всегда нужны.
Итого: есть два утверждения:
Существует алгоритм вывода типов
Легче читать код с аннотациями типов
В чём противоречие?
Откройте какой-нибудь учебник по теории типов и посмотрите хотя бы Simply Typed Lambda Calculus.
Во-первых сложность описания типов не связана с надёжностью системы типов. Во-вторых type inference существует не первый год и есть в большинстве мейнстримных функциональных ЯП. Посмотрите алгоритм Хинди-Милнера и в каких языках он используется.
Буду применять стандартные что? И как от этого сломается надёжность системы типов?
Вы ссылки на SF и plfa из комментария выше не открывали, верно? Мощные системы типов позволяют писать предикаты проверяемые на этапе компиляции и отлавливают, в том числе, ошибки в логике и стратегии.
Как кратность усложнения кода считали? Откуда усугубление проблем взялось? Надеюсь, усложнение считалось не так же как удлинение, а то там нехорошо получилось, и код с типами короче вышел.
Ваше объяснение "на пальцах" строится на полном незнании ни теории типов, ни современного ФП. Попробуйте выстроить линию аргументации в которой тезисы более стойкие чем "в ФП всё иммутабельное" и "типы не помогут если перепутать < и <=", которые, очевидно, ложные, о чём вам и в этом посте, и в соседних, не раз сказали.
Надёжные (sound) cистемы типов не минимизируют вероятность, они исключают ошибки типизации целиком.
Вы уж определитесь. "Много, очень много" стоит внедрение систем доказательств. После написания спецификации они ловят вообще все ошибки. Если же ошибки ловятся "редко, очень редко", то у вас система типов "слабая, очень слабая", а её внедрение, соответственно, "дешёвое, очень дешёвое".
О какой ошибке речь? Я пока что всё что я утверждал это:
Системы типов позволяют проверять логические утверждения
При достаточном бюджете можно верифицировать все компоненты системы, что вы привели.
Где я утверждал, что кому-либо следует внедрять верификацию в свой проект?