там, где имеет место HOA (HomeOwner Assocation) — сообщество домовладельцев — и там в правилах сообщества прописаны требования к участникам (типа «крыша только красная, трава не длиннее 2 дюймов, собак кормить только мраморным стейком и т. п.»)
У далеко не всех HOA такие требования. Трава должна быть просто опрятной, крышу я спокойно поменял на слегка другого цвета вообще без согласования с HOA, окна — тоже, солары поставил в уведомительном порядке (лан, тут законы Техаса обязывают их разрешить, если уведомление направлено, так что я даже не ждал ответа).
А даже те правила, что есть, энфорсятся не всегда. Например, собакам запрещено «excessive barking», но это не мешает одному товарищу четыре раза в день по 15 минут выгуливать свою незатыкающуюся и триггерящуюся на любое движение псину, что несколько мешает держать окна открытыми и при этом заниматься требующими концентрации делами. Это практически невозможно починить в данной полураздолбайской HOA, и я был бы рад жить там, где это энфорсится куда строже.
Ну то есть всё это социальные конструкты, только одни получше, а другие похуже.
Да, и?
Я говорю не о том, какие это конструкты, а о том, откуда идёт инициатива по их насаждению. Снизу вверх — может, норм, может, плохо. Сверху вниз — практически всегда плохо.
А теперь возьмем ситуацию, когда команда разработчиков не может договориться про выбор методики работы. Что тогда делать бизнесу, садиться и плакать? Нет же, top-down-процесс спешит на помощь!
Во-первых, бизнес ничего не делает. В нормальной группе что-то решает в данном случае тимлид, а не весь бизнес целиком. Это совсем не тот же top-down-процесс, как если бы CEO посмотрел буллшит-доклад какого-нибудь Мартина на какой-нибудь конферфенции с задорно выглядящими графиками и решил «мы теперь все работает по аджайлу».
Во-вторых, устраиваясь на работу в данную группу к данному тимлиду, я в том числе осознанно и открыто делегировал ему часть ответственности и больший вес по принятию решений (по крайней мере, выяснить, хочу ли я ему это делегировать — моя цель на интервью как нанимающегося). Рождение в данном государстве с данной политической системе (или пересечение отрезка жизни с революцией) не является настолько же осознанным и добровольным.
В-третьих, поменять группу (или работу) куда проще, чем государство. Настолько проще, что по факту дисбалансом власти между тимлидом и линейным программистом можно пренебречь.
С учётом всего этого говорить, что там характеристики top-down-процессов одинаковые, и
не только государства воплощают этот принцип, а и любая (почти, так как bottom-up бизнесов крайне мало) другая организация
а вы попробуйте выразить Ферма на ваших типах и убедитесь, что это именно констрейнты
Как раз выразил выше (опустив не сильно важную для дискуссии деталь).
Так всё же, слова «уравнение a^n + b^n = c^n не имеет решения в целых ненулевых числах для n ≥ 3» являются просто констрейнтом на подмножество (и чего), или нет?
Я понимаю, что очень хочется уязвить собеседника, но в следующий раз попробуйте привязываться к контексту его комментария целиком, а не к одному ключевому слову.
Мне очень интересно, откуда у вас вылезет теоркат в разработке оптимизирующего компилятора императивного ЯП?
Даже для функциональщины для оптимизаций вроде «композиция катаморфизма F-алгебры и стрелки той же алгебры при определённых условиях выражается единым катаморфизмом» хватает совершенно базовых определений и практически школьного понимания универсального свойства (даже конусы строить не надо!), а применения всякого чуть более хардкорного теорката (codensity monad для функтора там, которая строится как right Kan extension для этого функтора вдоль него же) вполне описывается практически без теорката.
Только для первых трёх пунктов достаточно практически школьного уровня и справочника, для четвёртого и шестого — этим занимается очень мало людей (особенно на уровне выше, чем «запихнуть данную от аналитиков формулу в солвер»), для пятого — необходимость статов и теорвера несколько переоценена для продуктового машинного обучения.
А какие это результаты в случае программиста? В моём опыте чем больше для задачи нужно математики, тем хуже условия труда и тем меньше за работу платят.
Математика и высшее образование вообще меня сделали хуже, ИМХО.
То, что Вы зовёте теоремами - простые констрейнты, ограничивающие подмножество внутри множества.
Вот это:
∀ n → n ≥ 3 → ∀ a b c → a ^ n + b ^ n ≢ c ^ n
тоже просто констрейнт?
Тип не защитит Вас от того, что Вы в этом месте напишете x > 0 вместо x >= 0.
Я вам в куче разных веток уже показывал, что защитит. Вы продолжаете твердить одно и то же из ветки в ветку, с завидным упорством игнорируя наблюдаемые данные. Как это можно назвать?
Когда наблюдаемые данные противоречат предсказаниям науки, вы меняете теорию и аксиомы.
Когда наблюдаемые данные противоречат предсказаниям богословия, вы сжигаете еретика или в лучшем случае применяете фундаментальную аксиому «пути господни неисповедимы».
Потому что подразумевается математическая логика, которая слегка отличается от богословской или ещё какой.
Кроме названий у анонимных функций, каким боком программирование может стоять близко к лямбда исчислению?
Лямбда-исчисление является моделью для программирования. Можно сформулировать язык в терминах одного из лямбда-исчислений и потом описывать его свойства, опираясь на соответствующий матаппарат.
что такое тип в программировании? Это сущность отделяющая одно значение от другого.
Нет. Это способ классификации выражений, который описывает, что с этими выражениями можно делать (или что они сами делают), а что — нельзя (или не делают).
Куски достаточно глубокой теории лежат даже тогда, когда вы обсуждаете ковариантность или контравариантность аргументов и возвращаемых значений ваших фукнций в вашей иерархии ООП-классов, или ко/контравариантность дженериков.
Но при чём здесь теория типов из математики? Ага, снова ни при чём!
Только в том случае, если вы с ней незнакомы. Но это больше говорит о вашем уровне знаний, а не о теории типов.
здесь тоже скрещивающиеся прямые: не всякий алгоритм может быть запрограммирован.
Лолшто.
Алгоритм — это практически по определению то, что может быть запрограммировано на тьюринг-полном языке.
Соответственно: математика - язык, на котором та или иная наука МОЖЕТ выражать свои выводы. А может этого не делать.
Может. Только науки без математики остались глубоко в прошлом, потому что даже современная, не знаю, биология весьма пользуется математикой (например, для построения филогенетических деревьев для анализа близости организмов, консервативности мутаций, и так далее).
Другое дело, что программирование — не наука, и программированием можно успешно заниматься (сиречь делать работу и получать за неё деньги) со школьным знанием математики. Просто неплохо при этом осознавать границы своего знания, а не рассказывать «да это всё не может быть нужно и не имеет никакого отношения».
Их действительно можно перепутать, но не потому, что вы не знаете, какой значок что означает, а потому, что предметная область сложная.
Да, там ведь используются совершенно одинаковые навыки. Матан — это про зубрёж, как таблица умножения.
Таблицу умножения по какому основанию, кстати? По основанию 30 запомнить и вы вряд ли сможете уже, но что это говорит?
У далеко не всех HOA такие требования. Трава должна быть просто опрятной, крышу я спокойно поменял на слегка другого цвета вообще без согласования с HOA, окна — тоже, солары поставил в уведомительном порядке (лан, тут законы Техаса обязывают их разрешить, если уведомление направлено, так что я даже не ждал ответа).
А даже те правила, что есть, энфорсятся не всегда. Например, собакам запрещено «excessive barking», но это не мешает одному товарищу четыре раза в день по 15 минут выгуливать свою незатыкающуюся и триггерящуюся на любое движение псину, что несколько мешает держать окна открытыми и при этом заниматься требующими концентрации делами. Это практически невозможно починить в данной полураздолбайской HOA, и я был бы рад жить там, где это энфорсится куда строже.
Да, и?
Я говорю не о том, какие это конструкты, а о том, откуда идёт инициатива по их насаждению. Снизу вверх — может, норм, может, плохо. Сверху вниз — практически всегда плохо.
Во-первых, бизнес ничего не делает. В нормальной группе что-то решает в данном случае тимлид, а не весь бизнес целиком. Это совсем не тот же top-down-процесс, как если бы CEO посмотрел буллшит-доклад какого-нибудь Мартина на какой-нибудь конферфенции с задорно выглядящими графиками и решил «мы теперь все работает по аджайлу».
Во-вторых, устраиваясь на работу в данную группу к данному тимлиду, я в том числе осознанно и открыто делегировал ему часть ответственности и больший вес по принятию решений (по крайней мере, выяснить, хочу ли я ему это делегировать — моя цель на интервью как нанимающегося). Рождение в данном государстве с данной политической системе (или пересечение отрезка жизни с революцией) не является настолько же осознанным и добровольным.
В-третьих, поменять группу (или работу) куда проще, чем государство. Настолько проще, что по факту дисбалансом власти между тимлидом и линейным программистом можно пренебречь.
С учётом всего этого говорить, что там характеристики top-down-процессов одинаковые, и
просто неверно и подмена тезиса.
Как раз выразил выше (опустив не сильно важную для дискуссии деталь).
Так всё же, слова «уравнение a^n + b^n = c^n не имеет решения в целых ненулевых числах для n ≥ 3» являются просто констрейнтом на подмножество (и чего), или нет?
Вы:
Я:
Я понимаю, что очень хочется уязвить собеседника, но в следующий раз попробуйте привязываться к контексту его комментария целиком, а не к одному ключевому слову.
Я именно к этому контексту и отсылаю. Или мне нужно все ваши комментарии целиком сюда копировать, а то иначе вы не вспомните, что вы сами писали?
И моя религия выражается в том, что я имею наглость регулярно вам напоминать, что от
>вместо≥типы тоже спасают, и показывать, как?Не все алгоритмы обязаны завершаться на любом входе. Не понимаю вашей претензии.
Ну почему же, есть. Даже в Пирсе в TAPL (базовая, вводная книжка) про это целая глава отведена.
Так, стоп. А великая теорема Ферма — это тоже просто констрейнт?
А можете вы меня просвятить, пожалуйста?
Полностью поддерживаю (в естественноязычной интерпретации: высказывание «2 + 2 = 4» не будет ересью, даже если исходит от марксиста).
Маркс напихал взаимных противоречий в свою логическую систему и сидит довольный, потому что теперь может доказать что угодно. Ура! Ура! Ура!
Для подробного разбора, почему Гегель вместе с Марксом — это гибель мозга, можете почитать второй том Поппера Open Society and Its Enemies, например.
А ещё Петрика ересью считают!
Дело в том, что учение Петрика (или Маркса) не является наблюдаемым фактом в петриковщине (или экономике).
Оттого, что вы будете раз за разом повторять «типы нинужны», это не станет разумным, практическим аргументом.
Мне очень интересно, откуда у вас вылезет теоркат в разработке оптимизирующего компилятора императивного ЯП?
Даже для функциональщины для оптимизаций вроде «композиция катаморфизма F-алгебры и стрелки той же алгебры при определённых условиях выражается единым катаморфизмом» хватает совершенно базовых определений и практически школьного понимания универсального свойства (даже конусы строить не надо!), а применения всякого чуть более хардкорного теорката (codensity monad для функтора там, которая строится как right Kan extension для этого функтора вдоль него же) вполне описывается практически без теорката.
Только для первых трёх пунктов достаточно практически школьного уровня и справочника, для четвёртого и шестого — этим занимается очень мало людей (особенно на уровне выше, чем «запихнуть данную от аналитиков формулу в солвер»), для пятого — необходимость статов и теорвера несколько переоценена для продуктового машинного обучения.
Можете пояснить, какого уровня теорию множеств вы считаете необходимой для написания программ?
Берёте язык вроде Qimaera... А, тьфу ты, там опять математика, и даже теория типов и прочее.
Праввила отношений этих классов возьмутся откуда?
А какие это результаты в случае программиста? В моём опыте чем больше для задачи нужно математики, тем хуже условия труда и тем меньше за работу платят.
Математика и высшее образование вообще меня сделали хуже, ИМХО.
Вот это:
тоже просто констрейнт?
Я вам в куче разных веток уже показывал, что защитит. Вы продолжаете твердить одно и то же из ветки в ветку, с завидным упорством игнорируя наблюдаемые данные. Как это можно назвать?
Когда наблюдаемые данные противоречат предсказаниям науки, вы меняете теорию и аксиомы.
Когда наблюдаемые данные противоречат предсказаниям богословия, вы сжигаете еретика или в лучшем случае применяете фундаментальную аксиому «пути господни неисповедимы».
Потому что подразумевается математическая логика, которая слегка отличается от богословской или ещё какой.
Лямбда-исчисление является моделью для программирования. Можно сформулировать язык в терминах одного из лямбда-исчислений и потом описывать его свойства, опираясь на соответствующий матаппарат.
Нет. Это способ классификации выражений, который описывает, что с этими выражениями можно делать (или что они сами делают), а что — нельзя (или не делают).
Куски достаточно глубокой теории лежат даже тогда, когда вы обсуждаете ковариантность или контравариантность аргументов и возвращаемых значений ваших фукнций в вашей иерархии ООП-классов, или ко/контравариантность дженериков.
Только в том случае, если вы с ней незнакомы. Но это больше говорит о вашем уровне знаний, а не о теории типов.
Лолшто.
Алгоритм — это практически по определению то, что может быть запрограммировано на тьюринг-полном языке.
Может. Только науки без математики остались глубоко в прошлом, потому что даже современная, не знаю, биология весьма пользуется математикой (например, для построения филогенетических деревьев для анализа близости организмов, консервативности мутаций, и так далее).
Другое дело, что программирование — не наука, и программированием можно успешно заниматься (сиречь делать работу и получать за неё деньги) со школьным знанием математики. Просто неплохо при этом осознавать границы своего знания, а не рассказывать «да это всё не может быть нужно и не имеет никакого отношения».
Теслу.
Лайтнинг в гараж тупо не влазит.