Я, конечно, предпочитаю избегать double negation elimination, потому что использование этой аксиомы работает только в булевых топосах (в отличие от proof of negation, часто путаемого с proof by contradiction), но что-то мне подсказывает, что вопросы у тебя не к этому.
Понятно, что есть некоторая грань допустимого, например, точно нельзя вырывать сердце у геймдизайнера за провальную игру.
А вот этот контраргумент неконсистентен с темой разговора :]
Нет устоявшихся студий, где вырывают сердца у геймдизайнеров. Поэтому к структуре тезиса «если X делалось раньше как один из компонентов результата Y, и Y вроде норм, то X зачем-то нужно» это не относится.
Процитированная мною часть комментария перешла на личности первой, в словах «_вы_ ведётесь», «_вы_ льёте воду», и так далее. Это намекает, что обсуждать собеседника напрямую допустимо для моего собеседника.
Ну и сложно сказать, что слова вроде «if you can't follow that rule» (где «rule» — это «I asked for early pull requests», кстати, что смешно) не являются переходом на личности в данном контексте. Это как если бы я написал первый абзац в виде «Я отвечал на конкретную отсылку к личности собеседника, и если вы неспособны понять это из текста моего комментария, то хотя бы [...]».
А, ну и да, это ж не единственный комментарий Торвальдса. Он много чего ещё говорил в духе мастурбирующих обезьянок, например.
Во второй цитате я точно так же указываю на то что:
Нет, во второй цитате вы пишете «а то сегодня ⇒ а завтра может».
Если вам не нравится некодифицированная мораль, то вы можете просто требовать её кодификации в трудовом договоре, не ссылаясь на то, что компания ещё может начать делать. А то когда вы на это ссылаетесь, то получается метаиронично.
И да, почти все встречавшиеся мне трудовые договора требовали от работников чего-то вроде заботы о моральном облике компании, без приведения конечного и ограниченного списка действий, которые бы считались аморальными.
Я обосновываю негативное отношение к действиям компании сейчас тем, что они уже сейчас поступают нехорошо когда начинают требовать от людей не быть меркантильными.
Ну тут понятно, конечно, что либо ежедневно хлопаешь секретаршу по заднице, либо нанимаешь синеволосых, которые пытаются инклюзивно засунуть в шутан женщину с крюком, небинарных персон и борьбу с изменением климата как игровую механику (в итоге шутан проваливается, конечно). Третьего не дано.
Интересно, в DICE снова первый вариант? bf6 походу даже играбельным будет, в отличие от предыдущих двух.
Вот опять законодатели наступают на горло свободных предпринимателей.
Мне интересно, если в некоей компании B, десятилетиями производящей известные и успешные игры, принята культура сексуальных домогательств, то бороться с ней не надо, и зачем-то она нужна, раз это работает?
Его снова пытаются "уйти", и нет ничего сложного в том, чтобы спровоцировать его "адекватность" и "человечность" прислав одновременно и мусор и со срывом сроков. А потом снова раздувать это в СМИ. А Вы на это ведётесь и тем самым льёте воду на чужую мельницу - оно Вам точно надо?
Поехавший конспиролог. Почему таблеточки принимать перестали?
тренирую внутреннего торвальдса, проявляю эмоциональную человечность и называю вещи своими именами
Противоположный. Во второй цитате вы обосновываете негативное отношение к действиям компании сейчас тем, что они могут привести к чему-то нехорошему потом. В первой цитате вы выступаете против подобного в других контекстах.
Но ситуативная этика — это социальная норма, так что ничего неожиданного.
«Сообщество» не развалилось потому, что «сообщество» сидит на зарплате у корпов, а не контрибьютит там что-то в личное время — по разным оценкам, где-то 80-85% контрибьюшенов в ядро делается людьми, сделавшими их в рабочее время за рабочую зарплату.
А в рабочее время за рабочую зарплату и не с такими напыщенными болванами работать приходится.
Смешно это слышать от человека, который обещал устроить бокс по интернету за то, что ему вернули его же высказывание о «вам курицы встречались» в разговоре о семейном бюджете.
Ты сам снежиночка та ещё, братюнь, и таешь от малейшего дуновения.
Мне лень придумывать как приведенные вами формулы удобно обернуть в программирование
Вот так всегда :(
Есть много математических библиотек для многих языков программирования. Там для обертки математических функций в функции программирования используют несколько английских слов, иногда конечно сокращая во что-то непонятное - но это все ещё более понятно чем в математике.
Можете привести примеры таких библиотек для теорката, теории типов, и так далее?
Не все. Их меньше, чем в полной записи Σ, и ваша запись описывает меньше случаев. Например, напишите, как будет выглядеть в вашей записи выражение
имя метода понятно.
А писали бы о произведении — уже было бы непонятно, что то ли произведение, то ли продукт какой-то в предметной области.
В математике же будет непонятная ∑ и параметра разбросанные сверху, снизу, сбоку.
В простейшем случае вроде покрываемого вашим Sum — нет. Я спокойно пишу Σ aᵢ, и из контекста вполне понятно, что это сумма всех элементов данной коллекции. Не нужно писать никакие параметры сверху-снизу.
В программировании можно
Окей, в математике у меня есть запись
Я сразу знаю, что это эпиморфизм (то есть, ∀ φ, ψ. φf = ψf ⇒ φ = ψ), что он действует в какую-то фактор-структуру по некоему отношению эквивалентности, и так как обычно под G понимают группы, то, скорее всего, у меня тут каноническая проекция из группы в фактор-группу по отношению эквивалентности, соответствующему какой-то нормальной подгруппе.
Можете это же записать так же выразительно в программировании, и чтобы глаза не вытекали от оверхеда синтаксиса?
Зачем плохой синтаксис математики тащить в программирование?
В математике можно наблюдать магические буквы (как минимум из греческого и латыни), стрелочки и другие неоднозначные символы. И нельзя просто так сделать обёртку, которую бы все тут же поняли и стали использовать просто подключив ваш пакет.
Как конкретно вы бы улучшили синтаксис, чтобы получилась обёртка, которую бы все тут же поняли?
Давайте на каком-нибудь примере: либо не самое сложное упражнение
Думаю, что вы отлично всё поняли, но решили дурочка включить.
Довольно забавно, что независимо от включения дурачка у вашего собеседника плюс-минус получилось докопаться до сути, и если бы не ООП, то он бы почти изобрёл Boehm-Berarducci encoding.
В этой кодировке тип Either e a = Left e | Right a (вернее, для простоты, инстанциирование его с конкретными E и A) представляется как
Either E A ≅ ∀ X. (E → X) → (A → X) → X
Left e ≅ λf. λg. f e
Right a ≅ λf. λg. g a
match (Left e) = expr1
match (Right a) = expr2
≅
λeither. either (λe → expr1) (λa → expr2)
(аннотации типов расставьте по вкусу)
Если вы знакомы с Church encoding, то Boehm-Berarducci — это, считайте, типизированный Чёрч (но есть несущественные на этом уровне нюансы).
Ваш собеседник, конечно, не удержался от того, чтобы не навернуть ООПшных интерфейсов методов перегрузка перезагрузка паблик статик финал вместо того, чтобы просто использовать параметрический полиморфизм и функции высших порядков, но смысл похожий (особенно учитывая, что вся эта ООП-муть тоже кодируется).
Похоже, у логики вашего комментария есть неявная предпосылка, что все получают более-менее одинаково, независимо от затрачиваемых усилий.
И какой вывод нужно делать из этого? Я делаю только один: работать много - хорошо и полезно для общественных достижений, только можно это буду не я :)
И это можете быть не вы, даже если вы живёте в США! В США далеко не все работают в режиме 996.
Просто тот чувак, который в таком режиме таки работает (в SpaceX, или в стартапе, или в хедж-фонде, или ещё где), получает кратно больше тех или иных ништяков (зарплаты, или ощущения причастности, или мало ли). Поэтому лично я не вижу никакого двоемыслия в этом.
Было бы интересно услышать мнение релокантов в Европу.
Пожил в Европе полтора года. Спасибо, в США лучше.
А это чем-то плохо? Вон даже википедия говорит
Я, конечно, предпочитаю избегать double negation elimination, потому что использование этой аксиомы работает только в булевых топосах (в отличие от proof of negation, часто путаемого с proof by contradiction), но что-то мне подсказывает, что вопросы у тебя не к этому.
А вот этот контраргумент неконсистентен с темой разговора :]
Нет устоявшихся студий, где вырывают сердца у геймдизайнеров. Поэтому к структуре тезиса «если X делалось раньше как один из компонентов результата Y, и Y вроде норм, то X зачем-то нужно» это не относится.
Вы правда не видите противоречия с
?
Законы физики не запрещают писать произвольные вещи, и бумага всё стерпит, понятное дело, но внутреннюю консистентность убеждений неплохо бы иметь бы.
Хотя вы можете и не иметь, конечно, законы физики не запрещают и этого.
Думаю, что там написано так, что судиться по этому поводу — себе дороже.
Бывает. Но это не тот случай.
Это случай, когда вы пишете «X, поэтому Y», а потом начинаете игру в «Y также следует из Z, а X тут ни при чём, вы меня не так поняли».
Процитированная мною часть комментария перешла на личности первой, в словах «_вы_ ведётесь», «_вы_ льёте воду», и так далее. Это намекает, что обсуждать собеседника напрямую допустимо для моего собеседника.
Ну и сложно сказать, что слова вроде «if you can't follow that rule» (где «rule» — это «I asked for early pull requests», кстати, что смешно) не являются переходом на личности в данном контексте. Это как если бы я написал первый абзац в виде «Я отвечал на конкретную отсылку к личности собеседника, и если вы неспособны понять это из текста моего комментария, то хотя бы [...]».
А, ну и да, это ж не единственный комментарий Торвальдса. Он много чего ещё говорил в духе мастурбирующих обезьянок, например.
Нет, во второй цитате вы пишете «а то сегодня ⇒ а завтра может».
Если вам не нравится некодифицированная мораль, то вы можете просто требовать её кодификации в трудовом договоре, не ссылаясь на то, что компания ещё может начать делать. А то когда вы на это ссылаетесь, то получается метаиронично.
И да, почти все встречавшиеся мне трудовые договора требовали от работников чего-то вроде заботы о моральном облике компании, без приведения конечного и ограниченного списка действий, которые бы считались аморальными.
Но написали вы не это.
Это ж парадокс неожиданной казни!
Но сводить всё к аналогии с гениталиями тоже нельзя.
Ну тут понятно, конечно, что либо ежедневно хлопаешь секретаршу по заднице, либо нанимаешь синеволосых, которые пытаются инклюзивно засунуть в шутан женщину с крюком, небинарных персон и борьбу с изменением климата как игровую механику (в итоге шутан проваливается, конечно). Третьего не дано.
Интересно, в DICE снова первый вариант? bf6 походу даже играбельным будет, в отличие от предыдущих двух.
Устrоим миrовую rеволюцию анаrхо-капитализма, товаrищи!
Мне интересно, если в некоей компании B, десятилетиями производящей известные и успешные игры, принята культура сексуальных домогательств, то бороться с ней не надо, и зачем-то она нужна, раз это работает?
Поехавший конспиролог. Почему таблеточки принимать перестали?
тренирую внутреннего торвальдса, проявляю эмоциональную человечность и называю вещи своими именами
Противоположный. Во второй цитате вы обосновываете негативное отношение к действиям компании сейчас тем, что они могут привести к чему-то нехорошему потом. В первой цитате вы выступаете против подобного в других контекстах.
Но ситуативная этика — это социальная норма, так что ничего неожиданного.
«Сообщество» не развалилось потому, что «сообщество» сидит на зарплате у корпов, а не контрибьютит там что-то в личное время — по разным оценкам, где-то 80-85% контрибьюшенов в ядро делается людьми, сделавшими их в рабочее время за рабочую зарплату.
А в рабочее время за рабочую зарплату и не с такими напыщенными болванами работать приходится.
Смешно это слышать от человека, который обещал устроить бокс по интернету за то, что ему вернули его же высказывание о «вам курицы встречались» в разговоре о семейном бюджете.
Ты сам снежиночка та ещё, братюнь, и таешь от малейшего дуновения.
Вот так всегда :(
Можете привести примеры таких библиотек для теорката, теории типов, и так далее?
Я вот могу привести что-нибудь из агды, где это есть, и там значочки не сильно лучше, например: https://agda.github.io/agda-categories/Categories.Category.Monoidal.Core.html или https://agda.github.io/agda-stdlib/v2.3/Function.Base.html — тоже значочки-закорючки какие-то непонятные, очень часто — односимвольные.
Не все. Их меньше, чем в полной записи Σ, и ваша запись описывает меньше случаев. Например, напишите, как будет выглядеть в вашей записи выражение
А писали бы о произведении — уже было бы непонятно, что то ли произведение, то ли продукт какой-то в предметной области.
В простейшем случае вроде покрываемого вашим
Sum— нет. Я спокойно пишу Σ aᵢ, и из контекста вполне понятно, что это сумма всех элементов данной коллекции. Не нужно писать никакие параметры сверху-снизу.Окей, в математике у меня есть запись
Я сразу знаю, что это эпиморфизм (то есть, ∀ φ, ψ. φf = ψf ⇒ φ = ψ), что он действует в какую-то фактор-структуру по некоему отношению эквивалентности, и так как обычно под G понимают группы, то, скорее всего, у меня тут каноническая проекция из группы в фактор-группу по отношению эквивалентности, соответствующему какой-то нормальной подгруппе.
Можете это же записать так же выразительно в программировании, и чтобы глаза не вытекали от оверхеда синтаксиса?
Как конкретно вы бы улучшили синтаксис, чтобы получилась обёртка, которую бы все тут же поняли?
Давайте на каком-нибудь примере: либо не самое сложное упражнение
либо кусочек статьи:
Я готов отвечать на уточняющие вопросы произвольно глубоко, насколько вам это нужно (особенно по первому примеру).
В качестве задачи со звёздочкой можно обсудить нотацию для, скажем,
Довольно забавно, что независимо от включения дурачка у вашего собеседника плюс-минус получилось докопаться до сути, и если бы не ООП, то он бы почти изобрёл Boehm-Berarducci encoding.
В этой кодировке тип
Either e a = Left e | Right a(вернее, для простоты, инстанциирование его с конкретнымиEиA) представляется как(аннотации типов расставьте по вкусу)
Если вы знакомы с Church encoding, то Boehm-Berarducci — это, считайте, типизированный Чёрч (но есть несущественные на этом уровне нюансы).
Ваш собеседник, конечно, не удержался от того, чтобы не навернуть ООПшных интерфейсов методов перегрузка перезагрузка паблик статик финал вместо того, чтобы просто использовать параметрический полиморфизм и функции высших порядков, но смысл похожий (особенно учитывая, что вся эта ООП-муть тоже кодируется).
Даже это, нетотальное, не существующее в том же
total-идрисе, громче (потому чтоright (Left foo)не продолжит выполнение), чемкоторое по установленному исходным комментатором «исключения невозможно проигнорировать» бейзлайну не считается.
Вы же:
Не, вам всё же стоит определиться.
Похоже, у логики вашего комментария есть неявная предпосылка, что все получают более-менее одинаково, независимо от затрачиваемых усилий.
И это можете быть не вы, даже если вы живёте в США! В США далеко не все работают в режиме 996.
Просто тот чувак, который в таком режиме таки работает (в SpaceX, или в стартапе, или в хедж-фонде, или ещё где), получает кратно больше тех или иных ништяков (зарплаты, или ощущения причастности, или мало ли). Поэтому лично я не вижу никакого двоемыслия в этом.
Пожил в Европе полтора года. Спасибо, в США лучше.
Как тут проигнорировать ручной result?
Но ведь вайб-кодеры не читают код!