По идее должно хорошо и просто работать в ФП языках так как там нет мутаций. Если разрешать мутации, то сразу много выплывает тонких кейсов, так что всё равно придется какие-то корректные вещи запрещать.
Ну вот например удалять из коллекции можно всегда — это не приведёт к проблемам типизации. Это на самом деле чудовищная тема если начать её копать, особенно если отойти от абстрактных вещей к конкретным. Я советую для разминки потратить где-то пол часа жизни что бы разобраться почему метод HashMap.get в Rust принимает не тип ключа K, а новый тип Q, который такой что
Вот кстати интересный пример про книгу. Скажем Преступление и наказание около 600 страниц. И в начале, если помните, там главный герой убивает старушку, а ещё свидетельницу: молодую девушку. Однако, в конце книге про свидетельницу нет уже ни слова. А была бы у Достоевского статическая типизация, книга бы до печати не дошла пока бы он не поправил несоответствия. Ну и подобных историй в литературе предостаточно.
Что касается концепций, признаться не могу понять в чем аргумент. У меня например постоянно такое, что концепции одинаковые (по крайней мере в моей голове), а код всё таки приходится подправлять.
Я бы почитал вашу статью так что обязательно пишите.
Сам я не писал серьезно на ДТ языках поэтому в целом я готов принять какие-то убедительные доводы. Однако ваши вызываю у меня вопросы.
вы концентрируетесь над потоком исполнения, контекст движется вместе с этим потоком и вам очевидно что происходит вокруг
Звучит так, как будто программа пишется так же, как исполняется её исходный код, в виде некоторого пайплайна. Однако, на практике написание программы скорее напоминает переусложнённую версию игры в Дженга, где вам приходится расширять программу изнутри периодически выделяя общие паттерны в мини-фреймворки, попутно удаляя неиспользуемое легаси. Более того сам характер взаимосвязей между компонентами не похож на поток: низкоуровневые компоненты переиспользуются многократно причем на разных абстрактных уровнях.
Сам я сталкивался с таким, что разработчик, не осилив написать типобезопасную версию апи, оставлял торчать Object-ы в декларациях или явные касты в коде и в результате тривиальный рефакторинг ломал всю программу, но понятно это было только при запуске тестов, а хочется же во время компиляции.
в этих языках важно писать как можно проще (явно как завещал Гвидо), компактнее и выбирать максимально читабельные и полные названия для всего
Писать так программы хорошо на любом языке, но тут мне кажется есть некоторая подмена понятий: хорошо писать код, который выглядит просто и понятно, но писать такой код совсем не просто: от того и идет «когнитивная нагрузка». Более того, если вы пишете библиотечный код, то самое главное, что бы им было просто и удобно пользоваться, а это зачастую значит писать очень сложный код внутри самой библиотеки.
Говорю же тут немного плавую. Знаю что изоморфизм есть, но не знал даже как он называется:) Про термы не понял, что такое терм в данном случае? Какое-то объявление типа или выражение?
И кстати как тебе статья в целом? Твое мнение было бы мне важно т.к. я на несколько твоих статей опираюсь здесь и даю на них ссылки:)
С утра ещё подумал и надо наверное пояснить почему программа это теорема. Теорема по сути это набор аксиом и последовательность применённых к ним правил вывода. А программа это набор входных типов и последовательность функций которые переводят один тип в другой. Компилятор верифицирует, что действительно есть такие функции, которые могут так трансформировать типы. Верификация теоремы проверяет, что действительно все правила вывода применены корректно. Один и тот же процесс по сути, только вместо типов утверждения. Легко показать, что для любой теоремы существует эквивалентная ей программа, так как надо всего лишь задать по типу для каждого утверждения. В обратную сторону это тоже работает. Если выписать все функции как правила вывода, а все типы как утверждения.
Без Гёделя возникает мысль что раз доказательство наличия свойства я пишу сам, то может быть удастся его построить даже если в общем виде такая задача невычислима. Гëдель же говорит, что доказательства нет вовсе.
Там кстати метод обхода похожий: делаешь функцию с кастом, но безопасным — как бы добавляешь геделевскую теорему как аксиому.
Я в этой теме плавую, но в моем понимании это примерно одно и тоже, просто с разных точек зрения. Теорема Райса говорит, что наличие свойств, скажем, отсутствие ошибок некоторого типа невычислимы. А я предлагаю взглянуть на программу как на доказательство теоремы о своей корректности в узком смысле, и тогда можно рассуждать в рамках теоремы Гёделя.
Наверное ссылка на Райса вызвала бы меньше вопросов, но мне кажется важным акцентировать внимание на том, что не просто компилятор проверяет какие-то свойства как бы сам по себе, а что код программы является доказательством наличия этих свойств, которое верифицирует компилятор.
Грубо говоря, когда ты пишешь программу на статически типизированном языке ты как бы пишешь две программы одним и тем же кодом: вычисление над типами и вычисление над данными. Про первое мне кажется удобнее рассуждать в терминах теорем, а про второе в терминах вычислимости и свойств.
«Делать нормально» и «получать рыночную зп» это две разные вещи совершенно. Рыночная зп — это достижимая цель, путем просвещения разработчиков на тему манипуляций: когда люди начнут чаще голосовать ногами, компании будут вынуждены подстроиться. Просвещать на эту тему мы можем себя только сами: я думаю нет нужды объяснять почему государственная система образования никогда не будет просвещать людей в этом направлении?)
«Делать нормально» — это совсем другая история. Компанию интересует прибыль и это нормально. Вас, наверное, интересует не только прибыль, и это тоже нормально. Этот конфликт интересов нормален и неустраним. Поэтому важно иметь пет-проджект для души. Не надо просто связывать свою жизнь и, скажем так, стремление к искусству с работой на компанию. Дело в том, что вы человек, а компания это общее дело объединяющая людей на тему подзаработать денег. Любой отдельно взятый человек всегда хочет большего чем денег, но для каждого человека в компании это «большее» разное.
Демократия не равно хорошо. Демократия это инклюзивный инструмент минимизации урона от конфиктов в обществе, если процедура прозрачна. Вместе с тем, демократия, если процедура не прозрачна, хороший инструмент манипуляции общественным мнением.
Но разработчика это всё не должно интересовать так как тут речь идёт не о государстве, а о рынке: сменить компанию проще простого. Ты можешь получать столько денег и других благ, сколько тебе готовы заплатить. Соответственно при твоем личном рациональном поведении ты получаешь всегда более менее адекватную зарплату, независимо от того, как устроена процедура ревью в отдельно взятой компании.
Степень нечестности ревью, просто пропорциональна рациональности разработчиков: если люди ведутся на манипуляцию, она будет выгодна компании, а если не ведутся тогда компания сделает себе хуже т.к. вообще потери от ухода разработчика, который проработал год и более довольно большие.
Performance review это на самом деле очень хитрый механизм очень похожий на механизмы контролируемой репрезентативной демократии. Грубо говоря вы делаете инклюзивную процедуру с непрозрачным подведением итогов и добиваетесь двух целей: во-первых непрозрачное подведение итогов позволяет вам контролировать конечный результат, когда это необходимо, во-вторых участие лигитимизирует результат в глазах участников.
Таким образом этот механизм может быть использован (а значит рано или поздно будет), для объяснения недоплатны сотруднику относительно его рыночной стоимости. Обычно пока компания растет всё ок, но когда у неё кризис, тогда неожиданные результаты ревью и прилетают. То есть конечно это всё манипуляция, но относиться к ней надо спокойно и просто ходить на другие интервью получать оферы, не забывать сколько ты на самом деле стоишь и не вестись на газлайтинг.
Ничто не мешает иметь модульность и сообщения со статической типизацией. Надежность системы это вопрос архитектуры прежде всего, а язык здесь играет роль второго плана. При этом я понимаю аргумент, что язык со статической типизацией и мощной системой типов в теории позволяет создать более надежный и менее хрупкий код, который сложнее сломать случайной правкой. При этом есть контраргумент, что статическая типизация расслабляет разработчиков и они реже пишут тесты. Здесь есть о чем спорить. Но заявлять что динамический язык повысит надежность системы это просто странно.
В комментариях верно упомянули про Erlang и странную классификацию по которой Java и C# стали языками с динамической типизацией, а PHP противопоставляется WordPress (на котором он написан).
От себя хочу добавить вот что. Я понимаю, что у разработчиков на динамических языках все обложено тестами, но в качестве плюса динамической типизации упоминать антихрупкость, хотя очевидно, что дополнительные проверки типов как минимум не увеличивают вероятность ошибок, это по моему пропаганда уровня «война — это мир».
Эм. Если упрощать я написал "Сократ — это человек. Все люди смертны. Следовательно Сократ смертен". Вы мне отвечаете "Плохое у вас определение Сократа, под него каждый человек подходит". Но я определения не давал, а выделил сущностные свойства для рассуждения.
В статье все неправильно.
Во-первых профсоюзы — это общественный институт, который выступает за права людей и изменения в законодательстве. Профсоюзы пожалуй следующая по политичности вещь после избирательной гонки.
Во-вторых мантра «если ты не готов идти на митинг, то не надо возмущаться» — может служить хорошим предлогом, что бы не делать вообще ничего, но не мотивирует людей на поступки. Так же она не отражает потенциальных политических последствий — если вы их хотите оценить. Вы можете не ходить на митинг, но поддерживать деньгами НКО. Вообще-то разделение труда — это эффективный механизм: да я плохо знаю законы, я плохой журналист, но я хороший разработчик и могу скинуться журналисту на онлайн из зала суда, а адвокату на работу.
В-третьих забудьте вообще об IT. Профсоюзов которые могут защитить права работника во всех отраслях в сумме можно пересчитать по пальцам одной руки. В стране где большинство граждан — это низкооплачиваемые наемные рабочие. Так может происходить по одной единственной причине, но кажется политики на сегодня достаточно, так что сами подумайте по какой.
В нашем проекте мы решаем эту проблему как в питоне — джентльменским соглашением. Считается что List всегда неизменяемый, если только он не создан локально в текущем методе и тогда лучше пользоваться явным типом ArrayList например. Стараемся не передавать в методы изменяемые коллекции, но если очень надо передаём лямбду List::add а принимаем консьюмер. Конечно хуже, чем в Rust, но кажется самый адекватный выход.
Здесь создается регексп сперва на каждую строчку в файле а потом и на каждое слово. IDEA умеет выносить за скобочки такое.
Collectors.counting
— аллоцирует Long на каждый инкремент (по крайней мере в Java 8). Знаю это довольно позорно, но это так. Тут либо можно написать свой MutableLong и реализовать редьюсер самому, либо взять сторонний Object2LongMap где можно эффективно инкрементить значения.
Ещё связка sort().limit(10) — у меня нет уверенности что там используется какой-то эффективный алгоритм, скорее всего сортируется вся последовательность целиком. Самый быстрый способ на коленки сделать лучше: положить все ентри в PriorityQueue (внутри там бинарная куча на массиве) через конструктор, а потом достать первые 10 элементов. Фокус в том, что можно за линию собрать кучу из массива. Главное не добавлять элементы по одному. Можно реализовать с помощью к-той порядковой статистики алгоритм эффективнее по памяти но это немного муторно.
На самом деле распределенные транзакции много где есть сегодня. Например в Apache Ignite. Двухфазный комит — стандартный алгоритм для этого и позволяет сделать CP систему с шардированием. Задержки там не очень большие если одновременно работающие транзакции в данных редко пересекаются. Но конечно если начать join запросы тяжёлые 1 в 1 с MySQL переносить на такое, то будет больно)
Ну вот например удалять из коллекции можно всегда — это не приведёт к проблемам типизации. Это на самом деле чудовищная тема если начать её копать, особенно если отойти от абстрактных вещей к конкретным. Я советую для разминки потратить где-то пол часа жизни что бы разобраться почему метод HashMap.get в Rust принимает не тип ключа K, а новый тип Q, который такой что и
doc.rust-lang.org/std/collections/struct.HashMap.html#method.get
Что касается концепций, признаться не могу понять в чем аргумент. У меня например постоянно такое, что концепции одинаковые (по крайней мере в моей голове), а код всё таки приходится подправлять.
Сам я не писал серьезно на ДТ языках поэтому в целом я готов принять какие-то убедительные доводы. Однако ваши вызываю у меня вопросы.
Звучит так, как будто программа пишется так же, как исполняется её исходный код, в виде некоторого пайплайна. Однако, на практике написание программы скорее напоминает переусложнённую версию игры в Дженга, где вам приходится расширять программу изнутри периодически выделяя общие паттерны в мини-фреймворки, попутно удаляя неиспользуемое легаси. Более того сам характер взаимосвязей между компонентами не похож на поток: низкоуровневые компоненты переиспользуются многократно причем на разных абстрактных уровнях.
Сам я сталкивался с таким, что разработчик, не осилив написать типобезопасную версию апи, оставлял торчать Object-ы в декларациях или явные касты в коде и в результате тривиальный рефакторинг ломал всю программу, но понятно это было только при запуске тестов, а хочется же во время компиляции.
Писать так программы хорошо на любом языке, но тут мне кажется есть некоторая подмена понятий: хорошо писать код, который выглядит просто и понятно, но писать такой код совсем не просто: от того и идет «когнитивная нагрузка». Более того, если вы пишете библиотечный код, то самое главное, что бы им было просто и удобно пользоваться, а это зачастую значит писать очень сложный код внутри самой библиотеки.
И кстати как тебе статья в целом? Твое мнение было бы мне важно т.к. я на несколько твоих статей опираюсь здесь и даю на них ссылки:)
С утра ещё подумал и надо наверное пояснить почему программа это теорема. Теорема по сути это набор аксиом и последовательность применённых к ним правил вывода. А программа это набор входных типов и последовательность функций которые переводят один тип в другой. Компилятор верифицирует, что действительно есть такие функции, которые могут так трансформировать типы. Верификация теоремы проверяет, что действительно все правила вывода применены корректно. Один и тот же процесс по сути, только вместо типов утверждения. Легко показать, что для любой теоремы существует эквивалентная ей программа, так как надо всего лишь задать по типу для каждого утверждения. В обратную сторону это тоже работает. Если выписать все функции как правила вывода, а все типы как утверждения.
Без Гёделя возникает мысль что раз доказательство наличия свойства я пишу сам, то может быть удастся его построить даже если в общем виде такая задача невычислима. Гëдель же говорит, что доказательства нет вовсе.
Там кстати метод обхода похожий: делаешь функцию с кастом, но безопасным — как бы добавляешь геделевскую теорему как аксиому.
Я в этой теме плавую, но в моем понимании это примерно одно и тоже, просто с разных точек зрения. Теорема Райса говорит, что наличие свойств, скажем, отсутствие ошибок некоторого типа невычислимы. А я предлагаю взглянуть на программу как на доказательство теоремы о своей корректности в узком смысле, и тогда можно рассуждать в рамках теоремы Гёделя.
Наверное ссылка на Райса вызвала бы меньше вопросов, но мне кажется важным акцентировать внимание на том, что не просто компилятор проверяет какие-то свойства как бы сам по себе, а что код программы является доказательством наличия этих свойств, которое верифицирует компилятор.
Грубо говоря, когда ты пишешь программу на статически типизированном языке ты как бы пишешь две программы одним и тем же кодом: вычисление над типами и вычисление над данными. Про первое мне кажется удобнее рассуждать в терминах теорем, а про второе в терминах вычислимости и свойств.
«Делать нормально» — это совсем другая история. Компанию интересует прибыль и это нормально. Вас, наверное, интересует не только прибыль, и это тоже нормально. Этот конфликт интересов нормален и неустраним. Поэтому важно иметь пет-проджект для души. Не надо просто связывать свою жизнь и, скажем так, стремление к искусству с работой на компанию. Дело в том, что вы человек, а компания это общее дело объединяющая людей на тему подзаработать денег. Любой отдельно взятый человек всегда хочет большего чем денег, но для каждого человека в компании это «большее» разное.
Поэтому надо просвещать разработчиков на тему социальных наук:)
Но разработчика это всё не должно интересовать так как тут речь идёт не о государстве, а о рынке: сменить компанию проще простого. Ты можешь получать столько денег и других благ, сколько тебе готовы заплатить. Соответственно при твоем личном рациональном поведении ты получаешь всегда более менее адекватную зарплату, независимо от того, как устроена процедура ревью в отдельно взятой компании.
Степень нечестности ревью, просто пропорциональна рациональности разработчиков: если люди ведутся на манипуляцию, она будет выгодна компании, а если не ведутся тогда компания сделает себе хуже т.к. вообще потери от ухода разработчика, который проработал год и более довольно большие.
Таким образом этот механизм может быть использован (а значит рано или поздно будет), для объяснения недоплатны сотруднику относительно его рыночной стоимости. Обычно пока компания растет всё ок, но когда у неё кризис, тогда неожиданные результаты ревью и прилетают. То есть конечно это всё манипуляция, но относиться к ней надо спокойно и просто ходить на другие интервью получать оферы, не забывать сколько ты на самом деле стоишь и не вестись на газлайтинг.
От себя хочу добавить вот что. Я понимаю, что у разработчиков на динамических языках все обложено тестами, но в качестве плюса динамической типизации упоминать антихрупкость, хотя очевидно, что дополнительные проверки типов как минимум не увеличивают вероятность ошибок, это по моему пропаганда уровня «война — это мир».
Эм. Если упрощать я написал "Сократ — это человек. Все люди смертны. Следовательно Сократ смертен". Вы мне отвечаете "Плохое у вас определение Сократа, под него каждый человек подходит". Но я определения не давал, а выделил сущностные свойства для рассуждения.
Во-первых профсоюзы — это общественный институт, который выступает за права людей и изменения в законодательстве. Профсоюзы пожалуй следующая по политичности вещь после избирательной гонки.
Во-вторых мантра «если ты не готов идти на митинг, то не надо возмущаться» — может служить хорошим предлогом, что бы не делать вообще ничего, но не мотивирует людей на поступки. Так же она не отражает потенциальных политических последствий — если вы их хотите оценить. Вы можете не ходить на митинг, но поддерживать деньгами НКО. Вообще-то разделение труда — это эффективный механизм: да я плохо знаю законы, я плохой журналист, но я хороший разработчик и могу скинуться журналисту на онлайн из зала суда, а адвокату на работу.
В-третьих забудьте вообще об IT. Профсоюзов которые могут защитить права работника во всех отраслях в сумме можно пересчитать по пальцам одной руки. В стране где большинство граждан — это низкооплачиваемые наемные рабочие. Так может происходить по одной единственной причине, но кажется политики на сегодня достаточно, так что сами подумайте по какой.
Эм… Вообще за участие в успешной революции обычно расстреливают спустят пару лет) Так, для справки чисто. Это не абсолютное правило конечно.
Местами прямо очень хорошо.
В нашем проекте мы решаем эту проблему как в питоне — джентльменским соглашением. Считается что List всегда неизменяемый, если только он не создан локально в текущем методе и тогда лучше пользоваться явным типом ArrayList например. Стараемся не передавать в методы изменяемые коллекции, но если очень надо передаём лямбду List::add а принимаем консьюмер. Конечно хуже, чем в Rust, но кажется самый адекватный выход.
Здесь создается регексп сперва на каждую строчку в файле а потом и на каждое слово. IDEA умеет выносить за скобочки такое.
— аллоцирует Long на каждый инкремент (по крайней мере в Java 8). Знаю это довольно позорно, но это так. Тут либо можно написать свой MutableLong и реализовать редьюсер самому, либо взять сторонний Object2LongMap где можно эффективно инкрементить значения.
Ещё связка sort().limit(10) — у меня нет уверенности что там используется какой-то эффективный алгоритм, скорее всего сортируется вся последовательность целиком. Самый быстрый способ на коленки сделать лучше: положить все ентри в PriorityQueue (внутри там бинарная куча на массиве) через конструктор, а потом достать первые 10 элементов. Фокус в том, что можно за линию собрать кучу из массива. Главное не добавлять элементы по одному. Можно реализовать с помощью к-той порядковой статистики алгоритм эффективнее по памяти но это немного муторно.
На самом деле распределенные транзакции много где есть сегодня. Например в Apache Ignite. Двухфазный комит — стандартный алгоритм для этого и позволяет сделать CP систему с шардированием. Задержки там не очень большие если одновременно работающие транзакции в данных редко пересекаются. Но конечно если начать join запросы тяжёлые 1 в 1 с MySQL переносить на такое, то будет больно)