Я, видимо, не очень понятно написал - разумеется, 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. Понимать, откуда они берутся? Сорри, для этого надо понимать, почему они умножаются как умножаются.
Ну аналогично вашим рассуждениям, я могу утверждать что вы не пользуетесь русским языком, потому что не разбираетесь в лингвистике.
Это сново несовсем то высказывание что я имел в виду. Но и это в полне будит правдой, если руским языком я буду пользоватся не согласно правилам, но достаточна длятого, что бы вы магли меня панять.
Свою коммуникативную функцию два предложения выше выполняют? Выполняют. Можете вы сказать, встретивши их в отрыве от контекста, что их автор знает русский язык? Ну хз, я бы не сказал.
И да, лингвистика изучает язык, а сам язык — это набор коммуникативных паттернов и рецептов. Я специально выбрал «лингвистику» в прошлом комментарии, потому что аналогично вашим рассужениям я знаю лингвистику, потому что могу применять предмет изучения лингвистики для достижения своих целей.
Вы по прежнему не объяснили почему перемножение базисных векторов даёт преобразование, почему это в принципе работает?
Мне вам весь вывод расписать, что ли? В комментариях латех-форматирование до сих пор не завезли, для начала, а без этого это будет больно и уродливо для всех участников дискуссии.
Ну и для начало надо в принципе объяснить как работает перемножение.
Так, чтобы соответствующий морфизм из линейных операторов в матрицы был функториальным.
Если вы не понимаете как работает перемножение то как вы можете перемножать матрицы?
Значит, не отличаете. Я же вам прямо написал, что разница в «уметь доказывать свойства» и «доказывать свойства каждый раз при их использовании», а вы продолжаете вести себя так, будто это одно и то же.
Ну и ответьте всё же на вопрос, чем это знание мне поможет?
Я не считаю, что оно поможет. Но я не считаю, что программисту нужно знание математики и не считаю, что знание рецептов является необходимым или достаточным условием знания математики.
Собсна, именно поэтому я и задал вопрос о причинах такой формулировки умножения, как иллюстрацию моего тезиса, что знание математики не является необходимым.
Могу вывести, но считаю что это ненужно. Переубедите меня, зачем это нужно?
Мой поинт был в том, что это не аксиома, а выводимое утверждение, и что отсутствие необходимости выводить это утверждение на практике не делает его менее выводимым или более аксиоматичным.
Спасибо, что доказали мой поинт.
Ой как мы запели, нуда нуда. А по моему имеет непосредственное отношение, как вы можете использовать перемножение если не понимаете что за этим лежит.
А вы не отличаете «при каждом умножении вспоминать, как оно определяется, и почему оно коммутативно/ассоциативно» и «понимать, как вводится умножение и как доказываются его свойства»?
Ваш вопрос — первое. Мой исходный тезис — второе. Соответственно, вы либо не понимаете этой разницы (и это очень печально), либо намеренно подменяете тезис, либо просто не привыкли задумываться о таких тонкостях (к чему математика, кстати, могла бы привить привычку — если бы вы её знали).
Вы видимо сводите к абсолюту, и ровняете фразу "Нужна математика" к "Нужны знания математики во всех сферах её применения "
Попробуйте всё же дочитать комментарий, на который отвечаете, до конца.
Если для вас прикладное знание математики в определённой области и её применение
Потому что у зазубрившего перемножение матриц человека нет знания математики.
у нас видимо отличается представление о том что заложено в фразе «знание математики необходимо программисту»
Эх, а если бы вы дочитали до конца…
Для меня это использование мат аппарата
А я знаю лингвистику, если успешно пользуюсь русским языком?
А долюбится можно до чего угодно, вот вы дали например определение матрицы, но на вопрос почему именно строка на столбец перемножается не ответили.
Потому что если расписать представление базисных векторов, то строка на столбец и получится (ну или столбец на строку, опять же, если вы всё консистентно транспонировали).
Почему всегда так получается, что как поскребёшь сторонника «знание математики необходимо программисту», то там оказывается, что и не знание, и не математики, и не то чтобы необходимо? И, более того, этот сторонник сам начинает тебе доказывать, что это всё не нужно?
Я вам ответил почему, и да это понимание не нужно, также как не нужно понимание почему числа перемножаются как перемножаются.
Тогда непонятно, откуда взялся ваш ответ «примерно все».
Я считаю что в фразе «программисту нужна математика» имеется в виду владение мат аппаратом, в ключе матриц, это знать свойства матриц и операции над ними, а не историю создания и почему они умножаются как умножаются.
Что означает «знать операции»? Зазубрить алгоритмы их выполнения? Уровень даже ниже grokking algorithms. Понимать, откуда они берутся? Сорри, для этого надо понимать, почему они умножаются как умножаются.
Причём тут история, вообще непонятно. Я это знаю не из истории математики, а из проработанной «linear algebra done right».
Отлично, а теперь вопрос, чем это заученное (или скорее всего скопированное откуда-то ) определение поможет мне в работе?
Почему заученное или, тем более, скопированное?
Я не занимаюсь матричным анализом, я использую линейную алгебру.
Вы используете матричный анализ. Линейная алгебра — это как раз про линейные операторы, в ней можно работать по большому счёту вообще без матриц.
Очевидно, что если она применяется постоянно, то конечно она берётся за базу, зачем выводит её каждый раз как встречается
Я спросил не про базу, а про аксиому. Дано ли нам богом свыше минус-бэ-плюс-минус-корень-из-бэ-квадрат-минус-четыре-ацэ-на-два-а (интонационные запятые досыпьте за меня)? И я не спросил, выводите ли вы это каждый раз. Я спросил, можете ли вы это вывести, или будете говорить, что это всё не нужно?
По вашему я так понимаю, что если человек не знает почему кватернионы например работают так как работают, но при этом успешно их использует, то он не использует математику.
По-моему в этом случае человек не знает и не понимает математику, да.
Вообще во всех этих дискуссиях проблема в том, что высказывается тезис «программисту нужна математика», и он потом как дышло поворачивается куда надо по желанию. Нужна математика в смысле «пользуюсь некоторыми рецептами» (да, очевидно нужна) или «получил вышку хотя бы в прикладной математике и могу вывести эти рецепты» (нафиг не нужно, как я изначально говорил и как вы, похоже, согласны)? Математика — это околошкольное «законы де Моргана булевой алгебры и формула Байеса» (даже это не везде нужно, но добирается легко по необходимости), или околоаспирантское «алгебра Хейтинга произвольных топосов и разложение Хана вероятностной меры» (не нужно практически нигде)?
И вот, собственно, практика этих дискуссий снова показывает, что обычно люди имеют в виду понимание, откуда берутся рецепты, и достаточно высокий уровень самой математики (а кто не знает — тот кодер-макака и лох), а как начинаешь копать вглубь, так… короче, см. мой первый абзац.
Так вы не ответили на вопрос, вы когда перемножаете два числа, каждый раз думаете как это работает?
Данный вопрос не имеет отношения к моему исходному вопросу и является попыткой увести разговор в сторону ложной аналогией.
Чтобы понять, почему умножение матриц происходит именно так, надо его вывести, например, исходя из того, что матрицы - это линейные операторы: в матрице просто записаны результаты действия оператора на базисные векторы, по столбцу на вектор
Это ровно то, о чём я писал выше.
Что касается вопросов знания или понимания: надо знать достаточно математики чтобы в ней ориентироватся, чтобы понять, а какую ее часть вообще надо в вашей задаче принимать. Потому что программирование - это написание алгоритмов, и этим занимается computer science, подраздел математики.
Угу, а бухгалтерия — это работа с числами. Надо бухгалтеру знать арифметику Пеано и чем она хуже (или лучше) арифметики Пресбургера?
Под ковёр из «достаточно» у вас тут очень много заметено. На практике достаточно уровня немногим выше хорошей школы, и книги уровня grokking algorithms достаточно для базы в 99% задач в 99% работ (и за невыполнение этого 1% с вами ничего не случится — я куда больше условной девопсни/техдоков/прочего делегирую другим и нормально живу). Более того, я знаю людей, которые и эту книгу не осилили, и которые на работе успешнее, чем я, зарабатывают больше, чем я глубоко математизированным программированием, и в целом счастливее, чем я.
Вызубрить ее всю без понимания невозможно, поэтому единственный оставшийся вариант - это математику все-таки понимать.
Опять же, практика (и, в частности, этот тред) показывает, что можно именно вызубрить, и рассуждать в терминах линейных операторов для 3D-графики не нужно. Рассуждать в терминах линейных операторов оказывается не нужно даже для успешной сдачи экзамена по «линалу» на отл в топовом российском (и не только) вузе.
Лично знаю компанию, успешно занимающуюся реализацией теории абстрактной интерпретации.
Я работал в такой. LLM там применимо максимум как «сгенери парсер опций командной строки для нашего тестового бинаря». Правда, сделать то же на optparse-applicative занимает примерно столько же времени.
Тогда да, 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. Понимать, откуда они берутся? Сорри, для этого надо понимать, почему они умножаются как умножаются.
Это сново несовсем то высказывание что я имел в виду. Но и это в полне будит правдой, если руским языком я буду пользоватся не согласно правилам, но достаточна длятого, что бы вы магли меня панять.
Свою коммуникативную функцию два предложения выше выполняют? Выполняют. Можете вы сказать, встретивши их в отрыве от контекста, что их автор знает русский язык? Ну хз, я бы не сказал.
И да, лингвистика изучает язык, а сам язык — это набор коммуникативных паттернов и рецептов. Я специально выбрал «лингвистику» в прошлом комментарии, потому что аналогично вашим рассужениям я знаю лингвистику, потому что могу применять предмет изучения лингвистики для достижения своих целей.
Мне вам весь вывод расписать, что ли? В комментариях латех-форматирование до сих пор не завезли, для начала, а без этого это будет больно и уродливо для всех участников дискуссии.
Так, чтобы соответствующий морфизм из линейных операторов в матрицы был функториальным.
Как обезьянка.
Значит, не отличаете. Я же вам прямо написал, что разница в «уметь доказывать свойства» и «доказывать свойства каждый раз при их использовании», а вы продолжаете вести себя так, будто это одно и то же.
По тем пунктам, которые вы добавили в правке:
Я не считаю, что оно поможет. Но я не считаю, что программисту нужно знание математики и не считаю, что знание рецептов является необходимым или достаточным условием знания математики.
Собсна, именно поэтому я и задал вопрос о причинах такой формулировки умножения, как иллюстрацию моего тезиса, что знание математики не является необходимым.
Мой поинт был в том, что это не аксиома, а выводимое утверждение, и что отсутствие необходимости выводить это утверждение на практике не делает его менее выводимым или более аксиоматичным.
Спасибо, что доказали мой поинт.
А вы не отличаете «при каждом умножении вспоминать, как оно определяется, и почему оно коммутативно/ассоциативно» и «понимать, как вводится умножение и как доказываются его свойства»?
Ваш вопрос — первое. Мой исходный тезис — второе. Соответственно, вы либо не понимаете этой разницы (и это очень печально), либо намеренно подменяете тезис, либо просто не привыкли задумываться о таких тонкостях (к чему математика, кстати, могла бы привить привычку — если бы вы её знали).
Попробуйте всё же дочитать комментарий, на который отвечаете, до конца.
Потому что у зазубрившего перемножение матриц человека нет знания математики.
Эх, а если бы вы дочитали до конца…
А я знаю лингвистику, если успешно пользуюсь русским языком?
Потому что если расписать представление базисных векторов, то строка на столбец и получится (ну или столбец на строку, опять же, если вы всё консистентно транспонировали).
Почему всегда так получается, что как поскребёшь сторонника «знание математики необходимо программисту», то там оказывается, что и не знание, и не математики, и не то чтобы необходимо? И, более того, этот сторонник сам начинает тебе доказывать, что это всё не нужно?
Тогда непонятно, откуда взялся ваш ответ «примерно все».
Что означает «знать операции»? Зазубрить алгоритмы их выполнения? Уровень даже ниже grokking algorithms. Понимать, откуда они берутся? Сорри, для этого надо понимать, почему они умножаются как умножаются.
Причём тут история, вообще непонятно. Я это знаю не из истории математики, а из проработанной «linear algebra done right».
Почему заученное или, тем более, скопированное?
Вы используете матричный анализ. Линейная алгебра — это как раз про линейные операторы, в ней можно работать по большому счёту вообще без матриц.
Я спросил не про базу, а про аксиому. Дано ли нам богом свыше минус-бэ-плюс-минус-корень-из-бэ-квадрат-минус-четыре-ацэ-на-два-а (интонационные запятые досыпьте за меня)? И я не спросил, выводите ли вы это каждый раз. Я спросил, можете ли вы это вывести, или будете говорить, что это всё не нужно?
По-моему в этом случае человек не знает и не понимает математику, да.
Вообще во всех этих дискуссиях проблема в том, что высказывается тезис «программисту нужна математика», и он потом как дышло поворачивается куда надо по желанию. Нужна математика в смысле «пользуюсь некоторыми рецептами» (да, очевидно нужна) или «получил вышку хотя бы в прикладной математике и могу вывести эти рецепты» (нафиг не нужно, как я изначально говорил и как вы, похоже, согласны)? Математика — это околошкольное «законы де Моргана булевой алгебры и формула Байеса» (даже это не везде нужно, но добирается легко по необходимости), или околоаспирантское «алгебра Хейтинга произвольных топосов и разложение Хана вероятностной меры» (не нужно практически нигде)?
И вот, собственно, практика этих дискуссий снова показывает, что обычно люди имеют в виду понимание, откуда берутся рецепты, и достаточно высокий уровень самой математики (а кто не знает — тот кодер-макака и лох), а как начинаешь копать вглубь, так… короче, см. мой первый абзац.
Данный вопрос не имеет отношения к моему исходному вопросу и является попыткой увести разговор в сторону ложной аналогией.
Это ровно то, о чём я писал выше.
Угу, а бухгалтерия — это работа с числами. Надо бухгалтеру знать арифметику Пеано и чем она хуже (или лучше) арифметики Пресбургера?
Под ковёр из «достаточно» у вас тут очень много заметено. На практике достаточно уровня немногим выше хорошей школы, и книги уровня grokking algorithms достаточно для базы в 99% задач в 99% работ (и за невыполнение этого 1% с вами ничего не случится — я куда больше условной девопсни/техдоков/прочего делегирую другим и нормально живу). Более того, я знаю людей, которые и эту книгу не осилили, и которые на работе успешнее, чем я, зарабатывают больше, чем я глубоко математизированным программированием, и в целом счастливее, чем я.
Опять же, практика (и, в частности, этот тред) показывает, что можно именно вызубрить, и рассуждать в терминах линейных операторов для 3D-графики не нужно. Рассуждать в терминах линейных операторов оказывается не нужно даже для успешной сдачи экзамена по «линалу» на отл в топовом российском (и не только) вузе.
Я работал в такой. LLM там применимо максимум как «сгенери парсер опций командной строки для нашего тестового бинаря». Правда, сделать то же на optparse-applicative занимает примерно столько же времени.