вон в Вашем неправильном примере выше если заменить
Не понял, это что за аргумент? «Есть класс ошибок, которые данная система типов не ловит, поэтому, несмотря на то, что она ловит другой и большой класс ошибок, она ничем не полезна»? Ппц, сгорел сарай — гори и хата.
то Ваш расчудесный компилятор вообще ничего не заметит, однако Вам на это всё равно, главное ведь то, что компилятор замечает.
Расчудесный — заметит. Я просто пишу рядом
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-секспров и не париться. Мы для верификации смарт-контрактов именно так и делали (хотя у нас были отдельные пассы для всяких предметно-специфичных вещей до солвера, но это отдельная и не очень релевантная история).
Меня всегда забавляет¹, как люди по сути требуют от других продемонстрировать их регалии перед тем, как хотя бы даже попытаться воспринять их слова по существу, хотя сами не делают ничего: не демонстрируют собственных достижений (что необходимо в их логике), да и даже не говорят ничего по существу, вместо этого размахивая вокруг вялым адхомом.
¹ вру, раньше расстраивало, а забавляет только последние пару лет
В данном случае, правда, границы чисто синтаксические: вы просто сэмплите не только случайных противников из толпы, но и случайные дисциплины. Свойства категории множеств позволяют переобозначить пары ⟨ противник , дисциплина ⟩ как противник', а соревнование с данным противником в данной дисциплине как игру в шахматы'.
Вы-то говорите, что если этот Вася выигрывает, то и другой Вася выиграет, потому, что оба - Васи.
В данном случае Вася — это определённая кульутра и научная школа. В бинаризованном случае у вас есть ненулевая вероятность, что Вася тот же (научная школа и культура сохранились), и прошлые исходы (косвенно) дают информацию о будущих, и есть ненулевая вероятность, что Васю подменили, и тогда прошлые исходы не дают никакой информации. Легко видеть, что при ненулевой вероятности сохранения Васи при прочих равных (или в отсутствие любой другой информации) наиболее эффективное решение совпадает с тем, как если бы вы считали, что Вася сохранился и остался тем же.
Понятно, что на самом деле там не бинарная вероятность, а вещественный спектр, но идея остаётся та же, просто сумма заменяется интегралом.
Надо просто мыслить вероятностными пространствами, а не скалярами, и всё будет нормально.
Я всё о своих схемах думаю — там именно появляются ограничения, и естественным образом это превращается в типы. С другой стороны, поскольку задача ещё не до конца сформулирована, я в некотором смысле «рисую цель там, куда могу попасть». Но мне нужно знать примерный ландшафт.
Я, к сожалению, про cad знаю слишком мало, чтобы вообще что-то по делу тут предлагать. Нутром чую, что RT тут не сильно помогут, но буду рад ошибиться.
Это работа с Ричадом?
Да.
Но тогда это тип функции, верно?
Это тип одного из аргументов, который торчит в типе функции. Весь тип функции выглядит где-то как
{ a : ℝ | True } → { b : ℝ | a ≥ b } → { r : ℝ | r × r = a - b }
(refinement на r можно ослабить, понятное дело)
То есть, из предметной области вытаскиваем язык (алгебру в терминах ADD)
В таком виде у этого языка не нужна предметно-специфичная система типов. Все нужные ограничения выражаются завтипами на сами элементы алгебры.
Так что вот оно — «настоящее программирование», а не «перекладывание JSON'ов».
Нет, это не ошибка горячей руки, потому что здесь нет случайного события (да и в большинстве случаев применения термина «ошибка горячей руки» искомые события тоже не были совсем случайными — у когнитивного искажения, сводящегося к некорректному применению лейблов других когнитивных искажений, наверняка тоже есть какое-нибудь название).
Если Вася систематически выигрывает в шахматы у рандомно взятого из толпы человека, то это повышает шансы, что он выиграет и у следующего рандомно взятого из толпы человека просто потому, что наблюдаемые данные («Вася выигрывает») повышают вероятность того, что мы живём в мире, где Вася действительно хороший шахматист на фоне среднего человека.
Конечно, процитированную вами фразу вашего исходного собеседника надо исправить на «и скорее всего так будет с Китаем», но на практике при человеческом языке отсылка к вероятностному мышлению опускается.
Не понял, это что за аргумент? «Есть класс ошибок, которые данная система типов не ловит, поэтому, несмотря на то, что она ловит другой и большой класс ошибок, она ничем не полезна»? Ппц, сгорел сарай — гори и хата.
Расчудесный — заметит. Я просто пишу рядом
и доказываю их как теоремы. Всё, тесты на эти случаи больше писать даже не надо, потому что это лучше, чем соответствующие тесты — у них здесь есть квантор всеобщности, а ваш средний юнит-тест проверяет один-два примера, и всё.
Но это агда или идрис. Тем временем даже в хаскеле типы могут помочь, потому что я могу записать эти свойства как утверждения для 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-секспров и не париться. Мы для верификации смарт-контрактов именно так и делали (хотя у нас были отдельные пассы для всяких предметно-специфичных вещей до солвера, но это отдельная и не очень релевантная история).
Конечно. Всё самое интересное случается в комплитайме.
Меня всегда забавляет¹, как люди по сути требуют от других продемонстрировать их регалии перед тем, как хотя бы даже попытаться воспринять их слова по существу, хотя сами не делают ничего: не демонстрируют собственных достижений (что необходимо в их логике), да и даже не говорят ничего по существу, вместо этого размахивая вокруг вялым адхомом.
¹ вру, раньше расстраивало, а забавляет только последние пару лет
У каждой аналогии свои границы применимости.
В данном случае, правда, границы чисто синтаксические: вы просто сэмплите не только случайных противников из толпы, но и случайные дисциплины. Свойства категории множеств позволяют переобозначить пары ⟨ противник , дисциплина ⟩ как противник', а соревнование с данным противником в данной дисциплине как игру в шахматы'.
В данном случае Вася — это определённая кульутра и научная школа. В бинаризованном случае у вас есть ненулевая вероятность, что Вася тот же (научная школа и культура сохранились), и прошлые исходы (косвенно) дают информацию о будущих, и есть ненулевая вероятность, что Васю подменили, и тогда прошлые исходы не дают никакой информации. Легко видеть, что при ненулевой вероятности сохранения Васи при прочих равных (или в отсутствие любой другой информации) наиболее эффективное решение совпадает с тем, как если бы вы считали, что Вася сохранился и остался тем же.
Понятно, что на самом деле там не бинарная вероятность, а вещественный спектр, но идея остаётся та же, просто сумма заменяется интегралом.
Надо просто мыслить вероятностными пространствами, а не скалярами, и всё будет нормально.
Я, к сожалению, про cad знаю слишком мало, чтобы вообще что-то по делу тут предлагать. Нутром чую, что RT тут не сильно помогут, но буду рад ошибиться.
Да.
Это тип одного из аргументов, который торчит в типе функции. Весь тип функции выглядит где-то как
(refinement на r можно ослабить, понятное дело)
В таком виде у этого языка не нужна предметно-специфичная система типов. Все нужные ограничения выражаются завтипами на сами элементы алгебры.
Только не нужно никому, и бабок не платят, увы.
Нет, это не ошибка горячей руки, потому что здесь нет случайного события (да и в большинстве случаев применения термина «ошибка горячей руки» искомые события тоже не были совсем случайными — у когнитивного искажения, сводящегося к некорректному применению лейблов других когнитивных искажений, наверняка тоже есть какое-нибудь название).
Если Вася систематически выигрывает в шахматы у рандомно взятого из толпы человека, то это повышает шансы, что он выиграет и у следующего рандомно взятого из толпы человека просто потому, что наблюдаемые данные («Вася выигрывает») повышают вероятность того, что мы живём в мире, где Вася действительно хороший шахматист на фоне среднего человека.
Конечно, процитированную вами фразу вашего исходного собеседника надо исправить на «и скорее всего так будет с Китаем», но на практике при человеческом языке отсылка к вероятностному мышлению опускается.