Обновить
3
2.1

Специалист по теории типов USB-кабелей

Отправить сообщение

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

Вряд ли на таком определении можно строить какую-то объективную теорию.

А у нас нет объективной теории ООП, инкапсуляции, и тому подобных вещей. Любые попытки построить такую теорию разбиваются о неприменимость её на практике.

Ну или давайте с другой стороны. Что такое по-вашему инкапсуляция?

По сути вы подменили одно умное слово другим умным словом, а это даже как-то не красиво. В таком направлении дискуссия мне не интересна.

Для протокола отмечу, что вы сами начали разговор с того, что написание в ФП-стиле с передачей лямбд в функции может ломать инкапсуляцию, но теперь при попытках поговорить по существу требуете от других прямо определять этот термин. Почему вам не нужно было его определять, когда вы сказали, что инкапсуляция от этого ломается?

Потом сам себя помилует и всех инсайдеров)

Надо продолжать традиции предыдущих президентов!

Edwin Brady — автор единственного в мире по-настоящему строго типизированного языка —: «ну да, ну да, кустарь я».

Ну он же далеко не единственный автор. Вот первая версия:

— на пару с не-рискну-транслитерировать-фамилию.

Вот вторая версия:

(плюс 570 commits 69 663++ 27 241-- в репе с blodwen). Снова далеко не один, и в моём личном опыте я с gallais и buzden встречался в обсуждении пуллреквестов или у них в дискорде сильно чаще, чем с самим Эдвином.

В продакшеге у вас один код который его сетит и он всегда исполняется при инициализации, а в тестах вы резетете его после/перед каждым тестом. Да конечно можно и функцию резет в самом типе реализовать, но она не нужна в продакшнене, а опшионал ее и так реализует.

А если бы вы просто имели параметр в конструкторе, то вам бы не пришлось ничего ресетить: вы просто создаёте новый объект на каждый новый экземпляр класса. Десинглтонизация снова выигрывает!

Я как раз на плюсах и пишу там помимо * и -> есть еще и валью и валью_ор и в 23 ещё и прочие функциональные зены и элсы подвезли.

Запретили уже стайлгайдом или линтером * и ->?

Первый тейк - относится не к невозможности писать в функциональном стиле, а что в сях не очень с полиморфизмом(обойдёмся без void*), и эти требования как то выше не предполагались. Хотя я на функциональных языках не программировал, мб это там повсеместно.

Это там именно что повсеместно. По крайней мере, в ML-семействе.

А второе - да, ошибся, код написал за 3 минуты.

Это как раз норм (для C++), потому что C++ и C не приучают думать в терминах типов. Функциональщик начал бы с написания сигнатуры и автоматически подумал «а как я инт-то верну на пустых входных данных? надо в Maybe завернуться».

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

Человек живёт в стае, а не в парах. Да, человек в среднем моногамен (или скорее полигиничен) на фоне других живых существ, но это не то же самое, что хотеть пару.

Есть альтернативное мнение, что лучше жениться найти долговременного партнёра как раз сильно до 30, чтобы иметь опыт совместного преодоления проблем (и вырабатывать этот опыт на кошках не очень важных проблемах вроде «уволили с первой работы в 23»), потому что это помогает лучше понять, кто рядом с тобой, да и выработать какое-то совместное уважение и, не знаю, признательность, что ли.

И тогда он просто психологически чувствует близкого ему человека с такими же жизненными ценностями и взглядами.

Никого не чувствую в 34 (и никого не хочу чувствовать, перегорело).

Нет, потому что в этих исследованиях рассматриваются не только подобные смерти, но и заболеваемость условным диабетом, депрессией и прочим (чуть ли не Альцгеймером). Холостяки сливают, увы.

У этих сторон сильно разная сила этого форса.

все получится

Учитывая вышесказанное вами про ваши положительные качества — всё больше напоминает все эти мемы-картинки про just be yourself bro and ask her out.

Лет 17-18 (или три четверти карьеры) печального опыта, оставившего такой след, да.

Инкапсуляция — это сокрытие иррелевантных деталей реализации. ООП-модификатор private — это просто частный случай.

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

Но можно и проще (для вас): покажите ФП-пример (раз мы тут ФП обсуждаем), где это ломает инкапсуляцию.

Когда вырастит

Что он вырастит? Геморрой от ночей дебага или шишку на лбу от бития об стол, когда дебаг совсем не удаётся?

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

Почему? Кто мне это в типах гарантирует? Это ведь сломается при малейшем рефакторинге или изменении требований.

Вообще какое-то странное требование, чтобы в тестах нужно было, а так — нет. Можно какой-нибудь пример, чтобы я лучше понимал контекст?

то доступ к значению опшионала кинет исключение или терминирует программу кому как нравится.

А если вы пишете на плюсах (мои искренние соболезнования)? Как там, что у нас operator* и operator-> говорят про пустой опшонал? А, во:

The behavior is undefined if *this does not contain a value.

Всё как всегда в плюсах.

Если же опшионал на самом деле нужен в продакшнене то ваша замена с конструктором не эквивалентна т.к. проверку на пусто кто то где то всё ж таки должен делать.

Я и говорю, что эта замена не эквивалентна, а лучше: проверку нужно делать один раз и в условном main(), а не размазывать её по всей кодовой базе с неясной семантикой на пару.

О, группа Гротендика.

С ней основная проблема в том, что целые числа там — это некоторый класс эквивалентности, а не напрямую единственным образом строящийся терм, а работать с классами эквивалентности в мейнстримных и устоявшихся пруверах исключительно больно, если кубы не гонять, но cubical type theory мы пока не очень понимаем. Возьмите любой результат из гугла по запросу «setoid hell» на ваш вкус.

Другой вопрос — причём тут вообще пруверы, но это уже моя профдеформация. На бумажке при разговоре с другим человеком с группой Гротендика всё норм.

Я, видимо, не очень понятно написал - разумеется, DSL.

Тогда да, ADD Магвайра, и формально доказывать выписанные для комбинаторов законы (и требовать в типах комбинаторов нужный контекст, если оно вылезает из законов).

Проблема в том, что я не очень понимаю, как из этой идеи выжать всё. В смысле, как понять, что можно ещё куда-то двинуться, или же наоборот, там всё украдено до нас.

Попытаться опубликовать статью и посмотреть на реакцию ревьюверов :]

Я подозреваю, что это не совсем то.

ХЗ, но я всё равно нашёл: https://arxiv.org/pdf/2111.10867

Думаю, что оно может оказаться релевантнее, чем кажется сходу.

Это означает какие операции к ним применимы, и их свойства.

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

Ну нет, так не пойдёт. Если следовать вашей логике, то вы не используете русский.

Я на всякий случай напомню о том, что русский язык — это не наука, а набор соглашений, а лингвистика — ну так, наука немножко (на самом деле вообще настолько наука, насколько гуманитарная вещь может быть наукой). Поэтому у слова «использовать» во фразах «использовать русский язык» и «использовать лингвистику/математику» несколько разная семантика (ну, как у «побег», который сериал из нулевых, и «побег», который у растений).

Поэтому да, в предыдущем абзаце я использую русский язык, но определять «использую $science» или «знаю $science» так, чтобы предыдущий абзац был заодно примером использования лингвистики, очень странно (но если хочется считать себя лингвистом, то можно, конечно, и так определить, кто ж запретит).

И аналогично говорить, что я знаю математику русский язык, если я пишу неправильно, но носитель русского языка всё равно может меня понять (то есть, если я достигаю цели использования языка) — это тоже очень нетипичное использование термина «знаю».

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

Вы всё ещё не отличаете «использовать результаты» от «знать, откуда они берутся»?

А я не знаю лингвистику, значит я не пишу на русском и не знаю его, интересно как же вы понимаете меня?

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

Естественно, желательно с доказательством и анализом, а то как я пойму математику вы мне объясняете, или же зазубренными аксиомами кидаетесь уровня grokking algorithms.

А кто мне мешает скопипастить из учебника?

Это ничего не объясняет

Зависит от языка, которым вы пользуетесь. Если человек достаточно интернализировал понятие морфизма и функториальности, то ему это скажет более чем нужно. Если же нет — ну, тут каждый из этих терминов раскрывается в несколько предложений.

как говорил Фейнман "Если вы не можете что-то объяснить ребенку, то вы этого не понимаете сами"

Ну объясните ребёнку квантмех или ОТО, пожалуйста, а я на это посмотрю.

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

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

Зависит от вашей формализации целых чисел (группа Гротендика, прямое построение как индуктивный тип поверх натуральных с двумя конструкторами nonneg : ℕ → ℤ и neg : ℕ → ℤ, или что-то ещё по вашему вкусу). Впрочем, во всех этих формализациях умножение дистрибутивно относительно сложения и коммутативно (что доказывается зависимо от формализации), а сложение формирует группу, где -x — (единственный, как и в любой группе) обратный к x, поэтому:

  1. ∀x, y. xy + (-x)y =[ дистрибутивность] (x + -x)y =[ -x обратный к x] 0y =[ определение умножения ] 0

    (-x)y =[единственность обратного] -(xy)

  2. ∀x, y. (-x)(-y) =[ п. 1 ] -(x(-y)) =[ коммутативность ] -((-y)x) =[ п. 1 ] -(-(yx)) =[ групповые свойства обратных ] yx =[ коммутативность ] xy

  3. Инстанциируем для x = y = -3: -3 × -3 = 3 × 3 = 9.

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

Правда, в некоторых формализациях (например, стандартной агдовской) умножение определяется как, упрощая, x × y = s(sign(x), sign(y)) × |x| × |y|, где s — очевидная табличная функция, выбирающая знак по знакам аргументов, и ваш вопрос имеет простой, но скучный ответ «по определению умножения», поэтому я выбрал отталкиваться от свойств умножения и сложения, реализуемых в любой формализации, опять же.

Я думаю правильнее было бы 'Как обезьянке.' Ну а что поделать, вы же упорно уходите от вопроса который неудобен для вас.a

Потому что вы в упор не видите разницы между вашим вопросом и моим вопросом, и я знаю, что будет, если я отвечу на ваш вопрос без указания на эту разницу: вы используете мой ответ на ваш вопрос как контраргумент против моего (совсем другого) вопроса. А так как разницу вы эту в упор не признаёте, то с чего б мне отвечать?

Конечно буду, например проблема уравнений Навье Стокса отсутствие полного понимания не мешает их использовать.

Слышал звон…

Отсутствие аналитического решения в общем виде именно что мешает их использовать. Приходится либо упрощать и решать аналитически при куче дополнительных упрощений, либо решать численно, и такие решения очень быстро разваливаются (о, хаос — сколько людей сходу знает, хотя бы в каких терминах формулируется определение хаотичной системы?).

Это ваши слова, не мои. Я считаю что математика нужна но не везде, и на разных уровнях.

Да, мои слова, потому что меня эта риторика в подобных тредах уже достала.

Что ваш коллега-преподаватель, попытавшийся выпендриться тормознутым кодом для умножения матриц совершенно не в тему здесь рядом (но при этом считающий, что я беру либу для умножения матриц не потому, что я знаю про эти тонкости, а потому, что я не знаю математики), и до того перечислявший красиво звучащие слова про векторные! пространства! над полями! Галуа!, что вы, не понимающий смысл вопроса «сколько людей понимает, почему …», что все другие рассказыватели необходимости вышки/знания хорошей (использованный непосредственно вами эпитет) математики/етц для программиста что на этой странице, что во всех других тредах — это всё, если поковырять, происходит из единого желания возвыситься над теми, кто «математику не осилил» (говорящие, правда, её тоже не осилили, но ведь у нас главное — казаться, а не быть).

Это происходит абсолютно каждый раз в таких тредах. Абсолютно каждый раз всё красиво начинается за здравие про необходимость математики (или pn-переходов, или RS-триггеров) для программиста, а то он зубрила/неуч/формошлеп/ещё что, и заканчивается за упокой про «да это всё не нужно, как мне это поможет?» и в лучшем случае переобуванием в прыжке про «ну эээ я имел в виду не прям знание математики а умение применять готовые формулы».

Никак не поможет, в том-то и суть. Просто ваше «знание математики» укладывается в одну-две странички книжки «3D-графика для чайников», где-то рядом с копипаст-кодом инициализации opengl (или что там сейчас модно). Это знание доступно каждому, кто закончил школу не со справкой, просто потому, что научить перемножать матрицы (как и брать производные, как говорил наш школьный препод по матану) можно даже обезьяну.

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

> Я нигде не писал этого.

Да в этом же сообщении чуть ниже

``И что если вы не выводите доказательства то вы не знаете математику

У меня заканчиваются нематерные и не прямо оскорбительные реакции на ваше систематическое непонимание разницы между «понимать математику» и «применять математику» (или «понимать доказательство коммутативности умножения чисел» и «каждый раз доказывать коммутативность при её использовании»). Это такой троллинг глупостью с вашей стороны?

Каждый человек, умеющий ходить, применяет неслабую теорию управления неустойчивыми системами, но подавляющее большинство умеющих ходить людей не то что эту теорию не знает, а даже не знает о её существовании. Означает ли это, кстати, что для ходьбы необходимо знать эту теорию? Олимпийский бегун, не знакомый с этой теорией, формо… тьфу, ногошлёп? И он, и вы пользуетесь её результатами, они у вас прямо в мозжечке и где-то там ещё прошиты!

В этом и проблема нашего спора, ваши ожидания отличаются от того что происходит по факту

Я экстраполирую свой опыт.

(по крайней мере из моего опыта, ни на одном собеседовании не спрашивали, почему матрицы перемножаются так а не иначе, зато спрашивали кучу именно прикладных вопросов, впрочем и я не спрашиваю когда собеседую, ибо смысла от этого 0)

Какие прикладные вопросы в линейной алгебре для 3D-графики вообще можно спрашивать? Просто из интереса.

Либо у вас там «линейная алгебра» — это эвфемизм для «зазубрил, что должно лежать в какой ячейке матрицы преобразования 4×4, как их перемножать и, если хорошо выспался, как посчитать детерминант».

Наверно потому что это непосредственно связанно с работой?

Да. В моём случае это не эвфемизм.

Но вряд ли вас спрашивают, какой код будет сгенерирован при компиляции того или иного участка, если это не связанно непосредственно с работой.

Ну да, линейные операторы и их матричное представление, и особенности компиляции конкретного кода конкретным компилятором с конкретными опциями под конкретную архитектуру — это вещи одного порядка фундаментальности.

И, кстати, в некоторых задачах спрашивают. Когда собеседуюсь во всякий лоу-летенси, например, там вообще норма написать какой-нибудь код и потом обсудить, во что можно ожидать, что он скомпилируется, какие у этого будут характеристики работы, и как можно сделать лучше (и у меня в резюме написано что-то про низкоуровневое понимание исполнения кода и производительности, поэтому эти вопросы я тоже ожидаю). Или однажды на позицию функциональщика попался интервьювер, с которым мы обсудили вообще всё, от влияния параметричности на рассуждения о хаскелевской функции поиска в связном списке и возможность усилить её тип в более продвинутых языках

lookup :: Eq a => a -> [(a, b)] -> Maybe b

через рассуждение о том, почему она плоха для процессора, до особенностей работы кэш-памяти, всякой там ассоциативности, MESI, и физических ограничений на её скорость. Помню, даже почему-то отличие групповой скорости от фазовой в проводниках обсуждали (но этот разговор я мог поддержать плохо).

Тот добрый был, а я злой.

Тут ничего не утекает, но "ад коллбеков" тоже ведь существует.

То, что этим обычно называют — почти синатксическая проблема, что код съезжает сильно вправо.

Я не представляю, что надо делать, чтобы получить ад коллбеков в вызове find.

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

Это ж gnuplot!

В правильных классах типов не очень важно, что именно вызывается. Если я дёргаю length, то неважно, какой именно Foldable мне пришёл (с некоторыми условиями типа действительно полиморфного кода).

Информация

В рейтинге
1 192-й
Зарегистрирован
Активность