Это точно полный и окончательный фикс? Я не вижу как он может предовратить имплементацию DerefMut, перемещающую self куда-нибудь. Или, например, меняющую местами две части self, которые отдаются в норме только через Pin (structured pinning это называется, кажется).
Если вы про пилот-волну, то она на самом деле не особо позволяет решить проблему измерения. Максимум — немного запутать дело так, что на первый взгляд проблема кажется решённой.
А что касается нелокальных скрытых параметров, то волновая функция в известном смысле таким параметром и является.
То что Optional нарушает монадные законы — это ясно. Что это, по-идее, плохо — тоже (я сам дважды имел неприятности из-за отсутствия ассоциативности там, где априори она ожидалась — с другими недомонадами, не с Optional).
Неясно, реально ли это мешает пользоваться Optional. Выглядит так, что конкретно в этом случае нарушение монадных законов не приводит к реальным проблемам.
По первой ссылке пишется явно корявый код (про который по второй ссылке говорится, что он "should never have existed"), а потом демонстрируется, что к нему трудно прикрутить Optional. Вот только к нему что угодно трудно прикрутить, ибо он коряв изначально.
По второй ссылке демонстрируются реальные проблемы, но они никак не связаны с нарушением монадных законов.
Ну, википедия она такая. Даже английская. Лучше загляните в хороший учебник. Это не хороший учебник, но здесь есть главная идея первого закона:
Первый закон Ньютона (или закон инерции) из всего многообразия систем отсчета выделяет класс так называемых инерциальных систем.
и собственно правильная формулировка:
Существуют такие системы отсчета, относительно которых изолированные поступательно движущиеся тела сохраняют свою скорость неизменной по модулю и направлению.
А ещё существуют неинерциальные системы отсчёта, в которых второй закон Ньютона не выполняется. И то, что можно всегда найти хотя бы одну инерциальную систему отсчёта — это нетривиально. (А то, что если есть хотя бы одна ИСО, то есть и много других ИСО, уже весьма просто доказывается.)
Мне дописывать не хочется, я не вижу в этом смысла. Но я считаю, что это возможно, хотя немного повозиться придётся.
Это вы записали, что "тела, на которые не действуют силы, движутся равномерно". А первый закон — "существуют СО, такие что в них тела, на которые не действуют силы, движутся равномерно".
На самом деле нет, не является. Первый закон утверждает, что всегда, в любой ситации можно найти систему отсчёта, являющуюся инерциальной. Я думаю, если очень надо, то его можно записать в виде формулы, правда смысла в этом большого нет.
Because of these difficulties, Haskell developers tend to think in some subset of Haskell where types do not have bottom values. This means that it only includes functions that terminate, and typically only finite values.
Напомню, что ни один Unix (настоящий Unix, ведущий родословную от разработки Кена Томпсона и Деннисом Ритчи) не позволяет вам выбирать, скажем, системный логгер.
Отсюда, очевидно, следует, что в идеале cистемный логгер и должен быть частью системы и поставляться с ней. Всегда.
Вы хотите пользоваться философией Unix, а я хочу пользоваться собственно Unix. Ну или чем-то похожим на Unix. И у меня это было, у меня был GNU/Linux. А потом у меня забрали возможность пользоваться GNU/Linux и подсунули вместо него systemd.
Если бы udev и всё остальное, не имеющее никакого отношения к PID 1, не шло в комплекте с systemd, им бы все пользовались с удовольствием.
А тем барахлом, что существует в реальности и называется systemd, добровольно пользуются только виндузятники, которым надёжность программ, а также удобство пользователей и разработчиков, дороже, чем принципы.
Зависит от того что понимать под троллингом. Но скорее нет, чем да, так как это выражение моего актуального мнения. Оно в значительной степени иррационально, но отсюда ещё не следует, что оно неверно.
Steam на Linux на самом деле не работает, потому что он 32-битный, а Линуксы — 64-битные или даже на arm. Если вам кажется, что он работает — то это только потому что 64-битные процессоры имеют совместимость с 32-битными (и эта ошибка неустранима), а Linux'ы имеют штуку под названием multiarch, и вот это легко исправляется: достаточно удалить multiarch и Steam либо удалится вместе с ним, либо перестанет работать, как это и должно быть.
Как раз используя обычную математику с обычным законом исключённого третьего можно доказать, что множество конструктивных действительных чисел счётно. (Доказательство тривиально: каждому конструктивному действительному числу соответсвует программа, его вычисляющая, а количество программ, очевидно, счётно.)
Поскольку аксиома счётного выбора следует из аксиомы детерменированности, замена аксиомы выбора на аксиому детерменированности ничего не изменит.
Однако, в конструктивной математике место вопроса о счётности занимает вопрос об эффективной счётности (перечислимости). И оказывается, что конструктивные числа неперечеслимы (это доказывается как раз диагональным методом). Поэтому — хоть это и может показаться неожиданным — на самом деле ситуация с действительными числами в конструктивной математике мало отличается от аналогичной ситуации в обычной математике.
Это точно полный и окончательный фикс? Я не вижу как он может предовратить имплементацию
DerefMut, перемещающуюselfкуда-нибудь. Или, например, меняющую местами две частиself, которые отдаются в норме только черезPin(structured pinning это называется, кажется).Тем не менее, получается, что "благодаря"
Pinсочетание safe Rust + standard library может приводить к BC. И это закрыли без фикса: https://github.com/rust-lang/rust/issues/66544Если вы про пилот-волну, то она на самом деле не особо позволяет решить проблему измерения. Максимум — немного запутать дело так, что на первый взгляд проблема кажется решённой.
А что касается нелокальных скрытых параметров, то волновая функция в известном смысле таким параметром и является.
То что
Optionalнарушает монадные законы — это ясно. Что это, по-идее, плохо — тоже (я сам дважды имел неприятности из-за отсутствия ассоциативности там, где априори она ожидалась — с другими недомонадами, не сOptional).Неясно, реально ли это мешает пользоваться
Optional. Выглядит так, что конкретно в этом случае нарушение монадных законов не приводит к реальным проблемам.По первой ссылке пишется явно корявый код (про который по второй ссылке говорится, что он "should never have existed"), а потом демонстрируется, что к нему трудно прикрутить
Optional. Вот только к нему что угодно трудно прикрутить, ибо он коряв изначально.По второй ссылке демонстрируются реальные проблемы, но они никак не связаны с нарушением монадных законов.
Ну, википедия она такая. Даже английская. Лучше загляните в хороший учебник. Это не хороший учебник, но здесь есть главная идея первого закона:
и собственно правильная формулировка:
А ещё существуют неинерциальные системы отсчёта, в которых второй закон Ньютона не выполняется. И то, что можно всегда найти хотя бы одну инерциальную систему отсчёта — это нетривиально. (А то, что если есть хотя бы одна ИСО, то есть и много других ИСО, уже весьма просто доказывается.)
Мне дописывать не хочется, я не вижу в этом смысла. Но я считаю, что это возможно, хотя немного повозиться придётся.
Это вы записали, что "тела, на которые не действуют силы, движутся равномерно". А первый закон — "существуют СО, такие что в них тела, на которые не действуют силы, движутся равномерно".
На самом деле нет, не является. Первый закон утверждает, что всегда, в любой ситации можно найти систему отсчёта, являющуюся инерциальной. Я думаю, если очень надо, то его можно записать в виде формулы, правда смысла в этом большого нет.
Вообще-то уже без боттомов:
Отсюда, очевидно, следует, что в идеале cистемный логгер и должен быть частью системы и поставляться с ней. Всегда.
Вы хотите пользоваться философией Unix, а я хочу пользоваться собственно Unix. Ну или чем-то похожим на Unix. И у меня это было, у меня был GNU/Linux. А потом у меня забрали возможность пользоваться GNU/Linux и подсунули вместо него systemd.
Если бы udev и всё остальное, не имеющее никакого отношения к PID 1, не шло в комплекте с systemd, им бы все пользовались с удовольствием.
А тем барахлом, что существует в реальности и называется systemd, добровольно пользуются только виндузятники, которым надёжность программ, а также удобство пользователей и разработчиков, дороже, чем принципы.
Подтверждаю, в приличном обществе Педивикию принято называть "мусоркой", а не "помойкой".
А вы сидите в ровной позе с прямой спиной? Да, так наверно это может работать.
А ноги вы куда денете? У меня они и при стандартной высоте не вполне влезают.
и убиться об стеклянный стол...
А Windows и так костыль на костыле, так что к ней аргумент не применим.
Но не очевидно, что нельзя получить более приятных и впечатляющих впечатлений, чем с VR.
Зависит от того что понимать под троллингом. Но скорее нет, чем да, так как это выражение моего актуального мнения. Оно в значительной степени иррационально, но отсюда ещё не следует, что оно неверно.
Steam на Linux на самом деле не работает, потому что он 32-битный, а Линуксы — 64-битные или даже на arm. Если вам кажется, что он работает — то это только потому что 64-битные процессоры имеют совместимость с 32-битными (и эта ошибка неустранима), а Linux'ы имеют штуку под названием multiarch, и вот это легко исправляется: достаточно удалить multiarch и Steam либо удалится вместе с ним, либо перестанет работать, как это и должно быть.
Как раз используя обычную математику с обычным законом исключённого третьего можно доказать, что множество конструктивных действительных чисел счётно. (Доказательство тривиально: каждому конструктивному действительному числу соответсвует программа, его вычисляющая, а количество программ, очевидно, счётно.)
Поскольку аксиома счётного выбора следует из аксиомы детерменированности, замена аксиомы выбора на аксиому детерменированности ничего не изменит.
Однако, в конструктивной математике место вопроса о счётности занимает вопрос об эффективной счётности (перечислимости). И оказывается, что конструктивные числа неперечеслимы (это доказывается как раз диагональным методом). Поэтому — хоть это и может показаться неожиданным — на самом деле ситуация с действительными числами в конструктивной математике мало отличается от аналогичной ситуации в обычной математике.