Я хочу опровергнуть квантор всеобщности частным случаем (весьма распространённым, к слову), когда выражение под квантором (улетающие байндинги из локального скоупа ведут к нарушению инкапсуляции) не выполняется.
Но можно и проще (для вас): покажите ФП-пример (раз мы тут ФП обсуждаем), где это ломает инкапсуляцию.
Например опшионал может быть нужен только для тестов, а не в продакшене, тогда нет нужды ни в каких проверках
Почему? Кто мне это в типах гарантирует? Это ведь сломается при малейшем рефакторинге или изменении требований.
Вообще какое-то странное требование, чтобы в тестах нужно было, а так — нет. Можно какой-нибудь пример, чтобы я лучше понимал контекст?
то доступ к значению опшионала кинет исключение или терминирует программу кому как нравится.
А если вы пишете на плюсах (мои искренние соболезнования)? Как там, что у нас operator* и operator-> говорят про пустой опшонал? А, во:
The behavior is undefined if *this does not contain a value.
Всё как всегда в плюсах.
Если же опшионал на самом деле нужен в продакшнене то ваша замена с конструктором не эквивалентна т.к. проверку на пусто кто то где то всё ж таки должен делать.
Я и говорю, что эта замена не эквивалентна, а лучше: проверку нужно делать один раз и в условном main(), а не размазывать её по всей кодовой базе с неясной семантикой на пару.
С ней основная проблема в том, что целые числа там — это некоторый класс эквивалентности, а не напрямую единственным образом строящийся терм, а работать с классами эквивалентности в мейнстримных и устоявшихся пруверах исключительно больно, если кубы не гонять, но cubical type theory мы пока не очень понимаем. Возьмите любой результат из гугла по запросу «setoid hell» на ваш вкус.
Другой вопрос — причём тут вообще пруверы, но это уже моя профдеформация. На бумажке при разговоре с другим человеком с группой Гротендика всё норм.
Я, видимо, не очень понятно написал - разумеется, DSL.
Тогда да, ADD Магвайра, и формально доказывать выписанные для комбинаторов законы (и требовать в типах комбинаторов нужный контекст, если оно вылезает из законов).
Проблема в том, что я не очень понимаю, как из этой идеи выжать всё. В смысле, как понять, что можно ещё куда-то двинуться, или же наоборот, там всё украдено до нас.
Попытаться опубликовать статью и посмотреть на реакцию ревьюверов :]
Это означает какие операции к ним применимы, и их свойства.
Окей, принято. Только это зубрёж уровня зубрежа дат в школьной истории или стихотворений в школьной литературе. Собственно, школьный уровень, да, как я и писал изначально.
Ну нет, так не пойдёт. Если следовать вашей логике, то вы не используете русский.
Я на всякий случай напомню о том, что русский язык — это не наука, а набор соглашений, а лингвистика — ну так, наука немножко (на самом деле вообще настолько наука, насколько гуманитарная вещь может быть наукой). Поэтому у слова «использовать» во фразах «использовать русский язык» и «использовать лингвистику/математику» несколько разная семантика (ну, как у «побег», который сериал из нулевых, и «побег», который у растений).
Поэтому да, в предыдущем абзаце я использую русский язык, но определять «использую $science» или «знаю $science» так, чтобы предыдущий абзац был заодно примером использования лингвистики, очень странно (но если хочется считать себя лингвистом, то можно, конечно, и так определить, кто ж запретит).
И аналогично говорить, что я знаю математику русский язык, если я пишу неправильно, но носитель русского языка всё равно может меня понять (то есть, если я достигаю цели использования языка) — это тоже очень нетипичное использование термина «знаю».
Не знаю, вы сначала диплом лингвиста покажите, а потом я смогу сказать используете вы русский или нет, а без этого никак.
Вы всё ещё не отличаете «использовать результаты» от «знать, откуда они берутся»?
А я не знаю лингвистику, значит я не пишу на русском и не знаю его, интересно как же вы понимаете меня?
Начинаю подозревать, что я ошибался, и что математику надо знать не программистам, а вообще всем, чтобы они не делали таких логических ошибок, на которые я устал указывать (потому что мои указания вы систематически игнорируете).
Естественно, желательно с доказательством и анализом, а то как я пойму математику вы мне объясняете, или же зазубренными аксиомами кидаетесь уровня grokking algorithms.
А кто мне мешает скопипастить из учебника?
Это ничего не объясняет
Зависит от языка, которым вы пользуетесь. Если человек достаточно интернализировал понятие морфизма и функториальности, то ему это скажет более чем нужно. Если же нет — ну, тут каждый из этих терминов раскрывается в несколько предложений.
как говорил Фейнман "Если вы не можете что-то объяснить ребенку, то вы этого не понимаете сами"
Ну объясните ребёнку квантмех или ОТО, пожалуйста, а я на это посмотрю.
Вообще зря люди в вузах учатся, дипломы защищают, кандидатские потом всякие. Можно же просто объяснить ребёнку, и ребёнок поймёт!
попробуйте объяснить мне почему -3 * -3 == 9 а не -9 это же база, но так как вы говорите что без выведений и доказательств это не математика, то докажите и выведите почему -3 * -3 == 9.
Зависит от вашей формализации целых чисел (группа Гротендика, прямое построение как индуктивный тип поверх натуральных с двумя конструкторами nonneg : ℕ → ℤ и neg : ℕ → ℤ, или что-то ещё по вашему вкусу). Впрочем, во всех этих формализациях умножение дистрибутивно относительно сложения и коммутативно (что доказывается зависимо от формализации), а сложение формирует группу, где -x — (единственный, как и в любой группе) обратный к x, поэтому:
∀x, y. xy + (-x)y =[ дистрибутивность] (x + -x)y =[ -x обратный к x] 0y =[ определение умножения ] 0 ⇒ (-x)y =[единственность обратного] -(xy)
∀x, y. (-x)(-y) =[ п. 1 ] -(x(-y)) =[ коммутативность ] -((-y)x) =[ п. 1 ] -(-(yx)) =[ групповые свойства обратных ] yx =[ коммутативность ] xy
Инстанциируем для 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.
В результате, смотришь на код, который вызывает какую-то функцию, но вот без вывода типов хрен поймёшь, какую же именно функцию он вызывает, а из имени совершенно непонятно, что же именно она делает.
В правильных классах типов не очень важно, что именно вызывается. Если я дёргаю length, то неважно, какой именно Foldable мне пришёл (с некоторыми условиями типа действительно полиморфного кода).
К примеру, я хочу написать CAD для моделирования электрических схем какого-то сорта, но я хочу сделать 2 уровня моделирования, первый - грубый, чтобы отсекать заведомо негодные схемы до отправки на расчёт. Это - типичная задача для типов.
Если это не DSL для описания схем, то типы тут не очень помогут.
То есть, ты, конечно, можешь вычислительное ядро своего CAD'а обложить типами, чтобы оно не принимало некорректные задачи, но это всё равно потребует кода по «валидации» пользовательских схем (пусть даже мы валидируем в строго типизированные значения), и никто не помешает описать некорректные пользовательские схемы.
Если же ты хочешь делать DSL, то настоятельно рекомендую почитать algebra-driven design Сэнди Магвайра. Это не совсем про типы, но достаточно близко.
Насчёт непосредственно использования сильных типов в подобных задачах не для академиков я ничего сходу вспомнить не могу. Книжки уровня software foundations — перебор и слишком базовые (это по факту учебник по coq'у, на твой вопрос оно не факт что ответит), условные научные статьи с условного ESOP, как люди там типами проверяют ширину квантовых схем, например — это, ну, научные статьи, а не для народного хозяйства, и люди там придумывают свою очередную систему типов, в хаскеле/идрисе ты такое не запрогаешь (хотя там что-то было про квантовую либу для идриса — могу найти, если интересно).
Я выбираю сразу написать по моему главному правилу: невалидное состояние системы непредставимо в системе типов.
Только вы им не пользуетесь.
Когда у вас есть static optional<Singleton> instance() и есть какой-то class SingletonUser , который без синглтона жить не может, но конструктор которого не требует синглтона, то у вас в ваших типах представимо состояние «синглтон не создался, а SingletonUser создался», что ведёт к боли, страданию и проверкам внутри каждого такого SingletonUser , действительно ли синглтон создался.
Когда у вас нет никакого static optional<Singleton> instance(), а есть конструктор
class SingletonUser
{
public:
SingletonUser(Singleton& instance);
};
то у вас состояние «синлтона нет, а клиент синглтона есть» непредставимо, как вы и хотели.
И вам даже нужно меньше проверок, потому что вы эти проверки делаете один раз и условно в main() вместо того, чтобы их делать каждый раз в каждом клиенте синглтона.
Во-первых, эта функция заточена на инты и массивы. Максимум может быть не только среди интов, не только в массивах (но и в мапах, например, или даже в optional'ах), да и хотелось бы уметь передавать произвольный предикат, чтобы хотя бы немножко почувствовать эту самую Ф при П. Ну, что-то вроде такого:
maximumBy :: Foldable t => (a -> a -> Ordering) -> t a -> Maybe a
Во-вторых, тип вашей функции показывает, что она скорее всего не будет работать для пустых массивов. И правда: array[0] ой сегфолт (в лучшем случае).
я тоже так думал потому что ситуация у меня была очень похожая, я интроверт и вообще избегал всяких тусовок и массовых мероприятий, пока не познакомился на ДР моего друга в ресторане (который ему тогда принадлежал) со своей будущей женой которая там официанткой работала в тот момент.
При этом вы куда-то сходили, где вы были достаточно привлекательно выглядящим (я уверен, что друг уборщика пользовался бы куда меньшим априорным интересом, чем друг владельца ресторана), и как-то завязали разговор (либо сами инициировали, либо ответили на инициацию — я бы во втором случае подумал, что от меня просто чаевых побольше хотят).
Если люди что-то делают для того, чтобы получать то, что они хотят, то у них больше шансов, чем если они будут просто ждать. Люди, работающие над своей привлекательностью для девушек, будут пользоваться большим спросом и в среднем придут к большему успеху, чем не работающие. Работать, конечно, надо в правильном направлении — я когда-то думал, что девочки любят отличников, но глубокое задротство почему-то к успеху не привело.
И это работает не только с девушками, на самом деле. Меня задолбала одышка от нескольких лестничных пролётов — я пошёл в тренажерку на кардио и избавился от неё (и это сильно более верный путь, чем ждать, пока она сама пройдёт). Меня задолбало, что у меня болит спина — я пошёл в тренажерку на силовые, и у меня больше не болит спина. Меня задолбало, что у меня хреновый режим сна — я пересмотрел потребление кофеина и сломал некоторые традиции, в которых он участвует.
которой передаётся предикат и список, и возвращается первый элемент, удовлетворяющий этому предикату. Я передаю туда лямбду, которая из текущего скоупа захватывает, например, хэшмапу и проверяет вхождение в неё. Где здесь что куда утекает и ломает инкапсуляцию?
Да нет, это вы утверждаете что умение применять математику, и умение выводить доказательства это одно и тоже.
Я нигде не писал этого.
А вот соседний оратор (что забавно, заплюсованный, в отличие от меня) прямо писал, что математику надо понимать для того, чтобы ей пользоваться на практике.
Почему такая разная реакция? Потому, что из его комментария не следует напрямую, что все эти разговоры про знание математики — клоунада и попытка возвыситься за счёт тупых макак, которые просто говнокодят и математику не знают, а из моего комментария это следует довольно прямо.
И что если вы не выводите доказательства то вы не знаете математику.
Да, всё так. Будете спорить?
Если на вакансии вы увидите требование "знание линейной алгебры" у вас будут спрашивать почему перемножение матрицы это строка на столбец, или всё же вопросы будут связаны с прикладной частью?
Я ожидаю, что будут спрашивать.
Собственно, я подаюсь на вакансии, где требуют знание теории типов, и ожидаю, что со мной поговорят про strong normalization у system f, например, и прочие подобные вещи. И, вы не поверите, говорят!
Ну то есть, если человек знает все свойства матриц и операций над ними, но не может сходу вывести перемножение
Повторю вопрос из недочитанного вами комментария:
Что означает «знать операции»? Зазубрить алгоритмы их выполнения? Уровень даже ниже grokking algorithms. Понимать, откуда они берутся? Сорри, для этого надо понимать, почему они умножаются как умножаются.
Ну аналогично вашим рассуждениям, я могу утверждать что вы не пользуетесь русским языком, потому что не разбираетесь в лингвистике.
Это сново несовсем то высказывание что я имел в виду. Но и это в полне будит правдой, если руским языком я буду пользоватся не согласно правилам, но достаточна длятого, что бы вы магли меня панять.
Свою коммуникативную функцию два предложения выше выполняют? Выполняют. Можете вы сказать, встретивши их в отрыве от контекста, что их автор знает русский язык? Ну хз, я бы не сказал.
И да, лингвистика изучает язык, а сам язык — это набор коммуникативных паттернов и рецептов. Я специально выбрал «лингвистику» в прошлом комментарии, потому что аналогично вашим рассужениям я знаю лингвистику, потому что могу применять предмет изучения лингвистики для достижения своих целей.
Вы по прежнему не объяснили почему перемножение базисных векторов даёт преобразование, почему это в принципе работает?
Мне вам весь вывод расписать, что ли? В комментариях латех-форматирование до сих пор не завезли, для начала, а без этого это будет больно и уродливо для всех участников дискуссии.
Ну и для начало надо в принципе объяснить как работает перемножение.
Так, чтобы соответствующий морфизм из линейных операторов в матрицы был функториальным.
Если вы не понимаете как работает перемножение то как вы можете перемножать матрицы?
Значит, не отличаете. Я же вам прямо написал, что разница в «уметь доказывать свойства» и «доказывать свойства каждый раз при их использовании», а вы продолжаете вести себя так, будто это одно и то же.
Инкапсуляция — это сокрытие иррелевантных деталей реализации. ООП-модификатор
private— это просто частный случай.Я хочу опровергнуть квантор всеобщности частным случаем (весьма распространённым, к слову), когда выражение под квантором (улетающие байндинги из локального скоупа ведут к нарушению инкапсуляции) не выполняется.
Но можно и проще (для вас): покажите ФП-пример (раз мы тут ФП обсуждаем), где это ломает инкапсуляцию.
Что он вырастит? Геморрой от ночей дебага или шишку на лбу от бития об стол, когда дебаг совсем не удаётся?
Почему? Кто мне это в типах гарантирует? Это ведь сломается при малейшем рефакторинге или изменении требований.
Вообще какое-то странное требование, чтобы в тестах нужно было, а так — нет. Можно какой-нибудь пример, чтобы я лучше понимал контекст?
А если вы пишете на плюсах (мои искренние соболезнования)? Как там, что у нас
operator*иoperator->говорят про пустой опшонал? А, во:Всё как всегда в плюсах.
Я и говорю, что эта замена не эквивалентна, а лучше: проверку нужно делать один раз и в условном
main(), а не размазывать её по всей кодовой базе с неясной семантикой на пару.О, группа Гротендика.
С ней основная проблема в том, что целые числа там — это некоторый класс эквивалентности, а не напрямую единственным образом строящийся терм, а работать с классами эквивалентности в мейнстримных и устоявшихся пруверах исключительно больно, если кубы не гонять, но cubical type theory мы пока не очень понимаем. Возьмите любой результат из гугла по запросу «setoid hell» на ваш вкус.
Другой вопрос — причём тут вообще пруверы, но это уже моя
профдеформация. На бумажке при разговоре с другим человеком с группой Гротендика всё норм.Тогда да, ADD Магвайра, и формально доказывать выписанные для комбинаторов законы (и требовать в типах комбинаторов нужный контекст, если оно вылезает из законов).
Попытаться опубликовать статью и посмотреть на реакцию ревьюверов :]
ХЗ, но я всё равно нашёл: https://arxiv.org/pdf/2111.10867
Думаю, что оно может оказаться релевантнее, чем кажется сходу.
Окей, принято. Только это зубрёж уровня зубрежа дат в школьной истории или стихотворений в школьной литературе. Собственно, школьный уровень, да, как я и писал изначально.
Я на всякий случай напомню о том, что русский язык — это не наука, а набор соглашений, а лингвистика — ну так, наука немножко (на самом деле вообще настолько наука, насколько гуманитарная вещь может быть наукой). Поэтому у слова «использовать» во фразах «использовать русский язык» и «использовать лингвистику/математику» несколько разная семантика (ну, как у «побег», который сериал из нулевых, и «побег», который у растений).
Поэтому да, в предыдущем абзаце я использую русский язык, но определять «использую $science» или «знаю $science» так, чтобы предыдущий абзац был заодно примером использования лингвистики, очень странно (но если хочется считать себя лингвистом, то можно, конечно, и так определить, кто ж запретит).
И аналогично говорить, что я знаю
математикурусский язык, если я пишу неправильно, но носитель русского языка всё равно может меня понять (то есть, если я достигаю цели использования языка) — это тоже очень нетипичное использование термина «знаю».Вы всё ещё не отличаете «использовать результаты» от «знать, откуда они берутся»?
Начинаю подозревать, что я ошибался, и что математику надо знать не программистам, а вообще всем, чтобы они не делали таких логических ошибок, на которые я устал указывать (потому что мои указания вы систематически игнорируете).
А кто мне мешает скопипастить из учебника?
Зависит от языка, которым вы пользуетесь. Если человек достаточно интернализировал понятие морфизма и функториальности, то ему это скажет более чем нужно. Если же нет — ну, тут каждый из этих терминов раскрывается в несколько предложений.
Ну объясните ребёнку квантмех или ОТО, пожалуйста, а я на это посмотрю.
Вообще зря люди в вузах учатся, дипломы защищают, кандидатские потом всякие. Можно же просто объяснить ребёнку, и ребёнок поймёт!
Зависит от вашей формализации целых чисел (группа Гротендика, прямое построение как индуктивный тип поверх натуральных с двумя конструкторами
nonneg : ℕ → ℤиneg : ℕ → ℤ, или что-то ещё по вашему вкусу). Впрочем, во всех этих формализациях умножение дистрибутивно относительно сложения и коммутативно (что доказывается зависимо от формализации), а сложение формирует группу, где -x — (единственный, как и в любой группе) обратный к x, поэтому:∀x, y. xy + (-x)y =[ дистрибутивность] (x + -x)y =[ -x обратный к x] 0y =[ определение умножения ] 0
⇒
(-x)y =[единственность обратного] -(xy)
∀x, y. (-x)(-y) =[ п. 1 ] -(x(-y)) =[ коммутативность ] -((-y)x) =[ п. 1 ] -(-(yx)) =[ групповые свойства обратных ] yx =[ коммутативность ] xy
Инстанциируем для x = y = -3: -3 × -3 = 3 × 3 = 9.
Я здесь пропустил пару шагов, понятных человеку, но непонятных агде или коку, но если вы найдёте, к чему придраться, то вы заодно понимаете, что я опустил.
Правда, в некоторых формализациях (например, стандартной агдовской) умножение определяется как, упрощая, x × y = s(sign(x), sign(y)) × |x| × |y|, где s — очевидная табличная функция, выбирающая знак по знакам аргументов, и ваш вопрос имеет простой, но скучный ответ «по определению умножения», поэтому я выбрал отталкиваться от свойств умножения и сложения, реализуемых в любой формализации, опять же.
Потому что вы в упор не видите разницы между вашим вопросом и моим вопросом, и я знаю, что будет, если я отвечу на ваш вопрос без указания на эту разницу: вы используете мой ответ на ваш вопрос как контраргумент против моего (совсем другого) вопроса. А так как разницу вы эту в упор не признаёте, то с чего б мне отвечать?
Слышал звон…
Отсутствие аналитического решения в общем виде именно что мешает их использовать. Приходится либо упрощать и решать аналитически при куче дополнительных упрощений, либо решать численно, и такие решения очень быстро разваливаются (о, хаос — сколько людей сходу знает, хотя бы в каких терминах формулируется определение хаотичной системы?).
Да, мои слова, потому что меня эта риторика в подобных тредах уже достала.
Что ваш коллега-преподаватель, попытавшийся выпендриться тормознутым кодом для умножения матриц совершенно не в тему здесь рядом (но при этом считающий, что я беру либу для умножения матриц не потому, что я знаю про эти тонкости, а потому, что я не знаю математики), и до того перечислявший красиво звучащие слова про векторные! пространства! над полями! Галуа!, что вы, не понимающий смысл вопроса «сколько людей понимает, почему …», что все другие рассказыватели необходимости вышки/знания хорошей (использованный непосредственно вами эпитет) математики/етц для программиста что на этой странице, что во всех других тредах — это всё, если поковырять, происходит из единого желания возвыситься над теми, кто «математику не осилил» (говорящие, правда, её тоже не осилили, но ведь у нас главное — казаться, а не быть).
Это происходит абсолютно каждый раз в таких тредах. Абсолютно каждый раз всё красиво начинается за здравие про необходимость математики (или pn-переходов, или RS-триггеров) для программиста, а то он зубрила/неуч/формошлеп/ещё что, и заканчивается за упокой про «да это всё не нужно, как мне это поможет?» и в лучшем случае переобуванием в прыжке про «ну эээ я имел в виду не прям знание математики а умение применять готовые формулы».
Никак не поможет, в том-то и суть. Просто ваше «знание математики» укладывается в одну-две странички книжки «3D-графика для чайников», где-то рядом с копипаст-кодом инициализации opengl (или что там сейчас модно). Это знание доступно каждому, кто закончил школу не со справкой, просто потому, что научить перемножать матрицы (как и брать производные, как говорил наш школьный препод по матану) можно даже обезьяну.
Впрочем, это всё меня достало во многом потому, что я повёлся на все эти рассказы про нужность математики и потратил на неё довольно много времени, а к счастью это меня не привело, только наоборот.
У меня заканчиваются нематерные и не прямо оскорбительные реакции на ваше систематическое непонимание разницы между «понимать математику» и «применять математику» (или «понимать доказательство коммутативности умножения чисел» и «каждый раз доказывать коммутативность при её использовании»). Это такой троллинг глупостью с вашей стороны?
Каждый человек, умеющий ходить, применяет неслабую теорию управления неустойчивыми системами, но подавляющее большинство умеющих ходить людей не то что эту теорию не знает, а даже не знает о её существовании. Означает ли это, кстати, что для ходьбы необходимо знать эту теорию? Олимпийский бегун, не знакомый с этой теорией, формо… тьфу, ногошлёп? И он, и вы пользуетесь её результатами, они у вас прямо в мозжечке и где-то там ещё прошиты!
Я экстраполирую свой опыт.
Какие прикладные вопросы в линейной алгебре для 3D-графики вообще можно спрашивать? Просто из интереса.
Либо у вас там «линейная алгебра» — это эвфемизм для «зазубрил, что должно лежать в какой ячейке матрицы преобразования 4×4, как их перемножать и, если хорошо выспался, как посчитать детерминант».
Да. В моём случае это не эвфемизм.
Ну да, линейные операторы и их матричное представление, и особенности компиляции конкретного кода конкретным компилятором с конкретными опциями под конкретную архитектуру — это вещи одного порядка фундаментальности.
И, кстати, в некоторых задачах спрашивают. Когда собеседуюсь во всякий лоу-летенси, например, там вообще норма написать какой-нибудь код и потом обсудить, во что можно ожидать, что он скомпилируется, какие у этого будут характеристики работы, и как можно сделать лучше (и у меня в резюме написано что-то про низкоуровневое понимание исполнения кода и производительности, поэтому эти вопросы я тоже ожидаю). Или однажды на позицию функциональщика попался интервьювер, с которым мы обсудили вообще всё, от влияния параметричности на рассуждения о хаскелевской функции поиска в связном списке и возможность усилить её тип в более продвинутых языках
через рассуждение о том, почему она плоха для процессора, до особенностей работы кэш-памяти, всякой там ассоциативности, MESI, и физических ограничений на её скорость. Помню, даже почему-то отличие групповой скорости от фазовой в проводниках обсуждали (но этот разговор я мог поддержать плохо).
Тот добрый был, а я злой.
То, что этим обычно называют — почти синатксическая проблема, что код съезжает сильно вправо.
Я не представляю, что надо делать, чтобы получить ад коллбеков в вызове
find.Это ж gnuplot!
В правильных классах типов не очень важно, что именно вызывается. Если я дёргаю
length, то неважно, какой именноFoldableмне пришёл (с некоторыми условиями типа действительно полиморфного кода).Если это не DSL для описания схем, то типы тут не очень помогут.
То есть, ты, конечно, можешь вычислительное ядро своего CAD'а обложить типами, чтобы оно не принимало некорректные задачи, но это всё равно потребует кода по «валидации» пользовательских схем (пусть даже мы валидируем в строго типизированные значения), и никто не помешает описать некорректные пользовательские схемы.
Если же ты хочешь делать DSL, то настоятельно рекомендую почитать algebra-driven design Сэнди Магвайра. Это не совсем про типы, но достаточно близко.
Насчёт непосредственно использования сильных типов в подобных задачах не для академиков я ничего сходу вспомнить не могу. Книжки уровня software foundations — перебор и слишком базовые (это по факту учебник по coq'у, на твой вопрос оно не факт что ответит), условные научные статьи с условного ESOP, как люди там типами проверяют ширину квантовых схем, например — это, ну, научные статьи, а не для народного хозяйства, и люди там придумывают свою очередную систему типов, в хаскеле/идрисе ты такое не запрогаешь (хотя там что-то было про квантовую либу для идриса — могу найти, если интересно).
Это что-то на уровне нацистской эстетики пресс-конференции Байдена?
Скрытый текст
Только вы им не пользуетесь.
Когда у вас есть
static optional<Singleton> instance()и есть какой-тоclass SingletonUser, который без синглтона жить не может, но конструктор которого не требует синглтона, то у вас в ваших типах представимо состояние «синглтон не создался, аSingletonUserсоздался», что ведёт к боли, страданию и проверкам внутри каждого такогоSingletonUser, действительно ли синглтон создался.Когда у вас нет никакого
static optional<Singleton> instance(), а есть конструкторто у вас состояние «синлтона нет, а клиент синглтона есть» непредставимо, как вы и хотели.
И вам даже нужно меньше проверок, потому что вы эти проверки делаете один раз и условно в
main()вместо того, чтобы их делать каждый раз в каждом клиенте синглтона.Во всём.
Во-первых, эта функция заточена на инты и массивы. Максимум может быть не только среди интов, не только в массивах (но и в мапах, например, или даже в optional'ах), да и хотелось бы уметь передавать произвольный предикат, чтобы хотя бы немножко почувствовать эту самую Ф при П. Ну, что-то вроде такого:
Во-вторых, тип вашей функции показывает, что она скорее всего не будет работать для пустых массивов. И правда:
array[0]ой сегфолт (в лучшем случае).При этом вы куда-то сходили, где вы были достаточно привлекательно выглядящим (я уверен, что друг уборщика пользовался бы куда меньшим априорным интересом, чем друг владельца ресторана), и как-то завязали разговор (либо сами инициировали, либо ответили на инициацию — я бы во втором случае подумал, что от меня просто чаевых побольше хотят).
Если люди что-то делают для того, чтобы получать то, что они хотят, то у них больше шансов, чем если они будут просто ждать. Люди, работающие над своей привлекательностью для девушек, будут пользоваться большим спросом и в среднем придут к большему успеху, чем не работающие. Работать, конечно, надо в правильном направлении — я когда-то думал, что девочки любят отличников, но глубокое задротство почему-то к успеху не привело.
И это работает не только с девушками, на самом деле. Меня задолбала одышка от нескольких лестничных пролётов — я пошёл в тренажерку на кардио и избавился от неё (и это сильно более верный путь, чем ждать, пока она сама пройдёт). Меня задолбало, что у меня болит спина — я пошёл в тренажерку на силовые, и у меня больше не болит спина. Меня задолбало, что у меня хреновый режим сна — я пересмотрел потребление кофеина и сломал некоторые традиции, в которых он участвует.
У меня есть функция
которой передаётся предикат и список, и возвращается первый элемент, удовлетворяющий этому предикату. Я передаю туда лямбду, которая из текущего скоупа захватывает, например, хэшмапу и проверяет вхождение в неё. Где здесь что куда утекает и ломает инкапсуляцию?
Угу, такой мощный, что spaceship пришлось вводить на уровне языка, а не библиотекой для метапрограммирования.
Я нигде не писал этого.
А вот соседний оратор (что забавно, заплюсованный, в отличие от меня) прямо писал, что математику надо понимать для того, чтобы ей пользоваться на практике.
Почему такая разная реакция? Потому, что из его комментария не следует напрямую, что все эти разговоры про знание математики — клоунада и попытка возвыситься за счёт тупых макак, которые просто говнокодят и математику не знают, а из моего комментария это следует довольно прямо.
Да, всё так. Будете спорить?
Я ожидаю, что будут спрашивать.
Собственно, я подаюсь на вакансии, где требуют знание теории типов, и ожидаю, что со мной поговорят про strong normalization у system f, например, и прочие подобные вещи. И, вы не поверите, говорят!
Повторю вопрос из недочитанного вами комментария:
Что означает «знать операции»? Зазубрить алгоритмы их выполнения? Уровень даже ниже grokking algorithms. Понимать, откуда они берутся? Сорри, для этого надо понимать, почему они умножаются как умножаются.
Это сново несовсем то высказывание что я имел в виду. Но и это в полне будит правдой, если руским языком я буду пользоватся не согласно правилам, но достаточна длятого, что бы вы магли меня панять.
Свою коммуникативную функцию два предложения выше выполняют? Выполняют. Можете вы сказать, встретивши их в отрыве от контекста, что их автор знает русский язык? Ну хз, я бы не сказал.
И да, лингвистика изучает язык, а сам язык — это набор коммуникативных паттернов и рецептов. Я специально выбрал «лингвистику» в прошлом комментарии, потому что аналогично вашим рассужениям я знаю лингвистику, потому что могу применять предмет изучения лингвистики для достижения своих целей.
Мне вам весь вывод расписать, что ли? В комментариях латех-форматирование до сих пор не завезли, для начала, а без этого это будет больно и уродливо для всех участников дискуссии.
Так, чтобы соответствующий морфизм из линейных операторов в матрицы был функториальным.
Как обезьянка.
Значит, не отличаете. Я же вам прямо написал, что разница в «уметь доказывать свойства» и «доказывать свойства каждый раз при их использовании», а вы продолжаете вести себя так, будто это одно и то же.