Например в агде уже не написать, потому что в юникоде нет символа .
Это на самом деле тоже раздражает, но между кастомным рендерером в редакторе (что заодно привязывает меня к редактору — вряд ли nvim так же умеет) и ограничением в индексах я скорее выберу второе.
Можешь привести какой-то пример? Я, кажется, не совсем понимаю что имеется ввиду
«Монада» — это просто такой интерфейс, удовлетворяющий определённым законам, как «ассоциативный контейнер» или «итератор». Зачем человека сразу теоркатом грузить?
Ну хз. Шрифты с закорючками всё равно нужны (а то как их редактор рисует-то?), аккорды вводить всё равно нужно (просто они не автозаменяются на уникодные символы), но при этом вне редактора (на гитхабе, например) приходётся читать неформатированный латех. По-моему, это строго нелучше и по некоторым аспектам хуже.
Во-первых набор символов сильно ограничен по сравнению с техом
Можно добавлять нужные, но отсутствующие в ваш редактор! Агде ж всё равно, она любой уникод жрёт.
А говорить, что (разовая, имеющая константную сложность) подготовка окружения к работе с каким-то инструментом — это недостаток инструмента, очень странно. Тогда все инструменты отстой и не готовы для бизнеса, потому что для всех инструментов нужно готовиться. Даже для программирования в машинных кодах надо хекс-редактор поставить.
Ну либо остаться на машинах, где весь интерфейс сводился к тумблерам на передней панели — там ничего ставить и готовиться не надо, идеальные машины, только бизнес тупой и слез с них почему-то.
Сами по себе закорючки возможно были бы ок, если бы был нормальный способ их вводить.
Ненормальный способ их вводить — это, условно, тыкать по экранной клавиатуре. Я не вижу существенных проблем с упомянутым выше способом, когда равенство из трёх горизонтальных палочек — это просто два знака равно подряд.
Слои на эргодоксе — ещё удобнее. Для определённой задачи определённые инструменты повышают удобство ⇒ я покупаю этот инструмент и овладеваю им. А с вашей точки зрения ни один бизнес никогда бы не завязался на аппсторы и производство приложений для них, потому что там нужно купить макбук (сильно дороже эргодокса) и получить полный вендорлок на конкретную экосистемы.
А способов ввода текстов в пяти измерениях нет вообще, никаких.
А вот код на go, например, у меня тоже не заведётся за отсутствием компилятора go.
Не знаю. Об этом надо много думать, я не позиционирую себя как дизайнер языков программирования.
Ну вот оказывается, что во всех языках, которые претендуют на хотя бы возможность формализации таких вещей и которые при этом успешны на этом поприще, есть возможность (и культура) работы с закорючками, кастомные миксфиксные операторы (вот эти все трёх-четырёх-пятиместные штуки с подчёркиваниями), и так далее. Много разных людей думало и не придумало ничего лучше.
Но не надо быть поваром чтобы понять что борщ недосолен.
У всех аналогий есть границы применимости, и у этой тоже.
Но вообще записать что-то в младший битик указателя, а потом вернуть всё обратно перед использованием — вроде как не UB. С pointer provenance ерунда будет, вероятно, но у меня есть чувство, что pointer provenance не понимает даже Комитет.
Ширину строк в кодстайле/линтере сделали такой, чтобы side-by-side-дифф влезал на экран? Или, может, удобство работы с мобильника не является ключевым фактором для кодингового окружения?
У меня были работы, где весь кодинг шёл через RDP на серверах где-то там, для доступа к чему надо было приложить палец к yubikey, вставленному в usb-порт. Код (и ревью, и прочее) у меня с мобилы не открывался вообще никак, ни квадратиками, ни вопросиками. Я правильно понимаю, что RDP — непригодная технология, и никакой бизнес на неё завязываться не будет?
Но это риторические вопросы. Нериторический, серьёзный вопрос другой: какая альтернатива? Как бы вы написали выражение выше, чтобы без закорючек?
Вы знаете ответ, никак, это придётся просто запомнить. Впрочем, я и не настаиваю что моё утверждение применимо ко всем языкам.
Подобный костыльный short-circuiting есть во всех¹ императивных языках, и подобная разница есть везде¹, где есть заодно и битовые операторы. Плюс, он действительно костыльный: например, в плюсах &&коротит только для встроенных типов, и свои short-circuiting-операторы вы определять не можете нигде¹.
¹ из тех языков, про которые я хоть что-то достаточно знаю, конечно
И у C есть куча недостатков и кривых решений (зачем вообще над указателем можно делать & я не знаю).
Я мог бы написать (bool)str, суть это меняет не сильно.
Но вообще затем, зачем над указателями вообще делать битовую арифметику: чтобы в младших (или старших) битиках там что-нибудь хранить. Во всяких локфри бывает полезно, да и вообще память экономит, так как указатели выровнены, и эти битики пропадают (а старшие на x86_64 не используются).
У вас очень много опечаток в фразе "Agda это решает через костыли".
Не нашёл ни одной, потому что написано то, что я и так хотел сказать.
Код пишется один раз, а читается много раз. Куда удобнее читать код, в котором не используются (визуальные) многозначковые комбинации или, чего хуже, слова, для тех вещей, для которых в предметной области есть устоявшаяся нотация.
где используются кастомные операторы и функции-закорючки, в порядке их появления — трёхместный _⊢[_]_ (_ обозначает, куда идёт аргумент) и бинарный _⇒_ на первой строке; четырёхместный _⊢[_]_⦂_ и бинарный _,_ во второй строке, и бинарный ƛ в третьей. Как бы вы написали это обычными словами, чтобы это можно было прочитать?
Если бы на клавиатурах реально был символ ≗
Одна из причин мне использовать эргодокс со слоями. Греческие буквы и наиболее частые символы я повесил на отдельные слои.
и у него было человеческое название
Поточечное пропозициональное равенство двух функций.
Но вот это вот изобретение нотации в шарообоазном вакууме в отрыве от реального мира - спасибо, нет.
Ох уж этот реальный мир и отсылки к нему, когда по реальным миром каждый понимает что-то своё.
в риальном мире так та и матиматика ненужна, и вуз, и дажи старшые классы школы. чаивые калькулятар пащитает, а граматнаст тоже ненужна ведь вы этоттекст тоже можите прачитать и панять што яимел ввиду
Клавиатура заточена под ввод букв и цифр, а не вот этой вот вашей красоты.
Agda это успешно решает вводом закорючек через аккорды. Например, ≡ — это \==, а ≗ — \circeq.
Люди общаются между собой словами. Все эти значочки надо как-то называть (а значит слова будут)
В агде это тоже решается: люди вполне успешно описывают эти значочки терминами из предметной области, например.
Незнакомый с нотацией человек мало того что неспособен прочесть написанное, он даже не может нормально задать вопрос "что делает Х", потому что непонятно как назвать Х.
И это.
Что-то я подозреваю что гуглить это всё тоже окажется околоневозможно.
Пользователю важно, что там есть тесты? Нет. Менеджменту и бизнесу важно, что там есть тесты? Нет.
Тесты ничего не добавляют, только вынуждают раздувать код в восемь и шесть седьмых раз, чтобы добавить все нужные моки, интерфейсы, SOLID и DI. Вы знаете, что в Штатах сейчас вообще правительство DEI запретило? Это просто хотели запретить DI из-за феерического разбазаривания ресурсов на пять экранов кода на каждую функцию, но просто когда печатали текст указа, то случайно вместе с D нажали на кнопку над ней (и тесты это не поймали, обратите внимание — толку с них?).
если легче читать с аннотациями, то вывод типов - это усложнение чтения
Топ-левел-байндинги легче читать с аннотациями, нетривиальные функции легче читать с аннотациями, простые вещи и локальные переменные легче читать без аннотаций.
У вас тезис уровня «вы определитесь, или говорящие имена переменных, или i как индекс массива».
ибо аннотации в общем случае удваивают количество кода
Мутабельность к этому не имеет вообще никакого отношения.
фотон без наблюдения ведёт себя иначе, чем если за ним наблюдают.
И там, где это важно, это пытаются минимизировать. Вы же даже не пытаетесь это сделать, а ставите те эксперименты, которые легче поставить (напихать трейсов и потом с умным видом сидеть их разглядывать), а не те, которые относятся к вашему предмету исследования (почему тормозит).
это именно про типы и было.
Абсолютно верно, без типов этой проблемы нет.
Этот тип является суммой множества типов
Вы даже сами сказали, «этот тип». Тип один, всё.
причём крайне разнородных, таких, как "контейнер сложных документов"
Обычная индукция/рекурсия, не вижу проблем.
и "ошибка".
Если это не часть семантики yaml, то это они зря, конечно. Но это вопрос конкретной реализации, а не теории типов.
в реализации этого типа под капотом точно та же структура, что получается при динамической типизации
Да, и? Вы думаете, тут цель — выпендриться и иметь в рантайме какое-то другое представление (что, кстати, делают с GADT'ами, но вы ещё не там)? Тут цель — это проверки в компилтайме, до запуска.
а просто когда у вас список становится большим, а он вон на простых примерах уже большой, чтобы возникнуть проблемам
а отсылка про то, что такое наблюдение влияет на наблюдаемый объект, она разве не про мутабельность была?
Эта отсылка была к тому, что ПО с дебагами и прочими трейсами ведёт себя совсем не так, как без них.
ага, это просто цена за инструмент. просто нужно о ней знать и всё.
Попробуйте в следующий раз дочитывать комментарии до конца. Или хрен с ними с комментариями, фразы-то до конца дочитывайте.
и О(N^2) на время разработки
и О(N^4) на поиск багов
А использовали бы типы — не было бы такой ерунды у вас, как вы описываете.
Возможность написать функцию, которая будет обрабатывать сразу много разных типов.
Нет, конечно. Она всё ещё обрабатывает ровно один тип.
а в языке динамической типизации эту сборку осуществляет компилятор, а не программист. вот и вся разница.
А кто в языке с динамической типизацией осуществляет проверку, что вещи вне этого списка не придут, и кто отличает String как Real от String как String?
На практике я бы считал приближённо и в интервальной арифметике — всё равно все данные с погрешностями. А там уже и формулы расслабить можно, и полегче будет.
Но, опять же, я ничего не знаю о предметной области.
А ассоциативный контейнер — это сущность, принципиально непостижимая кем?
Это на самом деле тоже раздражает, но между кастомным рендерером в редакторе (что заодно привязывает меня к редактору — вряд ли nvim так же умеет) и ограничением в индексах я скорее выберу второе.
Можно сюда добавлять всякое по желанию.
Ну или у меня самописный плагин для nvim'а — там тоже просто в файл добавляешь новые сочетания, и всё.
«Монада» — это просто такой интерфейс, удовлетворяющий определённым законам, как «ассоциативный контейнер» или «итератор». Зачем человека сразу теоркатом грузить?
Ну хз. Шрифты с закорючками всё равно нужны (а то как их редактор рисует-то?), аккорды вводить всё равно нужно (просто они не автозаменяются на уникодные символы), но при этом вне редактора (на гитхабе, например) приходётся читать неформатированный латех. По-моему, это строго нелучше и по некоторым аспектам хуже.
Можно добавлять нужные, но отсутствующие в ваш редактор! Агде ж всё равно, она любой уникод жрёт.
Нет, конечно. Просто альтернативы ещё хуже.
А говорить, что (разовая, имеющая константную сложность) подготовка окружения к работе с каким-то инструментом — это недостаток инструмента, очень странно. Тогда все инструменты отстой и не готовы для бизнеса, потому что для всех инструментов нужно готовиться. Даже для программирования в машинных кодах надо хекс-редактор поставить.
Ну либо остаться на машинах, где весь интерфейс сводился к тумблерам на передней панели — там ничего ставить и готовиться не надо, идеальные машины, только бизнес тупой и слез с них почему-то.
Ненормальный способ их вводить — это, условно, тыкать по экранной клавиатуре. Я не вижу существенных проблем с упомянутым выше способом, когда равенство из трёх горизонтальных палочек — это просто два знака равно подряд.
Слои на эргодоксе — ещё удобнее. Для определённой задачи определённые инструменты повышают удобство ⇒ я покупаю этот инструмент и овладеваю им. А с вашей точки зрения ни один бизнес никогда бы не завязался на аппсторы и производство приложений для них, потому что там нужно купить макбук (сильно дороже эргодокса) и получить полный вендорлок на конкретную экосистемы.
А способов ввода текстов в пяти измерениях нет вообще, никаких.
ХЗ, у меня с fira code всё работает.
А вот код на go, например, у меня тоже не заведётся за отсутствием компилятора go.
Ну вот оказывается, что во всех языках, которые претендуют на хотя бы возможность формализации таких вещей и которые при этом успешны на этом поприще, есть возможность (и культура) работы с закорючками, кастомные миксфиксные операторы (вот эти все трёх-четырёх-пятиместные штуки с подчёркиваниями), и так далее. Много разных людей думало и не придумало ничего лучше.
У всех аналогий есть границы применимости, и у этой тоже.
Когда настоящего сишника это останавливало?
Но вообще записать что-то в младший битик указателя, а потом вернуть всё обратно перед использованием — вроде как не UB. С pointer provenance ерунда будет, вероятно, но у меня есть чувство, что pointer provenance не понимает даже Комитет.
Ширину строк в кодстайле/линтере сделали такой, чтобы side-by-side-дифф влезал на экран? Или, может, удобство работы с мобильника не является ключевым фактором для кодингового окружения?
У меня были работы, где весь кодинг шёл через RDP на серверах где-то там, для доступа к чему надо было приложить палец к yubikey, вставленному в usb-порт. Код (и ревью, и прочее) у меня с мобилы не открывался вообще никак, ни квадратиками, ни вопросиками. Я правильно понимаю, что RDP — непригодная технология, и никакой бизнес на неё завязываться не будет?
Но это риторические вопросы. Нериторический, серьёзный вопрос другой: какая альтернатива? Как бы вы написали выражение выше, чтобы без закорючек?
А вы с телефона пишете код или проводите ревью?
Заодно там ширину строк под телефон (учитывая засилье вертикальных видео — в вертикальной ориентации) адаптировать не нужно?
Не максимализм, а демонстрация, что слова про реальный мир — это не аргумент, потому что им мы приходим к очевидно бредовым выводам.
Пойду расскажу об этом бизнесам, которые за агду платили.
Подобный костыльный short-circuiting есть во всех¹ императивных языках, и подобная разница есть везде¹, где есть заодно и битовые операторы. Плюс, он действительно костыльный: например, в плюсах
&&коротит только для встроенных типов, и свои short-circuiting-операторы вы определять не можете нигде¹.¹ из тех языков, про которые я хоть что-то достаточно знаю, конечно
Я мог бы написать
(bool)str, суть это меняет не сильно.Но вообще затем, зачем над указателями вообще делать битовую арифметику: чтобы в младших (или старших) битиках там что-нибудь хранить. Во всяких локфри бывает полезно, да и вообще память экономит, так как указатели выровнены, и эти битики пропадают (а старшие на x86_64 не используются).
Не нашёл ни одной, потому что написано то, что я и так хотел сказать.
Код пишется один раз, а читается много раз. Куда удобнее читать код, в котором не используются (визуальные) многозначковые комбинации или, чего хуже, слова, для тех вещей, для которых в предметной области есть устоявшаяся нотация.
У вас есть код
где используются кастомные операторы и функции-закорючки, в порядке их появления — трёхместный
_⊢[_]_(_обозначает, куда идёт аргумент) и бинарный_⇒_на первой строке; четырёхместный_⊢[_]_⦂_и бинарный_,_во второй строке, и бинарныйƛв третьей. Как бы вы написали это обычными словами, чтобы это можно было прочитать?Одна из причин мне использовать эргодокс со слоями. Греческие буквы и наиболее частые символы я повесил на отдельные слои.
Поточечное пропозициональное равенство двух функций.
Ох уж этот реальный мир и отсылки к нему, когда по реальным миром каждый понимает что-то своё.
в риальном мире так та и матиматика ненужна, и вуз, и дажи старшые классы школы. чаивые калькулятар пащитает, а граматнаст тоже ненужна ведь вы этоттекст тоже можите прачитать и панять што яимел ввиду
Как в C отличается порядок выполнения
str && str[0] == 'a'противstr & str[0] == 'a'?Agda это успешно решает вводом закорючек через аккорды. Например, ≡ — это \==, а ≗ — \circeq.
В агде это тоже решается: люди вполне успешно описывают эти значочки терминами из предметной области, например.
И это.
Да норм:
Пользователю важно, что там есть тесты? Нет. Менеджменту и бизнесу важно, что там есть тесты? Нет.
Тесты ничего не добавляют, только вынуждают раздувать код в восемь и шесть седьмых раз, чтобы добавить все нужные моки, интерфейсы, SOLID и DI. Вы знаете, что в Штатах сейчас вообще правительство DEI запретило? Это просто хотели запретить DI из-за феерического разбазаривания ресурсов на пять экранов кода на каждую функцию, но просто когда печатали текст указа, то случайно вместе с D нажали на кнопку над ней (и тесты это не поймали, обратите внимание — толку с них?).
Топ-левел-байндинги легче читать с аннотациями, нетривиальные функции легче читать с аннотациями, простые вещи и локальные переменные легче читать без аннотаций.
У вас тезис уровня «вы определитесь, или говорящие имена переменных, или
iкак индекс массива».Откуда удвоение-то?
Кто запрещает? Почему?
В чём мучение?
Мутабельность к этому не имеет вообще никакого отношения.
И там, где это важно, это пытаются минимизировать. Вы же даже не пытаетесь это сделать, а ставите те эксперименты, которые легче поставить (напихать трейсов и потом с умным видом сидеть их разглядывать), а не те, которые относятся к вашему предмету исследования (почему тормозит).
Абсолютно верно, без типов этой проблемы нет.
Вы даже сами сказали, «этот тип». Тип один, всё.
Обычная индукция/рекурсия, не вижу проблем.
Если это не часть семантики yaml, то это они зря, конечно. Но это вопрос конкретной реализации, а не теории типов.
Да, и? Вы думаете, тут цель — выпендриться и иметь в рантайме какое-то другое представление (что, кстати, делают с GADT'ами, но вы ещё не там)? Тут цель — это проверки в компилтайме, до запуска.
Какие проблемы возникают?
Эта отсылка была к тому, что ПО с дебагами и прочими трейсами ведёт себя совсем не так, как без них.
Попробуйте в следующий раз дочитывать комментарии до конца. Или хрен с ними с комментариями, фразы-то до конца дочитывайте.
А использовали бы типы — не было бы такой ерунды у вас, как вы описываете.
Нет, конечно. Она всё ещё обрабатывает ровно один тип.
А кто в языке с динамической типизацией осуществляет проверку, что вещи вне этого списка не придут, и кто отличает String как Real от String как String?
Лол ок.
На практике я бы считал приближённо и в интервальной арифметике — всё равно все данные с погрешностями. А там уже и формулы расслабить можно, и полегче будет.
Но, опять же, я ничего не знаю о предметной области.