Позвольте мне подушнить немного, потому что я тоже вижу среди некоторых сограждан поведение в отношении ИИ такое, каким бывает у других в отношении идолов, икон и прочих объектов почитания, которые мы с уверенностью называем религиозными.
Понятие религии очень плохо определено. Например, процитированное выше из Википедии (которой, как известно, доверять не стоит) не включает тотемизм и другие формы примитивной религии, не имеющие моральных норм или противопоставления естественного—сверхъестественного, а также едва ли включает буддизм. В самой Википедии (которой, как известно, доверять не стоит) проблема определения тоже рассматривается.
Процитирую первую после Википедии ссылку в поисковой выдаче, «Религиоведение» В. Лебедев, А. Прилуцкий, В. Викторов:
Сходным образом современный теолог и философ X. Р. Нибур понимает религию как веру в «иного–нежели–я–сам, который представляется людям скорее, когда они верят, чем когда они видят, слышат, осязают, даже скорее, чем когда они рассуждают. Принято говорить, что эта объективная реальность – Бог или боги – признается или познается в вере».
Подобная негативная оценка религии имеет в числе своих сторонников выдающегося евангелического протестантского теолога XX в. К. Барта. (...) согласно К. Барту, (...) религия – это придумывание бога человеком, дело сомневающегося человека.
Предложенное Э. Тайлором и породившее длительную дискуссию «минимальное определение религии» (т.е. характеризующее любую религию, универсальное) определяет религию как верование в духовные существа. Обобщая комментарии Э. Тайлора, французский социолог, один из основоположников социологии религии Э. Дюркгейм отмечает, что «под духовными существами следует понимать сознательных субъектов, наделенных силой высшей, чем та, которой обладает большинство людей»? это не только божества, но и души умерших, духи, демоны и т.д.
Я наблюдаю много сограждан, особенно вне IT, которые к ИИ относятся именно подобным образом, если сделать s/бог/ИИ/g.
</zanuda>
Вероятно, учёные, применившие ИИ для обнаружения 10000 белков, знают, что они делают и что они получили. Но в основном-то народ говорит иначе: «у них получилось для их задач, значит у нас точно(!) получится для наших», «если у нас не получилось, то проблема в нас, а не в ИИ», «наверное, вы просто недостаточно мощную модель/железо взяли — заплати и все проблемы будут решены». Критерий Поппера стоит в сторонке.
Задача состоит в том, чтобы на основе 3 документов составить один так, чтобы он содержал всю информацию, что содержится в первых двух документах, без повторов, компактно, с учётом того, что информация в третьем документе истинна и будущий читатель её знает. Дополнительная задача: обосновать соответствие полученного документа исходному заданию.
Непонятно, что значит игнорирует фрагменты документов в контексте данной задачи.
Вам дали задачу написать обзор на книгу. Вы берёте, вырываете случайные страницы клочками, что целые главы идут в топку, а только после этого садитесь её читать. Со вниманием, с усердием. Вот на что это похоже.
Не совсем понятно как длина контекста исправляет ненадежность верификации.
Я этого не говорил. Правда, я допускал, что кто-то может это сказать, мол, «докинь памяти побольше и будет тебе надёжность», к чему я отношусь скептически. Я же утверждаю, что если длина контекста с гулькин нос, но надёжности неоткуда взяться.
Каким образом осуществляется проверка (верификация) ответа, выданного сетью?
Покажу вопрос на примере, который был, когда я в последний раз пытался применить LLM.
Задача: соединить два подобных документа (скажем, две версии статьи по мотивам модуля) в один или переписать один документ в более компактном виде за счёт исключения повторений. При этом необходимо считать, что потенциальный читатель знает содержание некоторого третьего документа (скажем, список реализованных в модуле функций с их типами), чтобы 1) удалять то, что уже известно, 2) отождествлять то, что обычно не отождествляют.
Метод решения: просим LLM решить задачу, описывает ситуацию, добавляем все три документа, явно маркируя их границы, описываем выходной формат.
Проблема: бывает, что сетка игнорирует фрагменты документов (иногда фразы, иногда предложения, иногда разделы). Выходной результат неправильный.
Я пробовал использовать LLM для верификации, но столкнулся с двумя проблемами: или результат верификации ненадёжен, или требуется размер контекста больше, чем я могу предоставить (особенно если для верификации загружать и «рассуждения» первой сетки).
Пока не дочитал до конца, думал, что эта статья написана гопотой, потому что никто (кроме автора этой статьи) не будет вставлять код с неочевидным синтаксисом и не объяснять хотя бы в комментариях, что каждый синтаксический элемент означает и как надо думать, чтобы самому такое написать.
Выше имеется вполне хорошая дискуссия со сравнением этого языка с Агдой. Я тоже всуну свои пять копеек.
многие люди из академии больше сфокусированы на линейных и зависимых типах - горячие темы, которые легко продать сообществу. Но на мой дилетантский взгляд, это не сделает программирование более удобным занятием (...)
Развитые системы типов нужны для того, чтобы было сложнее сделать ошибку в логике программы. К удобству программирования это имеет слабое отношение, разве что кто-то скажет «как это удобно, когда компилятор не даёт мне писать код с ошибками типизации».
Плохо, что сейчас имеется мало исследований влияния дизайна языка программирования на его эргономику. Кажется, что это ровно то, чего автору не хватает в существующих языках. Впрочем, он и на своём языке не проверяет гипотезу о том, что кому-то на этом будет писать удобнее, чем на Haskell. Хнык.
По моему опыту ТК хорошо показывает себя в программировании в двух основных случаях:
(исследование) когда надо хорошо отработанную концептуальную систему перенести на другую область. Скажем, представления групп является частный случаем общего категорного метода, который подобные приёмы позволяет штамповать массово.
В частности, это позволяет оперировать известными понятиями и аналогиями (пространство, отображение, подпространство, произведение) без уточнения конкретики. Например,
в физике мы можем долго говорить о периодичной волновой функции и порождаемом ей расслоении на зоне Бриллюэна без уточнения, считаем ли мы её гладкой или дважды гладкой: в каждом случае мы просто говорим, что все упомянутые в рассуждении функции будут такими, какими мы хотим. Рассуждения становятся короткими, вся математическая лабуда про гладкость не упоминается, а выкладки не перестают быть формальными. При этом по рассуждениям чётко видно, какие минимальные требования на гладкость накладываются.
В программировании ТК позволяет нам корректно говорить о тех функциях, которыми мы программируем. Ведь если говорить по-честному, то, что мы привыкли называть функциями в программировании, имеет мало что общего с функциями в классической математике: 1) первые могут зацикливаться, а вторые всегда что-то возвращают; 2) первые с необходимостью задают алгоритм вычисления (даже в декларативных языках), вторые — нет; 3) первые имеют нефункциональные характеристики (затраты по времени и памяти), вторые — нет; 4) недетерминизм, работа с состоянием и прочие прелести во всех ЯП, кроме чистых функциональных. Тем не менее на практике мы склонные отождествлять эти понятия в одних случаях, и различать только тогда, когда вышеприведённые особенности проявляются. ТК легализует подобную (якобы) демагогию, переводя в статус аккуратно формализованной теории.
(обучение) когда надо спроектировать API, чтобы он воспринимался как естественный интерфейс. SQL тем хорош, что основывается на реляционном исчислении и реляционной алгебре: первое даёт метод решения широкого класса задач, выражаемых на языке первого порядка; второй позволяет быстро оценить, какие запросы эквивалентны. Обычно интерфейс, основанный на алгебраической системе, ощущается как более простой и обоснованный по сравнению с тем, который делает по велению левой пятки. ТК позволяет обобщить это на тот класс систем, API к которым в принципе не может выражаться простой алгебраической системой. В частности, ТК формализует рад полезных понятий:
функтор («структура данных», …)
естественное преобразование
терминальный и инициальный объекты (обычно имеют свои названия в разных предметных областях, вроде «атомарный X» или «пустой X»)
произведение и сумма
изоморфизм («равный с точностью до того, что нам не интересно»)
подобъект (подпространство, под-что-угодно)
универсальность (свободный функтор, сопряжения и т.п.)
Если проектируешь API и сумел достичь того, что большинство структур данных — функторы; большинство функций являются естественными преобразованиями; большинство объектов, с которыми пользователь будет работать, можно собрать из произведений, сумм, терминальных и инициальных объектов; все или почти все функции «уважают» изоморфизмы; все требования состоят в коммутативности некоторых диаграмм, — если всё это есть, то, вероятно, это прекрасный API, который не подложит свинью в неожиданный момент. Пользователь будет воспринимать этот интерфейс как естественный и, в идеале, как единственно возможный и обоснованный.
Я написал «по-маркетологски», но идея тут простая: API должен быть простым и обоснованным. Алгебры — это просто и обоснованно. Категории — это (для пользователя) просто и обоснованно. Для разработчика категории сложнее, ибо теория серьёзнее, но универсальнее.
А чисто посчитать что-то категории не нужны. Подобно типизации и тестированию, ТК не нужен, чтобы собственно считать, но занимают определённое место в проектировании и сопровождении программного продукта.
Насколько я понял, это перевод не от автора. Но вопросы есть.
Как может такой мощный язык, который практически является прикладной теорией категорий, не быть ЛУЧШИМ языком для категоризации строк на два класса эквивалентности
Это как? Какое отношение теории категорий имеет к задаче категоризации? Или это как с теорией групп, которая нужна для группировки вкладок в браузере, а теория полей — это раздел агрономии?
Теперь о предложенном в статье решении:
Решение в 15-ричном представлении, безусловно, короткое. Но следующее же изменения в правилах о замене 5 на 55 делает решение непригодным. И если бы было правило «DATA есть массив строк в 10-ричном представлении».
Я не понял правило №13. Во-первых, в оригинале «the input can (т.е. могут, но не обязаны) contain decimals». Кажется, что просят добавить в DATA строки вида "15.00" и "21.33", причём первое из них должно считаться кратным 3 и 5, верно? Если так, то решение автора не подходит.
Меньше ошибок на этапе runtime. Многие проблемы ловятся компилятором.
Я загрузил код из статьи в TS Playground и чуть-чуть его поменял. В частности, в функцию createClient я добавил отрицание перед route.hasIdParam и TS его проглотила, не показала ни одной ошибки типов.
Другой пример
const routes: Routes = { ... } // вместо "as const satisfies Routes"
function example(routes: Routes) {
const apiClient = createClient(routes);
apiClient.getUsers().then(console.log);
apiClient.getUserById().then(console.log); // <- нет ошибки
if (routes.getUserById.hasIdParam)
apiClient.getUserById(123).then(console.log); // <- есть ошибка
apiClient.createUser().then(console.log);
}
Приведённый в статье пример вынесен в функцию, routes имеет общий тип Routes, что является типичной ситуацией, когда конфигурация не отлитая в золоте и не высеченная в граните ещё до компиляции, а, например, считывается из файла.
Почему-то getUserById можно вызвать без аргументов, хотя она-то требует число. А если явно проверить, что hasIdParam истинно, то с числом вызвать нельзя.
Ложные-отрицательные срабатывания (проблемы нет, а ошибка случается) ещё терпимы, а ложно-положительные срабатывания (проблема в типизации есть, а компилятор молчит) — это бомба замедленного действия.
Можно ли где-то почитать конкретные критерии того, какие ошибки типизации отлавливаются TS, а какие требуют внимательного контроля со стороны программиста и тестирования?
Подобные языки для доказательства теорем очень напоминают правила построения грамматик.
Да, связь есть.
Терминология
«Языки для доказательств» называются «proof assistant».
Каждый из них основан на некоторой системе типов (Coq основан на CoC — calculus of constructions, что обусловило «петушиность» названия) и предоставляет некоторую обвязку в виде тактик, синтаксического сахара и прочих вещей, без которых повесится хочется.
В этом сообщении я не провожу различий между синтаксисом и грамматикой.
С одной стороны, система типов — это как бы грамматика на стероидах. Если грамматика выделяет из множества всех слов над алфавитом язык — подмножество слов, которые являются «синтаксически/грамматически правильными», — то типизация выделяет из этого языка те, которые к тому же являются «правильно-типизированными». Неформальная иллюстрация:
любой текст =[синтаксис]=> читаемый текст =[типизация]=> осмысленный текст
При этом правила типизации могут быть более выразительными за счёт того, что на этом этапе текст уже прошел синтаксический разбор и представим в виде AST со всеми особенностями и гарантиями используемой грамматики. Грубо говоря, это как переход работы со строка на bash к работе с объектами в PowerShell.
С другой стороны, процесс доказательства соответствия текста и системе типов, и грамматике называется выводом. В частности, если рассмотреть язык, в котором грамматика тривиальная (регулярка: .*), а система типов имеет конечное число типов, то такая система типов будет сама работать как грамматика, в которой типы выполняют роль нетерминальных символов. (Правда, надо ещё кое-какие ограничения наложить на вид правил вывода, чтобы получить точное соответствие порождающим грамматикам)
В качестве отправной точки можно посмотреть работы Барендрегта по Pure/Generalized Type Systems.
Кто-то как-то исследовал взаимосвязь грамматических правил и доказательство теорем?
Я не знаю работ именно по этому вопросу. Смежные привёл выше.
На всякий случай уточню, что системы типов — частный случай логических систем (некоторые считают, что справедливо и обратное), а вывод типов и доказательства теорем — это одно и то же в этих системах. Поэтому можно почитать любую литературу по теории типов: Girard et al. «Proofs and Types», Geuvers «Introduction to Type Theory» и прочие.
кто-то исследовал грамматики для построения описания научных правил и законов?
Не знаю. Идея формально описать естественно-научные теории и типизировать их лежит на поверхности. Не думаю, что никто этим не занимался.
лично моё мнение
С практической точки зрения интересны только те формализмы, которые позволят оперировать естественными для физики вещами, вроде «утверждение выполняется в лабораторных условиях / с интересующей точностью» при том, что не считается нужным или возможным точно проговаривать, в чём именно состоят лабораторные условия и какова в цифрах интересующая точность.
P.S. Только увидел презентацию Родина «Структурализм у Гильберта и Бурбаки», цитата оттуда:
Аксиоматический метод в исполнении Бурбаки существенно отличается от аксиоматического метода Гильберта. Патрик Суппес в контексте попытки использования аксиоматического метода в физике назвал бурбакистскую версию аксиоматического метод семантическим.
Странным образом дискуссия о различии между синтаксическим и семантическим вариантами аксиоматического метода мало затронула философию математики. Сами Бурбаки, по всей очевидности, просто не придавали значения таким логическим и философским тонкостям.
Контекст цитаты: обсуждение множества неизоморфных групп, изучаемых Лагранжем. То есть, это не совсем про наш вопрос, но слова те же :)
Статья предлагает следующий метод оценки возможности отличить результат генерации ИИ от человека:
Просим ChatGPT сгенерировать текст
Восхищаемся (или нет, как многие здесь в комментариях) результатом генерации
Скармливаем результат генерации инструментам классификации текстов
Видим, что в среднем классификаторы не могут отличить ChatGPT от человека
Делаем какие-то выводы
Задача ChatGPT — порождать правдоподобный текст. Это буквально значит, что задача гопоты — порождать тексты так, чтобы никаким образом нельзя было статистически значимо отличать его тексты от человеческих, по крайней мере по темам/жанрам/стилю/… обучающей выборки.
Если имеется инструмент, который статистически значимо может отличить текст от ChatGPT от человеческого, то всегда можно сделать обёртку над ChatGPT, которая бы генерировала тексты до тех пор, пока не будет сгенерирован текст, классифицируемый этим инструментом как человеческий.
Делать выводы на основе проверки текстов ИИ по работе классификаторов — это как делать выводы об уровне жизни в России по опросу московских депутатов.
Проще говоря, автор проверил, что создатели ChatGPT не облажались вчистую. Почему и на основе чего автор делает какие-то восторженно-эмоциональные выводы –- не понятно. Если же выбросить весь блок с экспериментом, то от статьи останется только вода и рассуждения об авторском праве.
особенно если у вас геометрическая/топологическая интуиция прокачана.
По моему мнению, геометрическая интуиция особо не поможет. Точнее, она поможет ровно в той части, где используется геометрическая интерпретация. А поскольку большую часть книги проще понять, используя логические и вычислительные аналогии, а за пределами используются ∞-категорные построения, которые фиг нарисуешь, кроме как диаграммой, на геометрическую интуицию надеяться не стоит.
ИМХО, слово «гомотопическая» в названии — это больше пиар-ход, чем характеристика теории. Хотя Роберт Харпер высказывался, что HoTT можно читать как «(некая) теория гомотопических типов» (ввиду упомянутой геометрической интерпретации типов) и как «гомотопическая теория (неких) типов» (ввиду синтетичного характера построений внутри теории).
движения там и правда особо не наблюдается
В 2023-2024гг. я наблюдал сильное желание втащить в HoTT модальность в разных вариациях: формализация на HoTT модальных теорий, теория модальных типов, модальная теория зависимых типов и т.д. и т.п.
Лично мне тяжело давалось понятие переменной в императивных языках, а и в целом концепция мутабельного состояния. В школе я недоумевал, почему нельзя писать так, как в математике принято, мол, «пусть y = f(x)» и чтоб дальше по тексту y и f(x) были взаимозаменяемы. А нельзя, потому что переменная — это не переменная, а участок памяти, и y меняться может. А функция — это не функция, а процедура, которая (как автор подметил) возвращает значение. Поэтому нельзя просто так «if y > 0 then print(y)» заменить на «if f(x) > 0 then print(f(x))».
Потом, когда уже приловчился работать с состоянием, я открыл для себя ФП и жизнь стала радостнее.
А вот некоторые мои знакомые, уже уважаемые физики, до сих пор не освоились. Питонят в терминах своей предметной области, а потом удивляют, почему это, когда строка в одной матрице меняется внутри функции, другая матрица, которая в этой же функции даже не используется, тоже меняется. Вот чудеса-то!
Мне вот интересно, можно ли обучить детей (особенно с математическим складом ума) программировать, отталкиваясь от λ-исчисления и вообще обходя стороной (до времени) вопросы о внутреннем устройстве железки? Своих детей ещё нет, хотя не уверен, что решусь и на них такой эксперимент поставить.
Любое линейное преобразование двумерного пространства это композиция растяжения, сдвига, скашивания, поворота и отражения относительно какой-либо линии.
За сдвиг отвечает сложение векторов, а умножение матрицы на вектор представляет те преобразования, которые оставляют начало координат на месте.
Я как-то привык, что, говоря о линейных преобразованиях, имеют в виду те, что сохраняют ноль. Но это маловажный вопрос терминологии.
Вопрос же: верно ли, что пространство преобразований сдвига изоморфно пространству векторов? Всегда ли «трансляционная» компонента независима от «линейной с неподвижным нулём»? Для обычных линейных пространств ℝ^n то всегда, но вдруг есть иные хитрые неведомые мне алгебраические структуры (кольца, модули), где эта догма не работает.
Классическая логика, в которой имеется закон снятия двойного отрицания, исключения третьего и принцип двойственности, не соответствует вычислительной системе. Так, многие теоремы о существовании не предлагают алгоритм нахождения того, существование чего они утверждают.
Интуиционистские логики тождественны некоторым вычислительным системам, что было показано упомянутыми двумя господами.
Вычисления не всегда подразумевают работу с числами. Слова получше не придумали.
С одной стороны, да. С другой же — ценность всей статьи состоит в ссылке на https://arxiv.org/pdf/1604.06766 и в графиках для известных проектов.
Отвечаю вместо автора цитатой:
Different alternatives could be used as a means for determining authorship <ссылки>. Among those, we chose the degree-of-authorship (DOA) metric <ссылки>, which we normalize after calculation. Given a file f with path fp, the degree-of-authorship of a developer d whose Git user has been mapped to md is given by DOA(md, fp) = 3.293 + 1.098 × FA(md, fp) + 0.164× DL(md, fp) − 0.321 × ln(1 + AC (md, fp)) From the equation, DOA depends on three factors: (i) first authorship (FA): if md originally created f, FA is 1; otherwise it is 0; (ii) number of deliveries (DL): number of changes in f made by md; (iii) number of acceptances (AC): number of changes in f made by any developer, except md.
The model assumes FA as the strongest predictor of authorship. Recency information (DL) positively contributes to authorship, but with less importance. In contrast, other developers’ changes (AC) decrease one’s DOA, although at a slower pace. The weights we use in the DOA model stem from empirical experiments performed elsewhere.
Заявленные (вполне очевидные, прямолинейно следующие из построения) преимущества модели:
(i) assuming the weights of the model to be general, DOA does not require a training set; (ii) DOA does not require monitoring editing activities as developers maintain different files; (iii) instead of considering all developers changing a file as its authors, DOA weights contributions differently, accounting for both changes of a developer in a file (increases DOA), as well as the changes performed by others (decreases DOA).
P.S. Впрочем, я так и не понял, откуда циферки взялись аж с тремя знаками после запятой. Возможно, это обосновывается в одной из ссылок, но в работе выглядит, конечно, странно.
Баг, версия, деталь, критический, манипуляция, органичный, элемент, эффект, фича — предложенные варианты перевода не соответствуют основному смыслу, но могут использоваться только в узком контексте.
Позвольте мне подушнить немного, потому что я тоже вижу среди некоторых сограждан поведение в отношении ИИ такое, каким бывает у других в отношении идолов, икон и прочих объектов почитания, которые мы с уверенностью называем религиозными.
Понятие религии очень плохо определено. Например, процитированное выше из Википедии (которой, как известно, доверять не стоит) не включает тотемизм и другие формы примитивной религии, не имеющие моральных норм или противопоставления естественного—сверхъестественного, а также едва ли включает буддизм. В самой Википедии (которой, как известно, доверять не стоит) проблема определения тоже рассматривается.
Процитирую первую после Википедии ссылку в поисковой выдаче, «Религиоведение» В. Лебедев, А. Прилуцкий, В. Викторов:
Я наблюдаю много сограждан, особенно вне IT, которые к ИИ относятся именно подобным образом, если сделать s/бог/ИИ/g.
</zanuda>
Вероятно, учёные, применившие ИИ для обнаружения 10000 белков, знают, что они делают и что они получили. Но в основном-то народ говорит иначе: «у них получилось для их задач, значит у нас точно(!) получится для наших», «если у нас не получилось, то проблема в нас, а не в ИИ», «наверное, вы просто недостаточно мощную модель/железо взяли — заплати и все проблемы будут решены». Критерий Поппера стоит в сторонке.
Задача состоит в том, чтобы на основе 3 документов составить один так, чтобы он содержал всю информацию, что содержится в первых двух документах, без повторов, компактно, с учётом того, что информация в третьем документе истинна и будущий читатель её знает. Дополнительная задача: обосновать соответствие полученного документа исходному заданию.
Вам дали задачу написать обзор на книгу. Вы берёте, вырываете случайные страницы клочками, что целые главы идут в топку, а только после этого садитесь её читать. Со вниманием, с усердием. Вот на что это похоже.
Я этого не говорил. Правда, я допускал, что кто-то может это сказать, мол, «докинь памяти побольше и будет тебе надёжность», к чему я отношусь скептически. Я же утверждаю, что если длина контекста с гулькин нос, но надёжности неоткуда взяться.
Каким образом осуществляется проверка (верификация) ответа, выданного сетью?
Покажу вопрос на примере, который был, когда я в последний раз пытался применить LLM.
Задача: соединить два подобных документа (скажем, две версии статьи по мотивам модуля) в один или переписать один документ в более компактном виде за счёт исключения повторений. При этом необходимо считать, что потенциальный читатель знает содержание некоторого третьего документа (скажем, список реализованных в модуле функций с их типами), чтобы 1) удалять то, что уже известно, 2) отождествлять то, что обычно не отождествляют.
Метод решения: просим LLM решить задачу, описывает ситуацию, добавляем все три документа, явно маркируя их границы, описываем выходной формат.
Проблема: бывает, что сетка игнорирует фрагменты документов (иногда фразы, иногда предложения, иногда разделы). Выходной результат неправильный.
Я пробовал использовать LLM для верификации, но столкнулся с двумя проблемами: или результат верификации ненадёжен, или требуется размер контекста больше, чем я могу предоставить (особенно если для верификации загружать и «рассуждения» первой сетки).
Прошу прощения, что публично, а не в личку, но пунктуация тут великолепна.
Скрытый текст
Пока не дочитал до конца, думал, что эта статья написана гопотой, потому что никто (кроме автора этой статьи) не будет вставлять код с неочевидным синтаксисом и не объяснять хотя бы в комментариях, что каждый синтаксический элемент означает и как надо думать, чтобы самому такое написать.
Выше имеется вполне хорошая дискуссия со сравнением этого языка с Агдой. Я тоже всуну свои пять копеек.
Развитые системы типов нужны для того, чтобы было сложнее сделать ошибку в логике программы. К удобству программирования это имеет слабое отношение, разве что кто-то скажет «как это удобно, когда компилятор не даёт мне писать код с ошибками типизации».
Плохо, что сейчас имеется мало исследований влияния дизайна языка программирования на его эргономику. Кажется, что это ровно то, чего автору не хватает в существующих языках. Впрочем, он и на своём языке не проверяет гипотезу о том, что кому-то на этом будет писать удобнее, чем на Haskell. Хнык.
По моему опыту ТК хорошо показывает себя в программировании в двух основных случаях:
(исследование) когда надо хорошо отработанную концептуальную систему перенести на другую область. Скажем, представления групп является частный случаем общего категорного метода, который подобные приёмы позволяет штамповать массово.
В частности, это позволяет оперировать известными понятиями и аналогиями (пространство, отображение, подпространство, произведение) без уточнения конкретики. Например,
в физике мы можем долго говорить о периодичной волновой функции и порождаемом ей расслоении на зоне Бриллюэна без уточнения, считаем ли мы её гладкой или дважды гладкой: в каждом случае мы просто говорим, что все упомянутые в рассуждении функции будут такими, какими мы хотим. Рассуждения становятся короткими, вся математическая лабуда про гладкость не упоминается, а выкладки не перестают быть формальными. При этом по рассуждениям чётко видно, какие минимальные требования на гладкость накладываются.
В программировании ТК позволяет нам корректно говорить о тех функциях, которыми мы программируем. Ведь если говорить по-честному, то, что мы привыкли называть функциями в программировании, имеет мало что общего с функциями в классической математике: 1) первые могут зацикливаться, а вторые всегда что-то возвращают; 2) первые с необходимостью задают алгоритм вычисления (даже в декларативных языках), вторые — нет; 3) первые имеют нефункциональные характеристики (затраты по времени и памяти), вторые — нет; 4) недетерминизм, работа с состоянием и прочие прелести во всех ЯП, кроме чистых функциональных.
Тем не менее на практике мы склонные отождествлять эти понятия в одних случаях, и различать только тогда, когда вышеприведённые особенности проявляются. ТК легализует подобную (якобы) демагогию, переводя в статус аккуратно формализованной теории.
(обучение) когда надо спроектировать API, чтобы он воспринимался как естественный интерфейс. SQL тем хорош, что основывается на реляционном исчислении и реляционной алгебре: первое даёт метод решения широкого класса задач, выражаемых на языке первого порядка; второй позволяет быстро оценить, какие запросы эквивалентны. Обычно интерфейс, основанный на алгебраической системе, ощущается как более простой и обоснованный по сравнению с тем, который делает по велению левой пятки. ТК позволяет обобщить это на тот класс систем, API к которым в принципе не может выражаться простой алгебраической системой. В частности, ТК формализует рад полезных понятий:
функтор («структура данных», …)
естественное преобразование
терминальный и инициальный объекты (обычно имеют свои названия в разных предметных областях, вроде «атомарный X» или «пустой X»)
произведение и сумма
изоморфизм («равный с точностью до того, что нам не интересно»)
подобъект (подпространство, под-что-угодно)
универсальность (свободный функтор, сопряжения и т.п.)
Если проектируешь API и сумел достичь того, что большинство структур данных — функторы; большинство функций являются естественными преобразованиями; большинство объектов, с которыми пользователь будет работать, можно собрать из произведений, сумм, терминальных и инициальных объектов; все или почти все функции «уважают» изоморфизмы; все требования состоят в коммутативности некоторых диаграмм, — если всё это есть, то, вероятно, это прекрасный API, который не подложит свинью в неожиданный момент. Пользователь будет воспринимать этот интерфейс как естественный и, в идеале, как единственно возможный и обоснованный.
Я написал «по-маркетологски», но идея тут простая: API должен быть простым и обоснованным. Алгебры — это просто и обоснованно. Категории — это (для пользователя) просто и обоснованно. Для разработчика категории сложнее, ибо теория серьёзнее, но универсальнее.
А чисто посчитать что-то категории не нужны. Подобно типизации и тестированию, ТК не нужен, чтобы собственно считать, но занимают определённое место в проектировании и сопровождении программного продукта.
Насколько я понял, это перевод не от автора. Но вопросы есть.
Это как? Какое отношение теории категорий имеет к задаче категоризации? Или это как с теорией групп, которая нужна для группировки вкладок в браузере, а теория полей — это раздел агрономии?
Теперь о предложенном в статье решении:
Решение в 15-ричном представлении, безусловно, короткое. Но следующее же изменения в правилах о замене 5 на 55 делает решение непригодным. И если бы было правило «DATA есть массив строк в 10-ричном представлении».
Я не понял правило №13. Во-первых, в оригинале «the input can (т.е. могут, но не обязаны) contain decimals». Кажется, что просят добавить в DATA строки вида "15.00" и "21.33", причём первое из них должно считаться кратным 3 и 5, верно? Если так, то решение автора не подходит.
Я загрузил код из статьи в TS Playground и чуть-чуть его поменял. В частности, в функцию
createClientя добавил отрицание передroute.hasIdParamи TS его проглотила, не показала ни одной ошибки типов.Другой пример
Приведённый в статье пример вынесен в функцию,
routesимеет общий типRoutes, что является типичной ситуацией, когда конфигурация не отлитая в золоте и не высеченная в граните ещё до компиляции, а, например, считывается из файла.Почему-то
getUserByIdможно вызвать без аргументов, хотя она-то требует число. А если явно проверить, что hasIdParam истинно, то с числом вызвать нельзя.Ложные-отрицательные срабатывания (проблемы нет, а ошибка случается) ещё терпимы, а ложно-положительные срабатывания (проблема в типизации есть, а компилятор молчит) — это бомба замедленного действия.
Можно ли где-то почитать конкретные критерии того, какие ошибки типизации отлавливаются TS, а какие требуют внимательного контроля со стороны программиста и тестирования?
Да, связь есть.
Терминология
«Языки для доказательств» называются «proof assistant».
Каждый из них основан на некоторой системе типов (Coq основан на CoC — calculus of constructions, что обусловило «петушиность» названия) и предоставляет некоторую обвязку в виде тактик, синтаксического сахара и прочих вещей, без которых повесится хочется.
В этом сообщении я не провожу различий между синтаксисом и грамматикой.
С одной стороны, система типов — это как бы грамматика на стероидах. Если грамматика выделяет из множества всех слов над алфавитом язык — подмножество слов, которые являются «синтаксически/грамматически правильными», — то типизация выделяет из этого языка те, которые к тому же являются «правильно-типизированными». Неформальная иллюстрация:
любой текст =[синтаксис]=> читаемый текст =[типизация]=> осмысленный текстПри этом правила типизации могут быть более выразительными за счёт того, что на этом этапе текст уже прошел синтаксический разбор и представим в виде AST со всеми особенностями и гарантиями используемой грамматики. Грубо говоря, это как переход работы со строка на bash к работе с объектами в PowerShell.
С другой стороны, процесс доказательства соответствия текста и системе типов, и грамматике называется выводом. В частности, если рассмотреть язык, в котором грамматика тривиальная (регулярка:
.*), а система типов имеет конечное число типов, то такая система типов будет сама работать как грамматика, в которой типы выполняют роль нетерминальных символов. (Правда, надо ещё кое-какие ограничения наложить на вид правил вывода, чтобы получить точное соответствие порождающим грамматикам)В качестве отправной точки можно посмотреть работы Барендрегта по Pure/Generalized Type Systems.
Я не знаю работ именно по этому вопросу. Смежные привёл выше.
На всякий случай уточню, что системы типов — частный случай логических систем (некоторые считают, что справедливо и обратное), а вывод типов и доказательства теорем — это одно и то же в этих системах. Поэтому можно почитать любую литературу по теории типов: Girard et al. «Proofs and Types», Geuvers «Introduction to Type Theory» и прочие.
Не знаю. Идея формально описать естественно-научные теории и типизировать их лежит на поверхности. Не думаю, что никто этим не занимался.
лично моё мнение
С практической точки зрения интересны только те формализмы, которые позволят оперировать естественными для физики вещами, вроде «утверждение выполняется в лабораторных условиях / с интересующей точностью» при том, что не считается нужным или возможным точно проговаривать, в чём именно состоят лабораторные условия и какова в цифрах интересующая точность.
P.S. Только увидел презентацию Родина «Структурализм у Гильберта и Бурбаки», цитата оттуда:
Контекст цитаты: обсуждение множества неизоморфных групп, изучаемых Лагранжем. То есть, это не совсем про наш вопрос, но слова те же :)
Если можно серию замен, то и регулярки не нужны.
Надо же. Получается, методология исследования в этой статье совсем никуда не годится.
Автор ответил на вопрос, но я резюмирую и отвечу с другой стороны.
Итак: да, всё правильно сказано, Это T пихают ровно затем, чтобы не писать вертикально, как положено, а горизонтально.
Причина проста: внутри текста очень хочется экономить вертикальное расстояние и по максимуму линеаризировать запись. Например,
Дроби стараются писать в строку
, а не в два этажа 
Индексы в пределах и суммах пишут в нижнем правом индексе, а не внизу:
Это не касается выключных формул, но и в них могут писать так по инерции.
Статья предлагает следующий метод оценки возможности отличить результат генерации ИИ от человека:
Просим ChatGPT сгенерировать текст
Восхищаемся (или нет, как многие здесь в комментариях) результатом генерации
Скармливаем результат генерации инструментам классификации текстов
Видим, что в среднем классификаторы не могут отличить ChatGPT от человека
Делаем какие-то выводы
Задача ChatGPT — порождать правдоподобный текст. Это буквально значит, что задача гопоты — порождать тексты так, чтобы никаким образом нельзя было статистически значимо отличать его тексты от человеческих, по крайней мере по темам/жанрам/стилю/… обучающей выборки.
Если имеется инструмент, который статистически значимо может отличить текст от ChatGPT от человеческого, то всегда можно сделать обёртку над ChatGPT, которая бы генерировала тексты до тех пор, пока не будет сгенерирован текст, классифицируемый этим инструментом как человеческий.
Делать выводы на основе проверки текстов ИИ по работе классификаторов — это как делать выводы об уровне жизни в России по опросу московских депутатов.
Проще говоря, автор проверил, что создатели ChatGPT не облажались вчистую. Почему и на основе чего автор делает какие-то восторженно-эмоциональные выводы –- не понятно. Если же выбросить весь блок с экспериментом, то от статьи останется только вода и рассуждения об авторском праве.
По моему мнению, геометрическая интуиция особо не поможет. Точнее, она поможет ровно в той части, где используется геометрическая интерпретация. А поскольку большую часть книги проще понять, используя логические и вычислительные аналогии, а за пределами используются ∞-категорные построения, которые фиг нарисуешь, кроме как диаграммой, на геометрическую интуицию надеяться не стоит.
ИМХО, слово «гомотопическая» в названии — это больше пиар-ход, чем характеристика теории. Хотя Роберт Харпер высказывался, что HoTT можно читать как «(некая) теория гомотопических типов» (ввиду упомянутой геометрической интерпретации типов) и как «гомотопическая теория (неких) типов» (ввиду синтетичного характера построений внутри теории).
В 2023-2024гг. я наблюдал сильное желание втащить в HoTT модальность в разных вариациях: формализация на HoTT модальных теорий, теория модальных типов, модальная теория зависимых типов и т.д. и т.п.
Сомнительный прогресс, конечно, но чем богаты.
Лично мне тяжело давалось понятие переменной в императивных языках, а и в целом концепция мутабельного состояния. В школе я недоумевал, почему нельзя писать так, как в математике принято, мол, «пусть y = f(x)» и чтоб дальше по тексту y и f(x) были взаимозаменяемы. А нельзя, потому что переменная — это не переменная, а участок памяти, и y меняться может. А функция — это не функция, а процедура, которая (как автор подметил) возвращает значение. Поэтому нельзя просто так «if y > 0 then print(y)» заменить на «if f(x) > 0 then print(f(x))».
Потом, когда уже приловчился работать с состоянием, я открыл для себя ФП и жизнь стала радостнее.
А вот некоторые мои знакомые, уже уважаемые физики, до сих пор не освоились. Питонят в терминах своей предметной области, а потом удивляют, почему это, когда строка в одной матрице меняется внутри функции, другая матрица, которая в этой же функции даже не используется, тоже меняется. Вот чудеса-то!
Мне вот интересно, можно ли обучить детей (особенно с математическим складом ума) программировать, отталкиваясь от λ-исчисления и вообще обходя стороной (до времени) вопросы о внутреннем устройстве железки? Своих детей ещё нет, хотя не уверен, что решусь и на них такой эксперимент поставить.
Я как-то привык, что, говоря о линейных преобразованиях, имеют в виду те, что сохраняют ноль. Но это маловажный вопрос терминологии.
Вопрос же: верно ли, что пространство преобразований сдвига изоморфно пространству векторов? Всегда ли «трансляционная» компонента независима от «линейной с неподвижным нулём»? Для обычных линейных пространств ℝ^n то всегда, но вдруг есть иные хитрые неведомые мне алгебраические структуры (кольца, модули), где эта догма не работает.
Да. На всякий случай уточню пару моментов:
Классическая логика, в которой имеется закон снятия двойного отрицания, исключения третьего и принцип двойственности, не соответствует вычислительной системе. Так, многие теоремы о существовании не предлагают алгоритм нахождения того, существование чего они утверждают.
Интуиционистские логики тождественны некоторым вычислительным системам, что было показано упомянутыми двумя господами.
Вычисления не всегда подразумевают работу с числами. Слова получше не придумали.
Из соответствия Карри-Говарда, например.
С одной стороны, да. С другой же — ценность всей статьи состоит в ссылке на https://arxiv.org/pdf/1604.06766 и в графиках для известных проектов.
Отвечаю вместо автора цитатой:
Заявленные (вполне очевидные, прямолинейно следующие из построения) преимущества модели:
P.S. Впрочем, я так и не понял, откуда циферки взялись аж с тремя знаками после запятой. Возможно, это обосновывается в одной из ссылок, но в работе выглядит, конечно, странно.
Спасибо, что хоть не «точный» и «правильный».
Баг, версия, деталь, критический, манипуляция, органичный, элемент, эффект, фича — предложенные варианты перевода не соответствуют основному смыслу, но могут использоваться только в узком контексте.