Ну и в языках с динамической типизацией тип является частью значения, поэтому коммутативность плюса явно запрещает определять тип по первому операнду.
Не понял. Из коммутативности плюса следует, что оба операнда абсолютно равноправны с точки зрения определения типов. Если вы запретили использовать первый, то и второй нелзья (потому что a + b = b + a, и, следовательно, ∀P. P(a + b) ⇒ P(b + a)).
Допустим в baz ошибка, которую мы поймали и обработали в foo.
А проблема в том, что источником ошибки может быть неверный код в функции bar. А когда пользователь смотрит на текст ошибки выброшенный функцией foo, он bar и baz не видит.
Не понял, мы ж ошибку поймали и обработали, что там ещё foo выбрасывает, что связано с bar и baz?
Но вообще это всё оттого, что у вас все ошибки — текст, и вообще всё — текст, даже в примере выше, который якобы должен был показать хорошие практики программирования. Естественно в таком случае у вас будет боль и страдание.
А если вместо текста ошибки (обработка которого, сюрприз, не проверяется компилятором) использовать нормальные типы для этих ошибок, в контексте которых понятно, откуда они берутся, то и проблемы такой нет. Оказывается, что вам больше не нужны коллстеки (которые компилятором могут быть обезображены до неузнаваемости из-за инлайнинга, например, или которые вообще могут быть иррелевантны в случае глубоко асинхронного кода), чтобы понять, что вообще происходит.
Но да, продолжайте сообщать об ошибках строками и винить тупых непониматоров из раста, зачем-то впихивающих специальный синтаксис для нормальной обработки ошибок. Бездна вашего непрофессионализма настолько глубока, что мне стрёмно за яндекс даже несмотря на то, что я к нему отношусь негативно по политическим причинам.
Так чё там как, в эрланге мутабельность-то есть? А то вы ключевой вопрос пропустили, а он ключевой потому, что:
вы говорите, что википедия — топ авторитет, и вся ваша дискуссия опирается на этот тезис
википедия говорит, что эрланг — это ФП
википедия говорит, что ФП — это чистота
известно, что в эрланге есть мутабельность (ETS и erlang:put/2 вместе с erlang:get/1)
Найти противоречие в этой системе утверждений (при некоторых дополнительных естественных вводных) смогёте?
Или можно взять ML (или ocaml) — википедия говорит, что он functional programming language, хотя там мутабельность огого (и, из моего опыта, разбираться в коде на окамле сильно неприятнее, чем на хаскеле).
"очевидный" - является аргументом
Нет, это констатация факта.
Исходный оратор сказал про лёгкость рефакторинга в ФП, я (практикующий ФП) понял, о чём он и какое определение ФП он имеет в виду, и девять из десяти (или 99 из 100) других практикующих ФП, поймут и/или уже поняли, о чём он (потому что те практикующие, что есть на хабре, уже правильно понимали аналогичные высказывания в других тредах, или сами их высказывали).
Эта ситуация подходит под семантику фразы «практикующим очевидно, что…».
Вы понимаете о чём говорите (но, увы, доказывать не собираетесь)
Эмпирический пример с type-driven-рефакторингом выше, где мне вообще не пришлось включать мозги, чтобы поправить код под изменившиеся семантические требования.
Более того, пример выше показывает, что для придуманной вами же задачи мне потребовалось меньше кода, код чище, тестируемее, и так далее. К вашему коду можно задать пару дюжин вопросов, не связанных с синтаксисом и семантикой самого языка, о поведении и состоянии разных стейтментов, к моему — сильно меньше.
Да вот беда: от перекладывания JSON'ов есть реальная польза
Я не зря написал про подмножество перекладывателей — тех, у кого при этом ещё воинственная безграмотность.
а от Ваших типов её нет.
А у этого утверждения есть какие-то доказательства, или вы доказательства только от окружающих требуете?
Видите ли, когда вы вот тут текст публикуете, то он тоже где-то в виде JSON'ов перекладывается туда-сюда.
Какая польза от опубликованного здесь мной (или вами) текста?
"подкатить к тёлочке" и коррекция сознания с заигрываниями/флиртом - это тоже часть этого. вы явно недооцениваете насколько широко гормоны и "прошивка это ф-ции" влияют на сознание..
Угу, ведь нам всем известны успехи едва половоззрелых пацанов на романтическом поле, у которых это самое сознание само отключается под влиянием гормональной бури-перестройки. Ведь всё именно так и происходит: в 12-15 лет все успешны, а потом навыки общения с девушками теряются под воздействием успокаивающихся гормонов и начинающего преобладать сознания.
вот "не могу взять и не мешать" - это тараканы в голове, вы буквально сами себя уговариваете что "это невозможно", хотя это не так.
Я говорю о том, что не всё ограничивается тем, что там якобы что-то мешает.
У человека как минимум может сбоить эта самая прошивка, и он может некорректно воспринимать и обрабатывать социальные сигналы, например. Этакий лёгкий аутизм, который не мешает на работе или в магазине, но мешает в построении отношений. А оно куда более тонкое и куда более чувствительно к отклонениям, кстати, потому что весь смысл всего этого дейтинга с точки зрения прошивок и прочих эволюций — отбраковать паршивые гены (что для нашего социального вида подразумевает в том числе своего рода неконформность, которую мне лень определять точно, но, надеюсь, смысл понятен).
а у вас какая проблема? у вас узкий кругозор? физиологические проблемы? или "я обычный парень, не могу выделится из толпы"?
У меня нет проблемы, потому что у меня нет незакрытых потребностей: я просто перестал испытывать потребность в паре. И, более того, от одной мысли о том, чтобы с кем-то знакомиться, общаться, ходить, свидания, и так далее, меня не то что тошнит, а выворачивает.
Раньше у меня была проблема с тем, что у меня, во-первых, не было времени, во-вторых, вокруг на одну девушку было в среднем 20-50 парней, и, в-третьих, у меня узкий иррелевантный кругозор. Я неспособен систематически и эффективно использовать общение для социального груминга (хотя я могу обсудить, например, опять же, эволюционные аспекты и теории развития языка для этого самого социального груминга, заодно против других теорий развития языка, и смежных вопросов), и у меня нет жизненного опыта, который был бы релевантен и интересен.
Если вам мешают моральные установки - рассмотрите их переоценку например...
О, ну это отдельный философский вопрос вообще. Если начинать переоценивать моральные установки каждый раз, как они в чём-то мешают, то это не установки, а фигня какая-то. Типа, «воровать нехорошо, но вон кошелёк с 10000000 долларами лежит, а мне деньги полезны будут, пойду переоценю свои установки, они чё-т мешают».
а вот то что мы обсуждаем, наш организм ВСЕГДА и у ВСЕХ имеет генетическую предрасположенность на эти действия и ограничиваеть его могут только мозги, которые с точки зрения физиологие думают чтото лишнее
А, не, ложная тревога.
Вот как вы просто не можете взять и за пять минут просто увидеть, как решать произвольную задачу, так и кто-то не может просто взять и «не мешать», или «быть собой», или подберите эвфемизм этому социальному процессу по вашему вкусу.
потому что так и надо сделать, ну? этот механизм не управляется сознанием напрямую...надо просто не мешать ему
Не управляется сознанием сунуть-вынуть (да и то вопрос спорный). Жить и взаимодействовать в человеческом обществе с другим человеком — без сознания тут никуда. Даже более примитивные животные, чем мы, это сознание используют.
вон в Вашем неправильном примере выше если заменить
Не понял, это что за аргумент? «Есть класс ошибок, которые данная система типов не ловит, поэтому, несмотря на то, что она ловит другой и большой класс ошибок, она ничем не полезна»? Ппц, сгорел сарай — гори и хата.
то Ваш расчудесный компилятор вообще ничего не заметит, однако Вам на это всё равно, главное ведь то, что компилятор замечает.
Расчудесный — заметит. Я просто пишу рядом
transfer-withdraws : (from to : UserId)
→ (amount : Nat)
→ (accounts : AccountsMap)
→ transfer from to amount accounts ≡ Success accounts'
→ balance (lookup from accounts) ≡ balance (lookup from accounts') + amount
transfer-adds : (from to : UserId)
→ (amount : Nat)
→ (accounts : AccountsMap)
→ transfer from to amount accounts ≡ Success accounts'
→ balance (lookup to accounts') ≡ balance (lookup to accounts) + amount
transfer-no-effect : (from to other : UserId)
→ other ≢ from × other ≢ to
→ (amount : Nat)
→ (accounts : AccountsMap)
→ transfer from to amount accounts ≡ Success accounts'
→ balance (lookup other accounts') ≡ balance (lookup other accounts)
transfer-preserves : (from to : UserId)
→ (amount : Nat)
→ (accounts : AccountsMap)
→ transfer from to amount accounts ≡ Success accounts'
→ totalBalance accounts ≡ totalBalance accounts'
и доказываю их как теоремы. Всё, тесты на эти случаи больше писать даже не надо, потому что это лучше, чем соответствующие тесты — у них здесь есть квантор всеобщности, а ваш средний юнит-тест проверяет один-два примера, и всё.
Но это агда или идрис. Тем временем даже в хаскеле типы могут помочь, потому что я могу записать эти свойства как утверждения для quickcheck'а, который по типам сам выведет и сгенерирует произвольное количество тестовых примеров и проверит, что эти условия выполняются. Да, не доказательства, но для обычных опердней сойдёт.
критерий "лучше" "хуже" без приведения доказательств - это только эмоциональная оценка.
Окей, я запомню это определение в разговоре с вами, равно как и вашу любовь к доказательствам очевидных для практикующих людей утверждений.
мы же с Вами выяснили, что сами по себе типы присутствуют во многих языках и это от ФП или НП не зависит
Нет, мы это не выяснили. Это вы сделали некорректную бинаризацию.
Речь о выразительной силе этих типов. Ежу понятно, что типы есть и в C (или в Go вон), но они там скорее помогают машине сгенерировать более эффективный код, а не человеку писать код более эффективно.
вот вот, нахватались звона про типы и айда этот звон повсюду распространять
Разница в том, что в моём случае это не звон, и я понимаю, о чём говорю.
Ещё раз: функциональный стиль программирования потому и сектантский, что базируется на понятиях "чистый" и "греховный", а греховность она именно от мутабельности
Ага, а ООП — сексистский, потому что объектифицирует, да?
«Чистый» — это исключительно технический термин, точно так же как «open neighborhood» — термин, а не приглашение пожить рядом с математиком-топологом. Пытаться в этом найти какие-то скрытые смыслы — это трэш уровня задорновщины.
чтобы не мараться в мутабельности вы и мучаетесь с рекурсиями и всеми прочими "миссионерскими" позами
Зачем? Где в коде выше рекурсия и какие-то позы? Получилось короче, понятнее и тестируемее, чем у вас, пока вы там, чтобы сократить количество кода, даже решили скипнуть оформление этого в какой-то цельный кусок, опять же.
ага, будь Ваша воля - на кострах бы жгли?
Будь моя воля, я бы ушёл затворником в леса, лишь бы не пересекаться с перекладывателями жсонов с Даннингом-Крюгером. Но, к сожалению, выращивать еду я сам не умею, а оттуда всё по наклонной.
А, и, кстати, я с непривычки не осилил поместить весь контекст вашего вопроса в голову, особенно на фоне императивного кода без единого типа (говорю ж, ФП расслабляет), и поэтому я не возвращаю новые балансы юзеров — не заметил это требование, сорри (которое бы, отмечу, заметил компилятор, если бы я где-то использовал эту функцию, где нужны балансы).
Сначала я хотел просто исправить комментарий, а потом подумал, что это будет хорошим упражнением для демонстрации рефакторинга. Итак, в текущем варианте я возвращаю новую мапу, которая функцией splitValidation приводится в удобный для stateTVar формат. Тип splitValidation:
splitValidation :: (s → Validation e s) → s → (Validation e (), s)
Мне надо возвращать дополнительные данные, поэтому я изменяю его на
splitValidation :: (s → Validation e (res, s)) → s → (Validation e res, s)
и смотрю, что скажет компилятор. Компилятор недоволен вызовом transfer под splitValidation, потому что splitValidation возвращает не то:
• Couldn't match type: AccountsMap with: ((), AccountsMap)
Оки, меняем тип transfer под splitValidation на ((Int, Int), AccountsMap) , и заодно меняем возвращаемый тип transferSTM на STM (Validation [TransferError] (Int, Int)) .
и всё. Мне ни разу не потребовалось даже запустить тесты.
А, нет, не всё. Так как я привык к equational reasoning'у, дваinsert подряд автоматически вызывает у меня вопрос: а что должно произойти, если id1 = id2? С этим вопросом можно либо пойти к аналитику, либо постулировать, что переводы себе — noop, добавив, например, в начале ещё одну проверку ровно на это, либо потребовать аргумент-доказательство, что эти два пользователя разные (но тут надо будет хаскель заменить на идрис), что будет самым адекватным решением (потому что если мы разрешим id1 = id2, то это сломает ряд интуитивно очевидных законов, которым должна подчиняться эта функция).
Типы и иммутабельные рассуждения снова помогают, и я ведь всё ещё не написал ни единого теста. А учитывая, что люди часто пишут тесты уровня «проверили один-два оптимистичных случая, вроде норм», то тестам доверия нет.
Окей. Так как вы топите за ООП и википедию, то поясните, пожалуйста, где в примере выше у вас наследование, полиморфизм, инкапсуляция, и так далее? Выходит, на деле даже для такого важного перекладывателя жсонов, зрящего в суть и указующего путь, как вы, ООП неприменим?
ну не знаю, например привести оценку частотности ошибок с типами.
Это не показывает простоту рефакторинга, потому что то, что компилятор закрывает типами, перекладыватели жсонов вроде вас покрывают адовой кучей тестов (причём, дублируя по факту реализацию, потому что мыслить в терминах свойств вы неспособны). Поэтому вам и нужно по 10 сторипоинтов на перекладывание одного жсона.
По моей статистике ошибок в логике - 99%, а ошибок в типах не более 1%.
По моей статистике 99% ошибок, которые я делаю в C++, исключаются системой типов хаскеля, и 99% ошибок в хаскеле исключаются системой типов идриса.
ну в вопросе кто более авторитетен: википедия или иуиуиу - я выберу первую.
Лучше бы было, конечно, выбрать разобраться в вопросе, но это путь для слабых духом. Сильные выбирают полагаться на авторитеты.
При этом обычные ЯП не чураются ФП подходов (например Rust) в то время, как ФП считают мутабельность нечистой (здесь сравнение с сектами уместно), греховной. И вынуждены сами преодолевать свои же рамки: сочиняя монады
Так я не понял, есть в ФП мутабельность или нет в итоге? А то её у вас то нет, то вон монады сочинили (хотя те же монадические парсеры на комбинаторах — тоже монады, и какое там состояние вообще, если это декларативный предметноспецифичный язык).
И чем монады — плохо? Может, у вас ООП тоже плохое, потому что там придумали, что всё надо декомпозировать на объекты, и даже пришлось для этого придумать специально классы, чтобы «преодолевать свои рамки»?
и АДТ.
Причём АДТ к стейту?
это Вы просто не пробовали писать ничего сложнее генератора ряда Фибоначчи (да и его, как правило, пишете неверно).
Ну хотя бы в интернете мне наконец-то расскажут, что я там пишу.
У вас там как, фабрика синглтонов печатальщиков hello world уже получилась, готовы перейти к гавкающим кошечкам и собачкам?
попробуйте например на языке SQL выразить следующую задачу:
Почему на SQL? Причём тут вообще SQL? С каких пор SQL — функциональный типизированный ЯП общего назначения?
нужно перевести 100 долларов с балланса пользователя 1 на баланс пользователя 2, при условии, что баланса у него достаточно и оба пользователя незаблокированы
Чё-т такое:
transfer :: UserId → UserId → Nat → AccountsMap → Validation [TransferError] AccountsMap
transfer id1 id2 amount accounts = do
let Just user1 = lookup id1 accounts
Just user2 = lookup id2 accounts
when (isLocked user1) $ Failure [AccountLocked id1]
when (isLocked user2) $ Failure [AccountLocked id2]
when (amount > balance user1) $ Failure [InsufficientFunds]
pure $ adjust (decreaseBalance amount) id1
$ adjust (increaseBalance amount) id2
$ accounts
transferSTM :: TVar AccountsMap → UserId → UserId → Nat → STM (Validation [TransferError] ())
transferSTM accountsTVar id1 id2 amount = stateTVar accountsTVar $ splitValidation $ transfer id1 id2 amount
А вы, кстати, забыли обработать возможность отсутствия юзера (тут я для честности пошёл по вашим стопам, хотя компилятор протестует) и не указали, какой из двух заблокирован (тут — решил указать). Плюс непонятно, может ли обломиться update или нет (и типы этого не скажут), и что в таком случае будет с транзакцией — закроется сама? Будет висеть? account1, который вернулся из accounts.get — это глубокая копия, или какой-то референс? При его обновлении оно обновляется в хранилище? Как связано transaction и accounts? Какие ещё вещи прикрываются transaction? Что будет, если я верну account1 из функции вне transaction и попробую его подёргать? Рантайм-ошибка? Обновится вне транзакции? Обновится ссылка вникуда и это будет noop?
А хрен его знает — ответ на все эти вопросы. Нужно написать больше тестов.
Плюс, это не оформлено у вас в функцию, и непонятно, как это тестировать. У меня же отдельно бизнес-логика в чистой функции без состояния, которую тестировать очень просто (включая property-тесты), а вся грязь-мутабельность — отдельным однострочником (который тестировать просто не нужно).
Когда у вас объём кода перейдёт экранов за пять, подумайте о том, что в реальной жизни и условий перевода денег больше и комиссии всякие встречаются (а не только блокировки) и так далее.
Не перешло — даже меньше получилось, чем у вас, хотя вы о тестировании, о заворачивании в какой-то семантически полный кусок кода вроде функции или класса там, и так далее, даже не заморачивались.
Не получится об этом подумать :(
Я указал на бездоказательность утверждения, Вы продолжили напирать на эмоциональную сферу.
Я не мог продолжить, потому что это был мой первый тезис вам на эту тему.
Что эмоционального в том, что код поддерживать проще, и что код надёжнее?
Типы к функциональному программированию отношения не имеют.
Сегодня — имеют.
Определение ФП из 60-х как того, где можно передавать функции в функции, к счастью, уже в прошлом (вместе с подавляющим большинством языков, где это не так). В C++, в питоне, в го вроде как, и так далее, можно передавать что угодно куда угодно (пусть иногда и с костылями), но это очевидно не делает их функциональными языками, поэтому с этим определением перестали бегать лет 10 назад.
Теперь перекладыватели жсонов (или балансов) с синдромом Даннинга-Крюгера (да, я знаю, что его не существует) нахватались звона про «иммутабельность» и вместо прошлых рассказов про «функции передавать в функции возвращать функции из функции ситизены первого класса» бегают с этой иммутабельностью, снова не понимая, зачем это надо, причём это к программированию, и какие у неё границы применимости и средства обеспечения. Более того, синдром Даннинга-Крюгера не позволяет перекладывателю хотя бы попробовать совместить свои утверждения с реальностью, где и в хаскеле, и в идрисе мутабельность есть (и не только монадами), что не делает их менее функциональными, и хотя бы попытаться подумать, что же в их по верхам нахватанных «знаниях» не так. Ведь если факты противоречат теории, то тем хуже для фактов.
Более того, этим людям плевать, как термины используются на практике в каком контексте — ведь они что-то где-то услышали, а разбираться-то после этого уже не нужно.
Поэтому да, то, что сегодня практикующие ФП люди понимают под этим самым ФП — это про контроль эффектов и инвариантов компилятором (и это, очевидно, ровно то определение, которое имел в виду ваш исходный собеседник, говоря о простоте рефакторинга). А контроль эффектов и инвариантов при компиляции мы умеем делать только типами (практически по определению типов), поэтому ФП — это про типы.
Есть Go с типами
На которые смотреть больно.
Есть LISP с динамической типизацией
Про который есть шутка: lisp — это такой язык, про который сишники говорят «а, это тот ненужный функциональный язык», а хаскелисты говорят «а, это тот ненужный императивный язык».
А если без шуток, то рефакторить код на лиспе — так себе удовольствие. Почему? Потому, что типов нет.
В общем, отношения к типам у всех разное и ФП здесь не несут ничего особенного.
А в эрланге «нет мутабельности»?
Понимаю, что поскольку энциклопедия противоречит вере (для сектантов это типично), то аргумент о неавторитетности энциклопедии будет базовым.
Какой вере? Это вопрос терминов, не более. Хотите называть лисп или эрланг функциональными — я не против, но их не имеют в виду, когда говорят о лёгкости рефакторинга. Человек, разбирающийся в теме, способен выполнить разрешение неоднозначностей, чтобы понять, какой сорт функциональщины имеется в виду, вы — нет, только и всего.
Вероятно именно поэтому Вы ходите из треда в тред с рассказами о боге, хрусте французской булки, превосходных качествах функционального программинга.
Вы всё ещё не заметили, что я отвечал на ваш комментарий другому человеку, или вы просто теперь будете прямо врать?
И вот эти пенсионеры не используют ни классы, ни паттерны, ни SOLID и никакие другие аналогичные вещи. И разобраться в коде COBOL-а, Fortran-а ой как проблематично.
Может, тут есть какая-то связь?
То, что выдается за хороший код и называется хорошим, это больше вопрос привычки.
Там же рядом, кстати, написано, что википедия не явялется авторитетным источником. На фактологические косяки в википедии (особенно в русской версии) я натыкался чуть чаще, чем хотелось бы.
однако АДТ - это способ уклониться от указания и обработки эффектов в типах. Это попытка вернуться к динамической типизации :)
С чего бы?
Конечно, чем больше ваши АДТ (и чем менее точны типы — вы можете вообще писать всё в IO, например), тем меньше вы можете сказать о поведении функции, глядя на её тип, но ФП бьёт за это по рукам и стимулирует выражаться точнее. В отличие от ООП.
Поэтому работать над ФП-проектами (на ФП-языках, конечно, а не когда ФП пытаются сделать, не знаю, на джаваскрипте или питоне) — одно удовольствие, а над ООП — погибель и статьи уровня исходной.
Знаете, с моей колокольни это вы ходите из треда в тред с похожими мифами про функциональное программирование, ну а я вынужден это комментировать.
Учитывая, что мой первый комментарий на этой странице был ответом на ваш, где вы уже что-то прокомментировали, то с вашей колокольни открывается какая-то альтернативная реальность. Но это, впрочем, не новость.
С бездоказательной заявки о том, что ФП лучше.
Только оно действительно лучше. Потому что оно стимулирует выражать вещи в типах, и это приводит к более поддерживаемому и надёжному коду.
Как доказывать, что рефакторить типизированный код проще, в рамках одного комментария на хабре — хз.
вот я могу так сказать, я вообще не умею в литкод, что не мешает мне быть сеньором
А я ни разу не решал литкод-задачи, что не мешало мне пройти влёт без подготовки интервью в гугл для себя самого и в другой фаанг за знакомого (тоже без подготовки, и сидя рядом и решая задачи на какой-нибудь динпрог, параллельно печатая ему, что он должен говорить, чтобы симулировать мыслительный процесс — это, если что, сильно сложнее, чем просто решать задачи).
Поэтому не понимаю, зачем люди готовятся к интервью в гугл. Им мешают сугубо внутриголовные тараканы! Надо просто верить в себя 💪💪💪 и не заморачиваться 🙌🙌🙌, и интервью 🎯🎯🎯 пройдётся 🚀🚀🚀, ведь вы огонь 🔥🔥🔥 и всё, что нужно для успеха 🏆🏆🏆, у вас уже есть 📚📚📚 !!!
Извините, примерно так (как последний абзац), для меня выглядят все эти рассуждения про изи поиск пары, стоит только открыть чакры и не париться. Я понимаю, что вы это говорите из лучших побуждений, но это не возымеет эффект на тех, кому это релевантно, и будет воспринято исключительно как самокрасование (как предпоследний абзац).
В N+1-й раз напишу вам, что ФП не отрицает мутабельность. ФП отрицает неуказание эффектов в типах.
Так как я пишу это в N+1-й раз для сильно ненулевого N, то позволю себе спросить: зачем вы из треда в тред ходите с похожими мифами и тезисами, и как только вам указывают на неконсистентность или некорректность ваших высказываний, вы из треда пропадаете, чтобы через какое-то время снова появиться в другом треде с тем же самым?
Советуете почитать конкретно с точки зрения честности изложения?
Я не нашёл существенных изъянов и биасов, особенно в первой из книг. «The Vision», конечно, биаснута, потому что показывает ментальную акробатику соответствующих людей, но каких-то серьёзных косяков и там не заметил (хотя, опять же, не со всем согласен).
У Соуэла в Basic Economics - просто постоянно biased примеры.
Basic Economics у него я не читал, а, кстати, интересно!
(ну условно сравнил мат-ожидание "парвильной страны" с медианой "неправильной страны")
Для некоторых распределений это норм, кстати. И чем более равномерное распределение (если говорить о доходах, например, к этому вроде даже стремятся), тем ближе матожидание к медиане.
Это я бы сказал «ну вообще в чём проблема с поиском работы, что вы всё переживаете и дрючите литкод, посмотрите вообще каких клоунов нанимают, и у меня никаких проблем с этим никогда не было, я просто не парюсь».
А потом надо искать фиксированную точку. Например, простой итерацией. Или двух фазным вычислением как в NSpice (первая фаза грубая, вторая - Ньютон-Рафсон).
Ой всё. Я лучше уволюсь, чем буду формализовывать вот эти все вычислительные методы.
Это всё проще в SMT загнать, сформулировать ограничения в терминах допусков, и пусть оно там проверяет.
То есть, получается, что типы простые, без полиморфизма, без функций высших порядков (можно их добавить, но это только усложнит инструмент без пользы). С другой стороны, ограничения явно есть, но не очень понятно пока, какие именно.
Ну как всегда — попробуй накидать примеры программ, какие ограничения хотелось бы навесить, а там уже можно будет делать выводы, наверное.
Опять же, я, к сожалению, предметную область дальше курса общефиза не знаю (и общефиз был давно), поэтому интуиции здесь у меня нет.
Но они же получаются связаны через функцию! То есть, для определения точного типа b нужно знать a.
Да, RT — это подвид зависимых типов. С некоторыми оговорками можно воспринимать их как сигма-типы (где, как я теперь знаю, второй аргумент стёрт aka рантайм-иррелевантен).
Там есть теоремы, с какими наборами подобных условий можно работать?
В общем виде — нет (и что-то окологёделевское говорит нам, что алгоритма, разрешающего разрешимость теории, не существует). Но в твоём случае вроде как достаточно стандартного SMT, и это хорошо: не надо заморачиваться.
Хотя в случае небольших количеств переменных (до десятков тысяч), с условно паскалевской изначальной системой типов, должно позволять добавление вот этих ограничений из твоего примера легко, верно?
Более-менее лёгкую арифметику — да.
И даже Z3 не надо - можно для таких размеров (до 10к переменных) всё сделать самостоятельно, да?
Если тебе охота поиграться с самодельным солвером, я бы делал это как отдельный проект :]
SMT очень нетривиальные, с кучей крайних случаев, и они могут подыхать даже на довольно малых наборах констрейнтов. Десятки тысяч переменных — это уже дофига. Лучше дёргать какой-нибудь z3 (haskell-z3 норм байндинги) или за вечер наваять парсер/генератор smtlib-секспров и не париться. Мы для верификации смарт-контрактов именно так и делали (хотя у нас были отдельные пассы для всяких предметно-специфичных вещей до солвера, но это отдельная и не очень релевантная история).
Не понял. Из коммутативности плюса следует, что оба операнда абсолютно равноправны с точки зрения определения типов. Если вы запретили использовать первый, то и второй нелзья (потому что a + b = b + a, и, следовательно, ∀P. P(a + b) ⇒ P(b + a)).
Не понял, мы ж ошибку поймали и обработали, что там ещё
fooвыбрасывает, что связано сbarиbaz?Но вообще это всё оттого, что у вас все ошибки — текст, и вообще всё — текст, даже в примере выше, который якобы должен был показать хорошие практики программирования. Естественно в таком случае у вас будет боль и страдание.
А если вместо текста ошибки (обработка которого, сюрприз, не проверяется компилятором) использовать нормальные типы для этих ошибок, в контексте которых понятно, откуда они берутся, то и проблемы такой нет. Оказывается, что вам больше не нужны коллстеки (которые компилятором могут быть обезображены до неузнаваемости из-за инлайнинга, например, или которые вообще могут быть иррелевантны в случае глубоко асинхронного кода), чтобы понять, что вообще происходит.
Но да, продолжайте сообщать об ошибках строками и винить тупых непониматоров из раста, зачем-то впихивающих специальный синтаксис для нормальной обработки ошибок. Бездна вашего непрофессионализма настолько глубока, что мне стрёмно за яндекс даже несмотря на то, что я к нему отношусь негативно по политическим причинам.
Так чё там как, в эрланге мутабельность-то есть? А то вы ключевой вопрос пропустили, а он ключевой потому, что:
вы говорите, что википедия — топ авторитет, и вся ваша дискуссия опирается на этот тезис
википедия говорит, что эрланг — это ФП
википедия говорит, что ФП — это чистота
известно, что в эрланге есть мутабельность (ETS и
erlang:put/2вместе сerlang:get/1)Найти противоречие в этой системе утверждений (при некоторых дополнительных естественных вводных) смогёте?
Или можно взять ML (или ocaml) — википедия говорит, что он functional programming language, хотя там мутабельность огого (и, из моего опыта, разбираться в коде на окамле сильно неприятнее, чем на хаскеле).
Нет, это констатация факта.
Исходный оратор сказал про лёгкость рефакторинга в ФП, я (практикующий ФП) понял, о чём он и какое определение ФП он имеет в виду, и девять из десяти (или 99 из 100) других практикующих ФП, поймут и/или уже поняли, о чём он (потому что те практикующие, что есть на хабре, уже правильно понимали аналогичные высказывания в других тредах, или сами их высказывали).
Эта ситуация подходит под семантику фразы «практикующим очевидно, что…».
Эмпирический пример с type-driven-рефакторингом выше, где мне вообще не пришлось включать мозги, чтобы поправить код под изменившиеся семантические требования.
Более того, пример выше показывает, что для придуманной вами же задачи мне потребовалось меньше кода, код чище, тестируемее, и так далее. К вашему коду можно задать пару дюжин вопросов, не связанных с синтаксисом и семантикой самого языка, о поведении и состоянии разных стейтментов, к моему — сильно меньше.
Я не зря написал про подмножество перекладывателей — тех, у кого при этом ещё воинственная безграмотность.
А у этого утверждения есть какие-то доказательства, или вы доказательства только от окружающих требуете?
Какая польза от опубликованного здесь мной (или вами) текста?
Угу, ведь нам всем известны успехи едва половоззрелых пацанов на романтическом поле, у которых это самое сознание само отключается под влиянием гормональной бури-перестройки. Ведь всё именно так и происходит: в 12-15 лет все успешны, а потом навыки общения с девушками теряются под воздействием успокаивающихся гормонов и начинающего преобладать сознания.
Я говорю о том, что не всё ограничивается тем, что там якобы что-то мешает.
У человека как минимум может сбоить эта самая прошивка, и он может некорректно воспринимать и обрабатывать социальные сигналы, например. Этакий лёгкий аутизм, который не мешает на работе или в магазине, но мешает в построении отношений. А оно куда более тонкое и куда более чувствительно к отклонениям, кстати, потому что весь смысл всего этого дейтинга с точки зрения прошивок и прочих эволюций — отбраковать паршивые гены (что для нашего социального вида подразумевает в том числе своего рода неконформность, которую мне лень определять точно, но, надеюсь, смысл понятен).
У меня нет проблемы, потому что у меня нет незакрытых потребностей: я просто перестал испытывать потребность в паре. И, более того, от одной мысли о том, чтобы с кем-то знакомиться, общаться, ходить, свидания, и так далее, меня не то что тошнит, а выворачивает.
Раньше у меня была проблема с тем, что у меня, во-первых, не было времени, во-вторых, вокруг на одну девушку было в среднем 20-50 парней, и, в-третьих, у меня
узкийиррелевантный кругозор. Я неспособен систематически и эффективно использовать общение для социального груминга (хотя я могу обсудить, например, опять же, эволюционные аспекты и теории развития языка для этого самого социального груминга, заодно против других теорий развития языка, и смежных вопросов), и у меня нет жизненного опыта, который был бы релевантен и интересен.О, ну это отдельный философский вопрос вообще. Если начинать переоценивать моральные установки каждый раз, как они в чём-то мешают, то это не установки, а фигня какая-то. Типа, «воровать нехорошо, но вон кошелёк с 10000000 долларами лежит, а мне деньги полезны будут, пойду переоценю свои установки, они чё-т мешают».
Ура, вы начинаете что-то понимать!
А, не, ложная тревога.
Вот как вы просто не можете взять и за пять минут просто увидеть, как решать произвольную задачу, так и кто-то не может просто взять и «не мешать», или «быть собой», или подберите эвфемизм этому социальному процессу по вашему вкусу.
Не управляется сознанием сунуть-вынуть (да и то вопрос спорный). Жить и взаимодействовать в человеческом обществе с другим человеком — без сознания тут никуда. Даже более примитивные животные, чем мы, это сознание используют.
Так вы же ООП не используете, потому что как доходит до дела, то все эти три столпа оказываются ненужными. О чём тут ещё говорить?
Что? Как связаны обобщённые алгоритмы и динамическая типизация?
Не понял, это что за аргумент? «Есть класс ошибок, которые данная система типов не ловит, поэтому, несмотря на то, что она ловит другой и большой класс ошибок, она ничем не полезна»? Ппц, сгорел сарай — гори и хата.
Расчудесный — заметит. Я просто пишу рядом
и доказываю их как теоремы. Всё, тесты на эти случаи больше писать даже не надо, потому что это лучше, чем соответствующие тесты — у них здесь есть квантор всеобщности, а ваш средний юнит-тест проверяет один-два примера, и всё.
Но это агда или идрис. Тем временем даже в хаскеле типы могут помочь, потому что я могу записать эти свойства как утверждения для quickcheck'а, который по типам сам выведет и сгенерирует произвольное количество тестовых примеров и проверит, что эти условия выполняются. Да, не доказательства, но для обычных опердней сойдёт.
Окей, я запомню это определение в разговоре с вами, равно как и вашу любовь к доказательствам очевидных для практикующих людей утверждений.
Нет, мы это не выяснили. Это вы сделали некорректную бинаризацию.
Речь о выразительной силе этих типов. Ежу понятно, что типы есть и в C (или в Go вон), но они там скорее помогают машине сгенерировать более эффективный код, а не человеку писать код более эффективно.
Разница в том, что в моём случае это не звон, и я понимаю, о чём говорю.
Ага, а ООП — сексистский, потому что объектифицирует, да?
«Чистый» — это исключительно технический термин, точно так же как «open neighborhood» — термин, а не приглашение пожить рядом с математиком-топологом. Пытаться в этом найти какие-то скрытые смыслы — это трэш уровня задорновщины.
Зачем? Где в коде выше рекурсия и какие-то позы? Получилось короче, понятнее и тестируемее, чем у вас, пока вы там, чтобы сократить количество кода, даже решили скипнуть оформление этого в какой-то цельный кусок, опять же.
Будь моя воля, я бы ушёл затворником в леса, лишь бы не пересекаться с перекладывателями жсонов с Даннингом-Крюгером. Но, к сожалению, выращивать еду я сам не умею, а оттуда всё по наклонной.
А, и, кстати, я с непривычки не осилил поместить весь контекст вашего вопроса в голову, особенно на фоне императивного кода без единого типа (говорю ж, ФП расслабляет), и поэтому я не возвращаю новые балансы юзеров — не заметил это требование, сорри (которое бы, отмечу, заметил компилятор, если бы я где-то использовал эту функцию, где нужны балансы).
Сначала я хотел просто исправить комментарий, а потом подумал, что это будет хорошим упражнением для демонстрации рефакторинга. Итак, в текущем варианте я возвращаю новую мапу, которая функцией
splitValidationприводится в удобный дляstateTVarформат. ТипsplitValidation:Мне надо возвращать дополнительные данные, поэтому я изменяю его на
и смотрю, что скажет компилятор. Компилятор недоволен вызовом
transferподsplitValidation, потому чтоsplitValidationвозвращает не то:Оки, меняем тип
transferподsplitValidationна((Int, Int), AccountsMap), и заодно меняем возвращаемый типtransferSTMнаSTM (Validation [TransferError] (Int, Int)).Дальше я меняю последние три строки на, например:
и всё. Мне ни разу не потребовалось даже запустить тесты.
А, нет, не всё. Так как я привык к equational reasoning'у, два
insertподряд автоматически вызывает у меня вопрос: а что должно произойти, еслиid1 = id2? С этим вопросом можно либо пойти к аналитику, либо постулировать, что переводы себе — noop, добавив, например, в начале ещё одну проверку ровно на это, либо потребовать аргумент-доказательство, что эти два пользователя разные (но тут надо будет хаскель заменить на идрис), что будет самым адекватным решением (потому что если мы разрешимid1 = id2, то это сломает ряд интуитивно очевидных законов, которым должна подчиняться эта функция).Типы и иммутабельные рассуждения снова помогают, и я ведь всё ещё не написал ни единого теста. А учитывая, что люди часто пишут тесты уровня «проверили один-два оптимистичных случая, вроде норм», то тестам доверия нет.
Окей. Так как вы топите за ООП и википедию, то поясните, пожалуйста, где в примере выше у вас наследование, полиморфизм, инкапсуляция, и так далее? Выходит, на деле даже для такого важного перекладывателя жсонов, зрящего в суть и указующего путь, как вы, ООП неприменим?
Это не показывает простоту рефакторинга, потому что то, что компилятор закрывает типами, перекладыватели жсонов вроде вас покрывают адовой кучей тестов (причём, дублируя по факту реализацию, потому что мыслить в терминах свойств вы неспособны). Поэтому вам и нужно по 10 сторипоинтов на перекладывание одного жсона.
По моей статистике 99% ошибок, которые я делаю в C++, исключаются системой типов хаскеля, и 99% ошибок в хаскеле исключаются системой типов идриса.
Лучше бы было, конечно, выбрать разобраться в вопросе, но это путь для слабых духом. Сильные выбирают полагаться на авторитеты.
Так я не понял, есть в ФП мутабельность или нет в итоге? А то её у вас то нет, то вон монады сочинили (хотя те же монадические парсеры на комбинаторах — тоже монады, и какое там состояние вообще, если это декларативный предметноспецифичный язык).
И чем монады — плохо? Может, у вас ООП тоже плохое, потому что там придумали, что всё надо декомпозировать на объекты, и даже пришлось для этого придумать специально классы, чтобы «преодолевать свои рамки»?
Причём АДТ к стейту?
Ну хотя бы в интернете мне наконец-то расскажут, что я там пишу.
У вас там как, фабрика синглтонов печатальщиков hello world уже получилась, готовы перейти к гавкающим кошечкам и собачкам?
Почему на SQL? Причём тут вообще SQL? С каких пор SQL — функциональный типизированный ЯП общего назначения?
Чё-т такое:
А вы, кстати, забыли обработать возможность отсутствия юзера (тут я для честности пошёл по вашим стопам, хотя компилятор протестует) и не указали, какой из двух заблокирован (тут — решил указать). Плюс непонятно, может ли обломиться
updateили нет (и типы этого не скажут), и что в таком случае будет с транзакцией — закроется сама? Будет висеть?account1, который вернулся изaccounts.get— это глубокая копия, или какой-то референс? При его обновлении оно обновляется в хранилище? Как связаноtransactionиaccounts? Какие ещё вещи прикрываютсяtransaction? Что будет, если я вернуaccount1из функции внеtransactionи попробую его подёргать? Рантайм-ошибка? Обновится вне транзакции? Обновится ссылка вникуда и это будет noop?А хрен его знает — ответ на все эти вопросы. Нужно написать больше тестов.
Плюс, это не оформлено у вас в функцию, и непонятно, как это тестировать. У меня же отдельно бизнес-логика в чистой функции без состояния, которую тестировать очень просто (включая property-тесты), а вся грязь-мутабельность — отдельным однострочником (который тестировать просто не нужно).
Не перешло — даже меньше получилось, чем у вас, хотя вы о тестировании, о заворачивании в какой-то семантически полный кусок кода вроде функции или класса там, и так далее, даже не заморачивались.
Не получится об этом подумать :(
Я не мог продолжить, потому что это был мой первый тезис вам на эту тему.
Что эмоционального в том, что код поддерживать проще, и что код надёжнее?
Сегодня — имеют.
Определение ФП из 60-х как того, где можно передавать функции в функции, к счастью, уже в прошлом (вместе с подавляющим большинством языков, где это не так). В C++, в питоне, в го вроде как, и так далее, можно передавать что угодно куда угодно (пусть иногда и с костылями), но это очевидно не делает их функциональными языками, поэтому с этим определением перестали бегать лет 10 назад.
Теперь перекладыватели жсонов (или балансов) с синдромом Даннинга-Крюгера (да, я знаю, что его не существует) нахватались звона про «иммутабельность» и вместо прошлых рассказов про «функции передавать в функции возвращать функции из функции ситизены первого класса» бегают с этой иммутабельностью, снова не понимая, зачем это надо, причём это к программированию, и какие у неё границы применимости и средства обеспечения. Более того, синдром Даннинга-Крюгера не позволяет перекладывателю хотя бы попробовать совместить свои утверждения с реальностью, где и в хаскеле, и в идрисе мутабельность есть (и не только монадами), что не делает их менее функциональными, и хотя бы попытаться подумать, что же в их по верхам нахватанных «знаниях» не так. Ведь если факты противоречат теории, то тем хуже для фактов.
Более того, этим людям плевать, как термины используются на практике в каком контексте — ведь они что-то где-то услышали, а разбираться-то после этого уже не нужно.
Поэтому да, то, что сегодня практикующие ФП люди понимают под этим самым ФП — это про контроль эффектов и инвариантов компилятором (и это, очевидно, ровно то определение, которое имел в виду ваш исходный собеседник, говоря о простоте рефакторинга). А контроль эффектов и инвариантов при компиляции мы умеем делать только типами (практически по определению типов), поэтому ФП — это про типы.
На которые смотреть больно.
Про который есть шутка: lisp — это такой язык, про который сишники говорят «а, это тот ненужный функциональный язык», а хаскелисты говорят «а, это тот ненужный императивный язык».
А если без шуток, то рефакторить код на лиспе — так себе удовольствие. Почему? Потому, что типов нет.
А в эрланге «нет мутабельности»?
Какой вере? Это вопрос терминов, не более. Хотите называть лисп или эрланг функциональными — я не против, но их не имеют в виду, когда говорят о лёгкости рефакторинга. Человек, разбирающийся в теме, способен выполнить разрешение неоднозначностей, чтобы понять, какой сорт функциональщины имеется в виду, вы — нет, только и всего.
Вы всё ещё не заметили, что я отвечал на ваш комментарий другому человеку, или вы просто теперь будете прямо врать?
Может, тут есть какая-то связь?
Да не, ерунда какая-то.
Там же рядом, кстати, написано, что википедия не явялется авторитетным источником. На фактологические косяки в википедии (особенно в русской версии) я натыкался чуть чаще, чем хотелось бы.
С чего бы?
Конечно, чем больше ваши АДТ (и чем менее точны типы — вы можете вообще писать всё в
IO, например), тем меньше вы можете сказать о поведении функции, глядя на её тип, но ФП бьёт за это по рукам и стимулирует выражаться точнее. В отличие от ООП.Поэтому работать над ФП-проектами (на ФП-языках, конечно, а не когда ФП пытаются сделать, не знаю, на джаваскрипте или питоне) — одно удовольствие, а над ООП — погибель и статьи уровня исходной.
Учитывая, что мой первый комментарий на этой странице был ответом на ваш, где вы уже что-то прокомментировали, то с вашей колокольни открывается какая-то альтернативная реальность. Но это, впрочем, не новость.
Только оно действительно лучше. Потому что оно стимулирует выражать вещи в типах, и это приводит к более поддерживаемому и надёжному коду.
Как доказывать, что рефакторить типизированный код проще, в рамках одного комментария на хабре — хз.
Что это всегда сугубо внутренние тараканы.
А я ни разу не решал литкод-задачи, что не мешало мне пройти влёт без подготовки интервью в гугл для себя самого и в другой фаанг за знакомого (тоже без подготовки, и сидя рядом и решая задачи на какой-нибудь динпрог, параллельно печатая ему, что он должен говорить, чтобы симулировать мыслительный процесс — это, если что, сильно сложнее, чем просто решать задачи).
Поэтому не понимаю, зачем люди готовятся к интервью в гугл. Им мешают сугубо внутриголовные тараканы! Надо просто верить в себя 💪💪💪 и не заморачиваться 🙌🙌🙌, и интервью 🎯🎯🎯 пройдётся 🚀🚀🚀, ведь вы огонь 🔥🔥🔥 и всё, что нужно для успеха 🏆🏆🏆, у вас уже есть 📚📚📚 !!!
Извините, примерно так (как последний абзац), для меня выглядят все эти рассуждения про изи поиск пары, стоит только открыть чакры и не париться. Я понимаю, что вы это говорите из лучших побуждений, но это не возымеет эффект на тех, кому это релевантно, и будет воспринято исключительно как самокрасование (как предпоследний абзац).
В N+1-й раз напишу вам, что ФП не отрицает мутабельность. ФП отрицает неуказание эффектов в типах.
Так как я пишу это в N+1-й раз для сильно ненулевого N, то позволю себе спросить: зачем вы из треда в тред ходите с похожими мифами и тезисами, и как только вам указывают на неконсистентность или некорректность ваших высказываний, вы из треда пропадаете, чтобы через какое-то время снова появиться в другом треде с тем же самым?
Я не нашёл существенных изъянов и биасов, особенно в первой из книг. «The Vision», конечно, биаснута, потому что показывает ментальную акробатику соответствующих людей, но каких-то серьёзных косяков и там не заметил (хотя, опять же, не со всем согласен).
Basic Economics у него я не читал, а, кстати, интересно!
Для некоторых распределений это норм, кстати. И чем более равномерное распределение (если говорить о доходах, например, к этому вроде даже стремятся), тем ближе матожидание к медиане.
Ну и славно: тогда точно не позвонят в три часа ночи, что в продакшене что-то упало.
Это я бы сказал «ну вообще в чём проблема с поиском работы, что вы всё переживаете и дрючите литкод, посмотрите вообще каких клоунов нанимают, и у меня никаких проблем с этим никогда не было, я просто не парюсь».
Ложное обобщение.
Ой всё. Я лучше уволюсь, чем буду формализовывать вот эти все вычислительные методы.
Это всё проще в SMT загнать, сформулировать ограничения в терминах допусков, и пусть оно там проверяет.
Ну как всегда — попробуй накидать примеры программ, какие ограничения хотелось бы навесить, а там уже можно будет делать выводы, наверное.
Опять же, я, к сожалению, предметную область дальше курса общефиза не знаю (и общефиз был давно), поэтому интуиции здесь у меня нет.
Да, RT — это подвид зависимых типов. С некоторыми оговорками можно воспринимать их как сигма-типы (где, как я теперь знаю, второй аргумент стёрт aka рантайм-иррелевантен).
В общем виде — нет (и что-то окологёделевское говорит нам, что алгоритма, разрешающего разрешимость теории, не существует). Но в твоём случае вроде как достаточно стандартного SMT, и это хорошо: не надо заморачиваться.
Более-менее лёгкую арифметику — да.
Если тебе охота поиграться с самодельным солвером, я бы делал это как отдельный проект :]
SMT очень нетривиальные, с кучей крайних случаев, и они могут подыхать даже на довольно малых наборах констрейнтов. Десятки тысяч переменных — это уже дофига. Лучше дёргать какой-нибудь z3 (haskell-z3 норм байндинги) или за вечер наваять парсер/генератор smtlib-секспров и не париться. Мы для верификации смарт-контрактов именно так и делали (хотя у нас были отдельные пассы для всяких предметно-специфичных вещей до солвера, но это отдельная и не очень релевантная история).