Тройка (A×B, π₁, π₂) называется прямым произведением A и B, если для любого объекта C и любых морфизмов f : C → A и g : C → B существует единственный морфизм u : C → A×B, что u π₁ = f и u π₂ = g.
Я бы предложил следующую интерпретацию: если на f и на g смотреть как на элементы из A и B, параметризованные параметром типа C (который может быть временем, конфигом, состоянием среды и т.п.), то они вместе образую пару u, которая есть элемент A×B с той же параметризацией. С одной стороны, любые два объекта f и g мы можем спарить в u. С другой стороны, имея u, мы можем восстановить f и g по формуле. А единственность гарантирует (и, собственно, означает), что кроме f и g объект u не содержит в себе ничего постороннего.
С одной стороны, наличие Any/Dyn делает систему типов как логическую систему противоречивой, поскольку возможно населить любой тип данных.
С другой стороны, постепенная типизация нужна для того, чтобы аккуратно согласовывать совместную разработку нетипизированной (= без формализованных утверждений о свойствах данных) и типизированной (= с концептуальной моделью, отраженной в определённых типах) подсистемы в рамках одной вычислительной системы.
Интерпретируя это в терминах логики, это как условная семья, где условный муж рассуждает формально и логически в рамках непротиворечивой логики, а условная жена использует противоречивую логику в своих рассуждениях. Цель здесь не сделать мужа носителем женской логики, а предложить единую среду, которая позволила бы аккуратно переходить от одной системы к другой, не умаляя достоинств каждой из них.
Лично я считаю, что непротиворечивость (soundness) понимается слишком строго. Вариант Soundness + Developer-Friendly описан как согласованность статической (которая проверяется до запуска) типизации и динамических (которые проверяются во время работы) контрактов, хотя механизм контрактов является плюс-минус независимым механизмом (Грис «Наука программирования», Хоар, Финдлер и пр.), который может в какой-то степени соотноситься с семантикой той или иной системы типов (doi:10.1145/3022670.2951930, doi:10.1016/j.procs.2018.11.069 или по-русски)
О blame как частной задачи отладки
Между тем, маленький оффтоп, Вадлеровский blame и git blame решают в сущности одну задачу — поиск причины, по которой возникла несогласованность, причём причина может лежать в коде, который в своём контексте (контракт на входные данные, коммит) выглядит безобидно и согласованно. По моему мнению эта задача является подзадачей глобальной задачи отладки и методы решения должны быть универсальными с точки зрения теоретической проработки, подобно тому, как есть теория конструкций языков программирования, теория структур данных, теория концептуального моделирования и т.п. Я не знаю, что на этот счёт уже придумано.
Для чистых ФП языков можно, например, хранить последовательность преобразований термов, для каждого указывать редекс и действующее на него трансформационное правило. Это похоже на журнал (логирование), но с возможностью пускать вычисления от любой точки по другому пути (выбором другого редекса), чтобы путь движения интересующего вычисляемого объекта был нагляднее.
Впрочем, сделав такое, мы напрочь отключаем сборщик мусора и прощай-прощай память.
Что такое Developer-Friendly
В работе doi:10.1145/3708981 предлагается метод «Рациональный программист» для оценки уровня Developer-Friendly. Это к вопросу автора о том, как можно формализовать этот аспект.
Все предыдущие комментарии содержали вопрос, зачем вообще нужна последовательная типизация. Нужна она не для того, чтобы один программист мог в рамках одного фрагмента своего кода свободно переключаться между «тут я хочу строгости и гарантий» и «тут я художник, я так вижу». Одна из причин названа @Ciyoxe: переписывание нетипизированного легаси, попутно добавляя типы. А ещё она нужна для сопряжения нетипизированного кода, который уже написан и, возможно, будет меняться в будущем, за который наш лирический программист не отвечает, и типизированного кода, который наш программист желает писать по уму.
Пример такой ситуации: как использовать JavaScript-пакеты из репозитория npm в типизированных проектах, которые компилируются в JS и исполняются в браузере? Очевидно, типизированный язык программирования должен предлагать средства для сопряжения нетипизированного кода библиотеки и типизированного кода самой программы. Причём далеко не всегда все импортируемые функции можно адекватно типизировать средствами самого языка.
Кстати, проблему можно распространить на более широкий класс: как переиспользовать код на языке с более «плохой» системой типов в проекте, который написан на более «хорошей» системе типов? Собственно, эта задача и решается постепенной типизацией.
А надо бы учить сразу и на человеческом тексте и на lean, чтобы языковые модели имели внутри себя этот язык. В результате получится объединить мощь ИИ для эвристического поиска и строгую проверку компилятором lean (или иной системой символьных вычислений) для верификации выдачи и организации обратной связи для нейросети.
Сейчас как раз пытаются это сделать. Там проблема в том, что корпус математических текстов написан недостаточно формально, а корпус формальных доказательств пока что покрывает мизерную долю математических «знаний».
Проблема ещё в том, что он не знает куда кидать ошибку
Автор пишет:
Несмотря на наличие в проекте большого количества примеров того, как должны быть написаны юнит-тесты,
значит, в контексте агента есть множество стереотипных примеров, куда кидать ошибку, а он их проигнорировал. Кстати, раньше мне казалось, что LLM должны хорошо справляться с написанием по образцу. Получается, он работать умеет только по подробной спецификации?
Это, конечно, всё очень интересно. И картиночки залипательные.
Но разве это не обычные сопряжения, которых в черчении пруд пруди? Неужели разработчики топовых градостроительных симуляторов не могут базовые функции САПР завезти? Или могут, но это им не нужно?
Палец — недалеко, остальная же часть владельца — не факт.
А если серьёзно, то телефон не всегда находится недалеко. Начиная от банальных краж. А при моём вялом взаимодействии с ним вообще могу обнаружить пропажу через неделю.
То есть (в контексте выдвигаемых в статье тезисов) мы соглашаемся с тем, что настоящие причины неудобств паролей для грамотных пользователей в неадекватных требованиях со стороны сайтов и сервисов с одной стороны?
Кстати, менеджер паролей — это альтернативный вариант управления паролями для тех, кто не доверяет своей памяти. Что всё так же в большинстве случаев лучше, чем другие рассмотренные в статье факторы.
З.Ы. а секретные вопросы — вообще боль, особенно когда их список задан жёстко сервисом. Кто в здравом уме будет ответом на секретный вопрос «Девичья фамилия матери» указывать реальную девичью фамилию матери?
Спуститься туда можно будет не только по лестнице, но и из мужских душевых на первом этаже.
Без шуток, если бы сразу спроектировали переход из бездны ада душевых до любого корпуса, перемещение было бы кратно менее напряжным половину всего года. И, что весьма важно, потребность в гардеробе отпала бы сама собой.
В целом, сложно будет из-за разрыва в степени абстракции. Но давайте такой пример рассмотрим. Сразу предупреждаю, что в нём категория будет работать как обычное отношение порядка.
Пусть R — множество всех ресурсов (имён файлов, node id и т.п.), которые потенциально могут существовать. Построим категорию порядка Ord(R), где объекты A — это какие-то множества каких-то ресурсов из R (A — подмножество R), морфизм f: A → A' — это пара (A,A'), в которой A — подмножество A'. Композиция тривиальная. Исследуем эту категорию: терминальный объект — это R, инициальный — пустое множество, произведение — это пересечение, сумма — объединение.
Теперь пусть G — множество всех групп, к которым может принадлежать ресурс. Построим такую же категорию Ord(G), в которой объекты U — это множества некоторых групп, морфизмы — это (U,U'), что U < U'. Композиция тривиальна. Рассмотрим любой функтор F: Ord(G) → Ord(R). Функториальность гласит: если множество групп U входит во множество групп U', то соответствующее ей множество ресурсов F(U) будет входить как подмножество в F(U'), что полностью соответствует нашей интуиции: чем больше групп пользователю даны, тем больше ресурсов ему доступно. В общем случае не следует считать, что F(U + U') = F(U) + F(U'), но всегда F(U + U') включает в себя F(U) + F(U'), это доказывается непосредственно по определению суммы F(U) + F(U').
Итак, мы рассмотрели две категории порядка, одна из которых формализует «множество доступных ресурсов», а другая — «множество групп, на которые абстрактный пользователь имеет права», рассмотрели простейшие пределы в этих категориях. Любой функтор между ними устанавливает соответствие — интерпретацию групп и их сочетаний как множество ресурсов. Функториальность интерпретируется как требование, чтобы реализуемая политика доступа увеличивала (не уменьшала) множество доступных ресурсов при увеличении прав.
Пример понятен?
вроде можно назвать категорией
Понятие категории настолько пермиссивное, что всегда (с точностью до погрешности) слово «вроде» можно убрать: если что-то похоже на категорию, то оно является категорией. Другой вопрос — какие там морфизмы и композиция, они самые важные, в них проявляются все категорные свойства.
Практических примеров навалом даже здесь на Хабре. Только они конкретные, без лишних абстракций, а потому, прочитав их, можно не узнать ТК.
Умозрительный пример. Допустим, мы разрабатываем собственную систему прав для авторизованного доступа пользователей к ресурсам. Мы решаем, что у каждого пользователя есть какая-то назначенная метаинформация о его правах (тип U), и у каждого ресурса есть то же самое (тип R). С точки зрения ресурса все пользователи делятся на две группы (кто имеет право или нет).
На U можно ввести порядок: для некоторых u1, u2 можно сказать, что всё, что разрешено u1, разрешено и u2. Это категория. Возникают автоматически два крайних режима: «всё запрещено» и «всё разрешено» — инициальный и терминальный объекты. Возникают автоматически операции над правами: если u и v — два возможных набора прав, то u×v — их пересечение (можно только то, что позволяют u и v одновременно), и u+v — объединение (можно то, что позволяет u, и то, что позволяет v).
А потом мы решаем учесть, что права пользователя не навсегда дают доступ, но к некоторым ресурсам требуется дополнительно ввести пароль, а к некоторым — код из СМС. Меняем категорию: теперь морфизмы несут информацию о дополнительных действиях, факт осуществления которых на время изменяет права. Кстати, процедура авторизации может быть представлена морфизмом из инициального объекта («всё запрещено») в получаемые права u. Теперь в категории между двумя объектами может быть несколько морфизмов (напр., повышение прав за счёт ввода пароль или кода из СМС). Композицию тоже можно сделать нетривиальной, чтобы отразить логику работы с паролями. Теперь прямое произведение u×v не только гарантирует, что разрешено только то, что u и v разрешают одновременно, но и гарантируется, что обретение таких прав требует «разумного» (с точки зрения выбранной категории) сочетания действий, необходимых для обретения прав u и v.
По моему опыту писания на Идрисе (а не прохождения собеседования) вариант, предложенный в разделе «Как не надо» самый правильный, если затем предвидится хотя бы малейшая вероятность, что о функции надо будет что-нибудь доказывать, например, самообратность. В целом, я пришел к выводу, что принцип «преждевременная оптимизация — зло» здесь работает в самой острой форме.
Зато если нужно получить шуструю функцию, которая не отжирает всю память, то лучше писать так, как в Haskell принято. Но там с доказательствами всё по-сложнее будет. Например, вытеснение пропозициональными равенствами обычных и удобных равенств по определению.
всегда когда ты настрадал какой-то опыт, то очень сложно наблюдать как другие идут не таким же путем, особенно если делают это на порядок легче в силу технологий или других обстоятельств. Ты как бы становишься лузером и они обесценивают тебя
Золотые слова. А примеры — нет.
Мой почерк улучшился после того, как я научился писать пером. Может, это ошибка выжившего. Но я плохо представляю, как можно развить трёхмерную моторику и управление нажимом, если инструмент скрывает эту компоненту; и как можно понять анатомию букв, если подходить с позиции «лишь бы что-то похожее на палочку получилось, а там поймут». Можно ли с шариковой ручкой достичь тех же результатов? Да можно, но сложнее (ИМХО).
IDE — это помощник. Она упрощает типовые действия. Если программист умеет программировать, то он и с IDE, и без неё напишет программу, разница только в затраченном времени. А если человек не может без IDE (но с доками и нормальным компилятором) два слова связать, то это странно как-то. Есть ли корреляция между использованием IDE в процессе обучения и эффективностью обучения, и какая она? Мне не очевиден ответ. Если есть исследования, хотелось бы посмотреть.
Благодарю за детальный ответ. Я сам сейчас в поисках материалов для «юного дизайнера», причём русскоязычного. На ютубе полно разных видео, но их поди найди. Есть каталог уроков на ютубе, но он только по Inkscape. На других площадках разнообразие и качество уроков сильно уступает ютубу.
В целом, описанная Вами ситуация понятна.
P.S. если будут легко разворачиваемые локально сервисы, вроде описанных выше, станет легче.
Небольшой оффтоп: есть какая-то специфика по содержанию этих видео? Например, хорошая методическая проработка или специализация по решаемым прикладным задачам? Для выбранной цели не окажется ли, что есть русскоязычные материалы, языковая доступность которых покрывает содержательное преимущество иноязычных? Или это собирается для личных целей исходя из личных хаотичных предпочтений.
Увы, но нет. По крайней мере, не прямолинейным образом.
Во-первых, logprobs не дают существенной информации о том, насколько данный кусок сама модель считает сомнительным. На то несколько причин: 1) вероятность понижается при наличии нескольких равнозначных способов сказать одно и то же. Впрочем, интересный противоположный случай: когда вероятность под 100% и, соответственно, энтропия низкая, модель как бы говорит «зуб даю — только так и не иначе». 2) вероятность может размазываться между словами. Сравни: распределение одного токена «мой» и распределение каждого по отдельности токена в «при-над-леж-ащий мне». Поэтому надо сравнивать полную вероятность семантически эквивалентных единиц текста. А как их выделять?
Во-вторых, эти сведения мы можем использовать только для оценки того, в каких местах модель могла бы ответить иначе. Так сказать, оценить потенциальные «точки бифуркации». При этом, как аргументировал предыдущий оратор, она сама не способна оценить соответствие реальности, потому что у неё нет встроенной эталонной (хотя бы частичной) модели реальности.
1) Объединение используется, как правило, в неявных (т.е. по Карри) системах типизации.
В теории типов они успешно изучаются, ищите по фразе «type intersection». Напр., Bono et al. «A typed lambda calculus with intersection types» (2008).
Ощущение, что в программировании оно чаще встречается, видимо, связано с нем, что традиционное программирование «помнит» о том, что в конечном счёте все структуры данных будут представлены байтами и, следовательно, любой тип в конечном счёте есть подмножество битовых слов. Это сближает с неявной типизацией. Например, TypeScript исходит из того, что любой типизированный объект — это объект JavaScript, а следовательно, тип — это «как бы» множество объектов. Отсюда проистекает использование объединений вместо сумм, как мне кажется.
2) Задача механизма проверки согласованности типов (англ. typechecker, не знаю хорошего русского перевода) — проверить, что существует вывод (доказательство) того, что код всей программы имеет тип, который должен быть у кода программы. Почти во всех системах типов это означает вывод типов для всех выражений на всех уровнях.
В явных системах указываются точные типы аргументов и результата и механизм проверки согласованности типов должен только лишь проверить, что указанный тип результата совпадает с тем, который должен быть по соответствующему правилу вывода типов.
В прикладных языках не все типы указываются, а поэтому механизм должен сперва восстановить все недостающие (не указанные) типы. Например, определить наиболее узкий тип по входным типам. Впрочем, есть замечательный принцип де Брёйна: typechecker должен внутри себя содержать минималистичное ядро, задача которого — только проверять согласованность, но ничего не выводить.
3) Вопрос плохо поставлен. Систем типизации много. Для каждой есть свой «близкий» ЯП. Тот же Haskell без расширений — хорошая реализация Хиндли-Милнера. На всякий случай оставлю список языков с более развитыми системами типов: Koka, Coq, Lean, Agda, Idris.
Безотносительно вашего многолетнего противостояния, хочу заметить, что меня тоже возмутила подача материала в статье по некоторым вопросам (собственно, по h2-section и по for-label).
Если стандарт требует, чтобы семантическая разметка была такой-то (скажем, чтобы label шел перед input), то и аргументация должна звучать как «это требуется стандартом и точка» без упоминания того, как там скринридеры или иные браузеры себя ведут или не ведут. Если же стандарт говорит «section должен содержать заголовок» и он содержит, а скинридеры его не умеют подвязывать, то это ошибка разработчиков скринридера и пусть их поносят пострадавшие, доколе не исправят.
Это мне напоминает времена, когда стандарты уже приняты, но MS и некоторые другие браузеры привносили отсебятину. Некоторые сайты на неё опирались. Эти сайты не открывались в нормальных браузерах, которые действовали по стандарту. Кого винили простые пользователи? Браузер, в котором сайт не работает, а не сайт, написанный альтернативно-одарёнными разработчиками, не умеющими в стандарт. Это не нормальная ситуация. И сейчас подобному потакать тоже не следует.
По моему мнению, там вообще неаккуратно написано.
Тройка (A×B, π₁, π₂) называется прямым произведением A и B, если для любого объекта C и любых морфизмов f : C → A и g : C → B существует единственный морфизм u : C → A×B, что u π₁ = f и u π₂ = g.
Я бы предложил следующую интерпретацию: если на f и на g смотреть как на элементы из A и B, параметризованные параметром типа C (который может быть временем, конфигом, состоянием среды и т.п.), то они вместе образую пару u, которая есть элемент A×B с той же параметризацией. С одной стороны, любые два объекта f и g мы можем спарить в u. С другой стороны, имея u, мы можем восстановить f и g по формуле. А единственность гарантирует (и, собственно, означает), что кроме f и g объект u не содержит в себе ничего постороннего.
С одной стороны, наличие Any/Dyn делает систему типов как логическую систему противоречивой, поскольку возможно населить любой тип данных.
С другой стороны, постепенная типизация нужна для того, чтобы аккуратно согласовывать совместную разработку нетипизированной (= без формализованных утверждений о свойствах данных) и типизированной (= с концептуальной моделью, отраженной в определённых типах) подсистемы в рамках одной вычислительной системы.
Интерпретируя это в терминах логики, это как условная семья, где условный муж рассуждает формально и логически в рамках непротиворечивой логики, а условная жена использует противоречивую логику в своих рассуждениях. Цель здесь не сделать мужа носителем женской логики, а предложить единую среду, которая позволила бы аккуратно переходить от одной системы к другой, не умаляя достоинств каждой из них.
Добротная статья.
Лично я считаю, что непротиворечивость (soundness) понимается слишком строго. Вариант Soundness + Developer-Friendly описан как согласованность статической (которая проверяется до запуска) типизации и динамических (которые проверяются во время работы) контрактов, хотя механизм контрактов является плюс-минус независимым механизмом (Грис «Наука программирования», Хоар, Финдлер и пр.), который может в какой-то степени соотноситься с семантикой той или иной системы типов (doi:10.1145/3022670.2951930, doi:10.1016/j.procs.2018.11.069 или по-русски)
О blame как частной задачи отладки
Между тем, маленький оффтоп, Вадлеровский blame и git blame решают в сущности одну задачу — поиск причины, по которой возникла несогласованность, причём причина может лежать в коде, который в своём контексте (контракт на входные данные, коммит) выглядит безобидно и согласованно. По моему мнению эта задача является подзадачей глобальной задачи отладки и методы решения должны быть универсальными с точки зрения теоретической проработки, подобно тому, как есть теория конструкций языков программирования, теория структур данных, теория концептуального моделирования и т.п. Я не знаю, что на этот счёт уже придумано.
Для чистых ФП языков можно, например, хранить последовательность преобразований термов, для каждого указывать редекс и действующее на него трансформационное правило. Это похоже на журнал (логирование), но с возможностью пускать вычисления от любой точки по другому пути (выбором другого редекса), чтобы путь движения интересующего вычисляемого объекта был нагляднее.
Впрочем, сделав такое, мы напрочь отключаем сборщик мусора и прощай-прощай память.
Что такое Developer-Friendly
В работе doi:10.1145/3708981 предлагается метод «Рациональный программист» для оценки уровня Developer-Friendly. Это к вопросу автора о том, как можно формализовать этот аспект.
Все предыдущие комментарии содержали вопрос, зачем вообще нужна последовательная типизация. Нужна она не для того, чтобы один программист мог в рамках одного фрагмента своего кода свободно переключаться между «тут я хочу строгости и гарантий» и «тут я художник, я так вижу». Одна из причин названа @Ciyoxe: переписывание нетипизированного легаси, попутно добавляя типы. А ещё она нужна для сопряжения нетипизированного кода, который уже написан и, возможно, будет меняться в будущем, за который наш лирический программист не отвечает, и типизированного кода, который наш программист желает писать по уму.
Пример такой ситуации: как использовать JavaScript-пакеты из репозитория npm в типизированных проектах, которые компилируются в JS и исполняются в браузере? Очевидно, типизированный язык программирования должен предлагать средства для сопряжения нетипизированного кода библиотеки и типизированного кода самой программы. Причём далеко не всегда все импортируемые функции можно адекватно типизировать средствами самого языка.
Кстати, проблему можно распространить на более широкий класс: как переиспользовать код на языке с более «плохой» системой типов в проекте, который написан на более «хорошей» системе типов? Собственно, эта задача и решается постепенной типизацией.
Сейчас как раз пытаются это сделать. Там проблема в том, что корпус математических текстов написан недостаточно формально, а корпус формальных доказательств пока что покрывает мизерную долю математических «знаний».
Не вайбкодер, но считаю эту аргументацию шаткой.
Это написано в документации к методу.
Автор пишет:
значит, в контексте агента есть множество стереотипных примеров, куда кидать ошибку, а он их проигнорировал. Кстати, раньше мне казалось, что LLM должны хорошо справляться с написанием по образцу. Получается, он работать умеет только по подробной спецификации?
Это, конечно, всё очень интересно. И картиночки залипательные.
Но разве это не обычные сопряжения, которых в черчении пруд пруди? Неужели разработчики топовых градостроительных симуляторов не могут базовые функции САПР завезти? Или могут, но это им не нужно?
Палец — недалеко, остальная же часть владельца — не факт.
А если серьёзно, то телефон не всегда находится недалеко. Начиная от банальных краж. А при моём вялом взаимодействии с ним вообще могу обнаружить пропажу через неделю.
То есть (в контексте выдвигаемых в статье тезисов) мы соглашаемся с тем, что настоящие причины неудобств паролей для грамотных пользователей в неадекватных требованиях со стороны сайтов и сервисов с одной стороны?
Кстати, менеджер паролей — это альтернативный вариант управления паролями для тех, кто не доверяет своей памяти. Что всё так же в большинстве случаев лучше, чем другие рассмотренные в статье факторы.
З.Ы. а секретные вопросы — вообще боль, особенно когда их список задан жёстко сервисом. Кто в здравом уме будет ответом на секретный вопрос «Девичья фамилия матери» указывать реальную девичью фамилию матери?
Без шуток, если бы сразу спроектировали переход из
бездны ададушевых до любого корпуса, перемещение было бы кратно менее напряжным половину всего года. И, что весьма важно, потребность в гардеробе отпала бы сама собой.Я подумал, что речь пойдёт о механике safe pocket, только в мышах.
В целом, сложно будет из-за разрыва в степени абстракции. Но давайте такой пример рассмотрим. Сразу предупреждаю, что в нём категория будет работать как обычное отношение порядка.
Пусть R — множество всех ресурсов (имён файлов, node id и т.п.), которые потенциально могут существовать. Построим категорию порядка Ord(R), где объекты A — это какие-то множества каких-то ресурсов из R (A — подмножество R), морфизм f: A → A' — это пара (A,A'), в которой A — подмножество A'. Композиция тривиальная. Исследуем эту категорию:
терминальный объект — это R,
инициальный — пустое множество,
произведение — это пересечение,
сумма — объединение.
Теперь пусть G — множество всех групп, к которым может принадлежать ресурс. Построим такую же категорию Ord(G), в которой объекты U — это множества некоторых групп, морфизмы — это (U,U'), что U < U'. Композиция тривиальна. Рассмотрим любой функтор F: Ord(G) → Ord(R). Функториальность гласит: если множество групп U входит во множество групп U', то соответствующее ей множество ресурсов F(U) будет входить как подмножество в F(U'), что полностью соответствует нашей интуиции: чем больше групп пользователю даны, тем больше ресурсов ему доступно. В общем случае не следует считать, что F(U + U') = F(U) + F(U'), но всегда F(U + U') включает в себя F(U) + F(U'), это доказывается непосредственно по определению суммы F(U) + F(U').
Итак, мы рассмотрели две категории порядка, одна из которых формализует «множество доступных ресурсов», а другая — «множество групп, на которые абстрактный пользователь имеет права», рассмотрели простейшие пределы в этих категориях. Любой функтор между ними устанавливает соответствие — интерпретацию групп и их сочетаний как множество ресурсов. Функториальность интерпретируется как требование, чтобы реализуемая политика доступа увеличивала (не уменьшала) множество доступных ресурсов при увеличении прав.
Пример понятен?
Понятие категории настолько пермиссивное, что всегда (с точностью до погрешности) слово «вроде» можно убрать: если что-то похоже на категорию, то оно является категорией. Другой вопрос — какие там морфизмы и композиция, они самые важные, в них проявляются все категорные свойства.
Практических примеров навалом даже здесь на Хабре. Только они конкретные, без лишних абстракций, а потому, прочитав их, можно не узнать ТК.
Умозрительный пример. Допустим, мы разрабатываем собственную систему прав для авторизованного доступа пользователей к ресурсам. Мы решаем, что у каждого пользователя есть какая-то назначенная метаинформация о его правах (тип U), и у каждого ресурса есть то же самое (тип R). С точки зрения ресурса все пользователи делятся на две группы (кто имеет право или нет).
На U можно ввести порядок: для некоторых u1, u2 можно сказать, что всё, что разрешено u1, разрешено и u2. Это категория. Возникают автоматически два крайних режима: «всё запрещено» и «всё разрешено» — инициальный и терминальный объекты. Возникают автоматически операции над правами: если u и v — два возможных набора прав, то u×v — их пересечение (можно только то, что позволяют u и v одновременно), и u+v — объединение (можно то, что позволяет u, и то, что позволяет v).
А потом мы решаем учесть, что права пользователя не навсегда дают доступ, но к некоторым ресурсам требуется дополнительно ввести пароль, а к некоторым — код из СМС. Меняем категорию: теперь морфизмы несут информацию о дополнительных действиях, факт осуществления которых на время изменяет права. Кстати, процедура авторизации может быть представлена морфизмом из инициального объекта («всё запрещено») в получаемые права u. Теперь в категории между двумя объектами может быть несколько морфизмов (напр., повышение прав за счёт ввода пароль или кода из СМС). Композицию тоже можно сделать нетривиальной, чтобы отразить логику работы с паролями. Теперь прямое произведение u×v не только гарантирует, что разрешено только то, что u и v разрешают одновременно, но и гарантируется, что обретение таких прав требует «разумного» (с точки зрения выбранной категории) сочетания действий, необходимых для обретения прав u и v.
По моему опыту писания на Идрисе (а не прохождения собеседования) вариант, предложенный в разделе «Как не надо» самый правильный, если затем предвидится хотя бы малейшая вероятность, что о функции надо будет что-нибудь доказывать, например, самообратность. В целом, я пришел к выводу, что принцип «преждевременная оптимизация — зло» здесь работает в самой острой форме.
Зато если нужно получить шуструю функцию, которая не отжирает всю память, то лучше писать так, как в Haskell принято. Но там с доказательствами всё по-сложнее будет. Например, вытеснение пропозициональными равенствами обычных и удобных равенств по определению.
Золотые слова. А примеры — нет.
Мой почерк улучшился после того, как я научился писать пером. Может, это ошибка выжившего. Но я плохо представляю, как можно развить трёхмерную моторику и управление нажимом, если инструмент скрывает эту компоненту; и как можно понять анатомию букв, если подходить с позиции «лишь бы что-то похожее на палочку получилось, а там поймут». Можно ли с шариковой ручкой достичь тех же результатов? Да можно, но сложнее (ИМХО).
IDE — это помощник. Она упрощает типовые действия. Если программист умеет программировать, то он и с IDE, и без неё напишет программу, разница только в затраченном времени. А если человек не может без IDE (но с доками и нормальным компилятором) два слова связать, то это странно как-то. Есть ли корреляция между использованием IDE в процессе обучения и эффективностью обучения, и какая она? Мне не очевиден ответ. Если есть исследования, хотелось бы посмотреть.
Благодарю за детальный ответ. Я сам сейчас в поисках материалов для «юного дизайнера», причём русскоязычного. На ютубе полно разных видео, но их поди найди. Есть каталог уроков на ютубе, но он только по Inkscape. На других площадках разнообразие и качество уроков сильно уступает ютубу.
В целом, описанная Вами ситуация понятна.
P.S. если будут легко разворачиваемые локально сервисы, вроде описанных выше, станет легче.
Небольшой оффтоп: есть какая-то специфика по содержанию этих видео? Например, хорошая методическая проработка или специализация по решаемым прикладным задачам? Для выбранной цели не окажется ли, что есть русскоязычные материалы, языковая доступность которых покрывает содержательное преимущество иноязычных? Или это собирается для личных целей исходя из личных хаотичных предпочтений.
Увы, но нет. По крайней мере, не прямолинейным образом.
Во-первых, logprobs не дают существенной информации о том, насколько данный кусок сама модель считает сомнительным. На то несколько причин:
1) вероятность понижается при наличии нескольких равнозначных способов сказать одно и то же. Впрочем, интересный противоположный случай: когда вероятность под 100% и, соответственно, энтропия низкая, модель как бы говорит «зуб даю — только так и не иначе».
2) вероятность может размазываться между словами. Сравни: распределение одного токена «мой» и распределение каждого по отдельности токена в «при-над-леж-ащий мне». Поэтому надо сравнивать полную вероятность семантически эквивалентных единиц текста. А как их выделять?
Во-вторых, эти сведения мы можем использовать только для оценки того, в каких местах модель могла бы ответить иначе. Так сказать, оценить потенциальные «точки бифуркации». При этом, как аргументировал предыдущий оратор, она сама не способна оценить соответствие реальности, потому что у неё нет встроенной эталонной (хотя бы частичной) модели реальности.
Не автор, но отвечу, как вижу.
1) Объединение используется, как правило, в неявных (т.е. по Карри) системах типизации.
В теории типов они успешно изучаются, ищите по фразе «type intersection». Напр., Bono et al. «A typed lambda calculus with intersection types» (2008).
Ощущение, что в программировании оно чаще встречается, видимо, связано с нем, что традиционное программирование «помнит» о том, что в конечном счёте все структуры данных будут представлены байтами и, следовательно, любой тип в конечном счёте есть подмножество битовых слов. Это сближает с неявной типизацией. Например, TypeScript исходит из того, что любой типизированный объект — это объект JavaScript, а следовательно, тип — это «как бы» множество объектов. Отсюда проистекает использование объединений вместо сумм, как мне кажется.
2) Задача механизма проверки согласованности типов (англ. typechecker, не знаю хорошего русского перевода) — проверить, что существует вывод (доказательство) того, что код всей программы имеет тип, который должен быть у кода программы. Почти во всех системах типов это означает вывод типов для всех выражений на всех уровнях.
В явных системах указываются точные типы аргументов и результата и механизм проверки согласованности типов должен только лишь проверить, что указанный тип результата совпадает с тем, который должен быть по соответствующему правилу вывода типов.
В прикладных языках не все типы указываются, а поэтому механизм должен сперва восстановить все недостающие (не указанные) типы. Например, определить наиболее узкий тип по входным типам. Впрочем, есть замечательный принцип де Брёйна: typechecker должен внутри себя содержать минималистичное ядро, задача которого — только проверять согласованность, но ничего не выводить.
3) Вопрос плохо поставлен. Систем типизации много. Для каждой есть свой «близкий» ЯП. Тот же Haskell без расширений — хорошая реализация Хиндли-Милнера. На всякий случай оставлю список языков с более развитыми системами типов: Koka, Coq, Lean, Agda, Idris.
Как то обычно бывает, нужен раздел с сопоставлениями с аналогами.
Предлагаю начать с такого: Лямбда-исчисление в 397 байтах. Тут автор не заботится о красивом представлении на метаязыке, зато размер поменьше будет.
Безотносительно вашего многолетнего противостояния, хочу заметить, что меня тоже возмутила подача материала в статье по некоторым вопросам (собственно, по h2-section и по for-label).
Если стандарт требует, чтобы семантическая разметка была такой-то (скажем, чтобы label шел перед input), то и аргументация должна звучать как «это требуется стандартом и точка» без упоминания того, как там скринридеры или иные браузеры себя ведут или не ведут. Если же стандарт говорит «section должен содержать заголовок» и он содержит, а скинридеры его не умеют подвязывать, то это ошибка разработчиков скринридера и пусть их поносят пострадавшие, доколе не исправят.
Это мне напоминает времена, когда стандарты уже приняты, но MS и некоторые другие браузеры привносили отсебятину. Некоторые сайты на неё опирались. Эти сайты не открывались в нормальных браузерах, которые действовали по стандарту. Кого винили простые пользователи? Браузер, в котором сайт не работает, а не сайт, написанный альтернативно-одарёнными разработчиками, не умеющими в стандарт. Это не нормальная ситуация. И сейчас подобному потакать тоже не следует.