Уточню. Вот тут не надо путать терм (тот самый x) и его значение. Для значений нет проблем построить предикат принадлежности.
Да. Я, конечно, говорю только о термах. Понятие «значения» требует определения, что мы под ним понимаем: если денотат в модели, то нужна сама модель.
Ага, только вот во всех языках программирования, включая Agda и Idris, любой тип является множеством (есть попытки убрать аксиому K из языков, но они все за флагами)
Не знал, что в Агде пытаются убрать аксиому K. Спасибо за тему.
В целом, ожидается, что в «обычных» ЯП тип является «множеством» в смысле HoTT. Просто это не совсем похоже на классические множества.
Я тут ещё вспомнил про constraint type, которые как раз интерпретируются как предикаты на универсуме значений (не разбираюсь в них, ссылок сходу не нашел, хотя упомянутый Картрайт о них говорит). Так что моя категоричность пошаталась. Я не ситх, мне можно.
занимаясь практическим программированием считать типы множествами не так уж и глупо.
Не глупо, если учитывать все оговорки. Правильно ли это дидактически? Я усомнился, поэтому высказался.
Лет десять назад я имел такие же представления о типах. Сейчас же у меня вызывают протест многие утверждения из начала статьи, которые формируют неформально понятийную систему у читателя и тем самым определяют путь в своих рассуждениях.
Множество — это коллекция элементов, обладающих общим свойством, которые рассматриваются как единое целое
В общепринятой математике множество — это (неформально говоря) объекты, рассматриваемые как один объект. На объектах определено отношение (двуместный предикат) принадлежности, то есть один объект или принадлежит второму, или нет. Если второй объект не множество — всегда нет.
Никакое требование об общем свойстве не накладывается: множество {1, "hello", <кот Василий>} существует. Есть множества, все элементы которого имеют только то общее свойство, что они принадлежат этому множеству.
Множества подчиняются аксиоме объёмности: если два множества состоят из одних и тех же элементов, то это одно и то же множество.
Типы в программировании можно(и нужно) рассматривать как математические множества.
Лучше бы так не делать, потому что типы не обладают вышеперечисленными свойствами множеств. Начнём с того, что нет предиката принадлежности объекта типу. Когда мы пишем x : T, мы не говорим «вот есть объект T, вот есть объект x; кстати, T — это тип; ах да, x принадлежит T». Мы вместо этого говорим или «вот есть выражение x и оно доказуемо по построению имеет T», или «вот переменная x, считать её по определению имеющей тип T».
Многие системы типов устроены так, что никакой объект не может быть экземпляром двух типов. Как в таких условиях говорить об аксиоме объёмности?
Я бы говорил о типах как о метках, которые мы ставим на выражениях. Система типов должна ограничивать нас, и через этого гарантировать, что выполняются какие-то свойства у любого правильно-типизированного выражения.
В качестве антитезы следует согласиться, что типы и множества связаны.
С одной стороны, развитые системы типов (вроде Agda, Coq, HoTT) считают, что множество — это частный вид типов. Но там и множество понимает не общепринято. Поскольку я плохо разбираюсь в интуиционистском варианте теории множеств, призываю малышку @Natasha_Klaus на помощь пояснить за Coq. В HoTT множеством называется тип, у которого любые два экземпляра равны не более чем одним способом.
С другой стороны, для системы типов можно построить модель, в которой каждому типу сопоставляется множество. Впрочем, для программирования более полезны другие виды моделей:
тип как топологическое пространство (точнее, решётка, см. работы Даны Скотт) — позволяет адекватно говорить о функции f : A → B как о непрерывном отображении из A в B, потому что не всякая функция из множества A во множество B может быть программой
тип как идеал — то же, но с поддержкой полиморфизма (дженериков)
тип как интервал — то же, но с нормальной поддержкой полиморфизма и типов-дополнений (т.е. «всё, что не является элементом типа A»)
Всего лишь несколько столетий назад считалось, что Земля неподвижна, а Солнце и планеты вращаются вокруг неё. Теперь мы знаем, что именно планеты движутся вокруг Солнца.
Прибедняетесь.
Ньютон и Кеплер жили сильно раньше. Коперник — вообще полтысячилетия назад.
Благодарю за ответ. Хотя я и не увидел в нём ссылок на серьёзные работы, сделанные серьёзными людьми, а не только рассуждения анонимуса с неизвестной мне квалификации, на остальные вопросы я получил ответ.
P.S. Наука является деятельность, а любая деятельность обладает целью (или же является бесцельной, но это не случай науки). Субъект ставит (и в этом смысле её имеет) и достигает цель.
Предисловие: я не имею цель с вами спорить. Я аргументированно прокомментировал первоначальный наезд, а сейчас отвечаю за свои слова. Плохо понимаю ваш уровень вовлечённости в лингвистику и в науку в целом, поэтому, возможно, не понял подтекст вашего последнего комментария.
налицо некорректное обобщение.
Обобщение сделано в контексте текущей беседы.
Зализняк — известный и признанный учёный в своей области. Поэтому позиция по умолчанию «умного дядьку надо слушать». Любая другая позиция требует пояснений, например:
«я тоже учёный в этой же области и мне виднее»
«более авторитетный учёный выразил несогласие и привёл более убедительные аргументы»
«я никаво ни слушаю, гы-гы-гы»
конкретно Зализняк много участвовал в берестяных грамотах и СПИ,что дает повод поставить под сомнение и другие его достижения.
Вы знаете что-то такое, чего не знаю я, видимо. Что не так с БГ? Что не так с СПИ?
Например, я слушал его лекцию, посвященную СПИ, где он приводит (помимо других) аргумент о порядке слов в перфекте «творил есмь» / «есмь творил», закон которого был открыт в последние десятилетия, но который соблюдается в каждом случае употребления в СПИ. Мне показался аргумент любопытным и достаточно убедительным.
а научно-профессионалная историческая лингвистика используется .. для того же.но ! используется научно и профессионально, а это совсем другое.
Я выразился неаккуратно. Цель и причина любительского словоблудия — дешевая агитация. Цель науки — изучение того, как наш мир функционирует. Использование же науки лежит вне научного метода, а именно, в смежных прикладных областях человеческой деятельности: инженерии, политике и т.п. Впрочем, без этого (эффективного) использования не было бы спроса на науку, а вместе с тем не было бы и самой науки за ненадобность.
С одной стороны, буквально на днях слушал лекцию Зализняка нашего уважаемого А.А., в которой он на вопрос о происхождении слова «счастье» выдал именно эту версию. Это в то время, как лекция была про научный метод и содержала направленную на Фоменко, Задорнова и прочих критику их вольный построений («задорновщины»).
А если предлагается с мнением Зализняка не считаться и «отказаться от использования историко-лингвистических/этимологических построений», то и других учёных тогда можно не слушать, дескать, «я отказался от теоретико-физических построений, чего и всем рекомендую». Странно это. Лично я не рекомендую так делать.
С другой стороны, этот параграф в тексте выглядит инородно. Он как будто бы пытается на основе этимологии вывести современный нам смысл и что-то этим обосновать или дополнить в нелингвистических исследованиях. Это похоже на примеры, которые в упомянутой лекции Зализняк приводил про «укров» и «эт-русков», когда любительская этимология используется для обоснования политических или социальных притязаний.
Если в игре есть экономика, то она устанавливает стоимость предмета. Но для этого она должна быть, включая 1) механику купли-продажи, 2) наличие спроса и предложение (достаточное число игроков). Если игроки разводятся по инстансам и вообще это одиночная РПГ, то экономики не будет.
Полезность метода вот в чём. Допустим, игроделы выпустили прототип игры, собрали данные от тестеров, понерфили-побалансировали характеристики, включая цену, выпустили в народ. А затем начали клепать контент, включая предметы в большом количестве. Какие характеристики установить, чтобы не надо было дополнительно балансировать их?
Предлагается все, кроме цены, взять с потолка, а цену рассчитать по формуле.
Я так вижу практическую значимость статьи. Другое дело, линейное приближение мне кажется плохим. Вон выше уже написали об этом, а кроме того в дуэлях единица урона может отделять победу, так что в тех случаях цена может быть очень нелинейной.
В последних рассуждениях я неявно предположил, что теория обладает экстенсиональностью, т.е. что из f(x) = g(x) для любого x следует f = g. Если это не так, всё усложняется. Замечу, что с этой же проблемой должен был столкнуться автор текста где-то в окрестности следующего абзаца:
Вторым интересным свойством identity функций является то что мы всегда можем подобрать такой код что программно будет легко определить что это identity функция.
Далее мои мысли:
Dependent&refined types как раз являются реализацией этой парадигмы на минималках.
Refined types — это да, подходящая тема. А зависимые типы интересны и сами по себе. А поскольку они требуют некий рантайм на уровне типов, то без явной типизации там очень сложно.
Наконец, автор предложил порассуждать насчёт соответствия Карри-Говарда. В то время как классическая логика старается говорить о высказываниях и задвинуть доказательства под ковёр (например, мало кого интересует, каким доказательством доказана теорема Пифагора во время использования, ведь важно только то, что оно где-то существует), в предложенном подходе будет наблюдаться ровно обратная ситуация: доказательства (=функции) есть, а высказываний (=типов) нет. Впрочем, я плохо представляю, какой логике соответствует система refined types, поскольку с ними не работал вплотную.
P.S. редактор Хабры преждевременно отправил сообщение. Поэтому прошу прощения за резкость в первом абзаце, я перечитал текст и увидел полезные ссылки и сравнения.
Несмотря на низкий интерес сообщества к этой теме, выскажу свои замечания насчёт того, что в определённых кругах всем известно, чтобы интересующиеся могли пойти читать серьёзную литературу, а те, кто в теме, могли соотнести сказанное в этой статье с другими близкими направлениями. Так сказать, восполню отсутствующий в тексте раздел Related Works.
В теории категорий известно, что морфизмы важнее объектов. Применимо к категории типов (как бы она ни определялась) это значит, что функции важнее типов. В частности, существует способ сформулировать понятие категории исключительно на морфизмах, вообще не прибегая к упоминанию объектов (см. МакЛейн «Категории для работающего математика», первые главы). Применимо к категории типов это значит, что можно говорить о типизации и о типах вообще не упоминая типы, а говоря только о функциях. Например, ℕ — это не отдельная сущность, а класс всех функций f (которые мы бы назвали функция от натурального аргумента f : ℕ → A), с которыми может компоноваться любая функция из другого класса всех функций g (которые мы бы назвали натуральнозначными g : B → ℕ). А поскольку функция идентичности id : ℕ → ℕ принадлежит обоим классам, то в целом можно её использовать как каноничный представитель класса и, таким образом, как функцию, которая указывает на тип.
С другой стороны, можно проделать обратный переход (от нетипизированной системы функций к типизированной). Пример такого перехода описан в работе Данны Скотт «Relating Theories of the λ-calculus», в работах Ламбека. Суть состоит в том, что в нетипизированном языке чистых(!) функций можно выделить класс функций A, удовлетворяющих A(x) = A(A(x)) для вообще любого выражения x (вообще любой функции). Для каждой пары таких A и B можно выделить класс функций f таких, что f(x) = B(f(A(x))) для любого x (вообще любого, без ограничений). Можно показать, что каждая функция A ведёт себя как тип, а каждая функция f из второго класса как типизированная f : A → B.
Звучит это очень интересно. Прототип бы ещё увидеть воочию — вообще было бы хорошо.
Есть ли какие-нибудь существующие аналоги подобным системам? Насколько я знаю, в рамках AGI подобные вещи в разных вариантах рассматривались, правда, применимо к решению практических задач.
Контрпримеры навскидку - "README.md", "CHANGELOG.md" файлы в репозитории. Вполне нужны прямо в репозитории, причём changelog вполне может быть сгенерированным (на основе закрытых тасков и тп).
В репозитории должны быть исходные файлы, а артефакты сборки/обработки/генерации на основе исходников следует версионировать отдельно (не абсолютное правило, но рекомендация на уровне «не устанавливайте туалет на кухне»).
README.md не является артефактом.
CHANGELOG.md может быть результатом генерации, но не на основе исходников.
В статье рассматривается именно случай генерации из файла, который, предположительно, уже лежит в репе.
Это если у вас весь тулинг в проекте свой. А если какой-то внешний инструмент использует эти файлы?
Та же ситуация, что и с любыми другими артефактами сборки. Собственно, как было замечено на примере статики, вопрос шире обсуждаемой здесь темы. От себя скажу, что у нас сейчас ещё нет достаточно продвинутой системы версионирования, чтобы единообразно и систематически решать подобные задачи.
Исторически «щ» — лигатура, а «ъ» — такая же гласная, как «ь».
Синхронно «щ» никем не воспринимается как лигатура и ничем по своему статусу не отличается от, скажем, «ц». То же касается «ю» — кто вспомнит, лигатурой каких букв она является?
Впрочем, ничего из этого не относится к предмету вашей дискуссии.
Не надо обобщать. То, что многие не знают, зачем они что-то делают, не значит, что это занятие всем бесполезно.
Между тем специализированная база знаний — это очень полезная вещь для тех, кому надо.
Например, я веду учёт статей, чтобы при необходимости ссылаться на «уважаемые рецензируемые издания» или «достоверные первоисточники». Мол, широкоизвестный в узких кругах факт — это не моя выдумка из головы, вот тут [ссылка] об это написано. И как в посте написано, важно знать, зачем заметка нужна, как и когда (хотя бы в общих чертах) она будет использована.
Программы пишут на ЯП. Любой ЯП, который может использовать homo sapiens, не сломав при этом себе мозг, хорошо ложится на машину Тьюринга и приводит к очень неэффективному машинному коду для КК.
Программы бывают разные и ЯП бывают разные. Если говорить о решении бизнес-задач, то я бы поспорил, что под МТ писать сильно проще, чем под КК. Вы сами-то пробовали хотя бы раз что-нибудь собственно под МТ написать? Для человека удобнее программировать в терминах функций и абстракций (распространение ФП и пр. тому подтверждение), поэтому λ-исчисление кажется более удачной моделью для homo sapiens. Причём
1) если имеющиеся компиляторы/интерпретаторы с GC, JIT и прочим имеют проблемы с производительностью и некоторые решение, то почему КК нельзя?
2) есть попытки построить квантовое λ-исчисление. Ещё видел библиотеку на Idris2, предоставляющую хорошо-типизированный интерфейс к квантовому вычислителю (сам вычислитель, правда, то ли эмулируется за отсутствием оного, то ли просто декларируется).
Если же говорить о низкоуровневом программировании, то ИМХО и программирование на классическом asm/логических вентилях, и программирование на гейтах — занятие специфичное, головоломистое.
Либо надо разрабатывать новую математику с нуля, с новой системой счисления, хорошо приспособоенной к квантовым вычислениям. Поднимать на этой математике богатый набор теорем и алгоритмов.
Так занимаются же этим. Ну то есть я в настоящее время не слежу, но одно время бодро исследовали квантовые алгоритмы, предлагали набор теорем и алгоритмов, как Вы и говорите (ничего, что на Вы?).
Интересны конкретные системы применяемых правил и примеры того, что получается на выходе. Как следует составлять правила, чтобы, например, уровень был интересен для гриндеров? для азартных игроков? для тех или иных конкретных игровых целей?
Основная разница между приведённой мною ссылкой и этой темой в том, что мы хотим получить не только красивую/вычурную карту, но и играбельную, с вызовом и интересом. Какими правилами или их сочетаниями это можно достичь?
Странно, что автор только упоминает наркокартели и азартные игры, но не сравнивает психические, социальные и экономические механизмы, и гос. регулирование.
Между тем, проблема, мягко говоря, не нова. Опыта борьбы и эксплуатации подобной зависимости было достаточно, чтобы проецировать на современность, только форма и масштаб другие.
но все даём честное слово не пользоваться unsafeCoerce и подобным ей функциям.
Поправьте, если не прав, но всякие функции вроде unsafeCoerce являются встроенными хаками системы типов, когда она не может иначе выразить то, что хочется. Значит, нужно отбивать руки всем, кто использует её бездумно, а каждое употребление следует снабжать подробным комментарием, зачем эта функция используется. Запрещать отдельно использовать её для RIO тогда избыточно — достаточно общего правила.
Конечно, писать каждый блок в своей песочнице тяжелее, чем если всё писать в IO.
Не об этом идёт речь. С этим-то вообще никто не спорит.
Проблема в следующем: вот некий модуль (собственный ли, из своей библиотеки, из 3rd-party библиотеки) реализует свои функции через RIO с неким типом Permission; а зависящий от него модуль хочет ещё некоторые операции или дополнительные сорта прав. Что делать? Расширяете RIO для этого модуля, а с модулем-зависимостью как быть? Писать адаптер между первоначальным RIO и новым. Или абстрагировать.
По мнению комментатора выше, абстрагирование должно привести к системе эффектов (кажется, разумный вывод).
И наверное действительно нет смысла писать разные монады для разных блоков. Скорее просто можно ограничить в правах всё приложение
Да. Я, конечно, говорю только о термах. Понятие «значения» требует определения, что мы под ним понимаем: если денотат в модели, то нужна сама модель.
Не знал, что в Агде пытаются убрать аксиому K. Спасибо за тему.
В целом, ожидается, что в «обычных» ЯП тип является «множеством» в смысле HoTT. Просто это не совсем похоже на классические множества.
Я тут ещё вспомнил про constraint type, которые как раз интерпретируются как предикаты на универсуме значений (не разбираюсь в них, ссылок сходу не нашел, хотя упомянутый Картрайт о них говорит). Так что моя категоричность пошаталась. Я не ситх, мне можно.
Не глупо, если учитывать все оговорки. Правильно ли это дидактически? Я усомнился, поэтому высказался.
Лет десять назад я имел такие же представления о типах. Сейчас же у меня вызывают протест многие утверждения из начала статьи, которые формируют неформально понятийную систему у читателя и тем самым определяют путь в своих рассуждениях.
В общепринятой математике множество — это (неформально говоря) объекты, рассматриваемые как один объект. На объектах определено отношение (двуместный предикат) принадлежности, то есть один объект или принадлежит второму, или нет. Если второй объект не множество — всегда нет.
Никакое требование об общем свойстве не накладывается: множество {1, "hello", <кот Василий>} существует. Есть множества, все элементы которого имеют только то общее свойство, что они принадлежат этому множеству.
Множества подчиняются аксиоме объёмности: если два множества состоят из одних и тех же элементов, то это одно и то же множество.
Лучше бы так не делать, потому что типы не обладают вышеперечисленными свойствами множеств. Начнём с того, что нет предиката принадлежности объекта типу. Когда мы пишем x : T, мы не говорим «вот есть объект T, вот есть объект x; кстати, T — это тип; ах да, x принадлежит T». Мы вместо этого говорим или «вот есть выражение x и оно доказуемо по построению имеет T», или «вот переменная x, считать её по определению имеющей тип T».
Многие системы типов устроены так, что никакой объект не может быть экземпляром двух типов. Как в таких условиях говорить об аксиоме объёмности?
Я бы говорил о типах как о метках, которые мы ставим на выражениях. Система типов должна ограничивать нас, и через этого гарантировать, что выполняются какие-то свойства у любого правильно-типизированного выражения.
Простым примером системы типов является система цветных функций.
В качестве антитезы следует согласиться, что типы и множества связаны.
С одной стороны, развитые системы типов (вроде Agda, Coq, HoTT) считают, что множество — это частный вид типов. Но там и множество понимает не общепринято. Поскольку я плохо разбираюсь в интуиционистском варианте теории множеств, призываю малышку @Natasha_Klaus на помощь пояснить за Coq. В HoTT множеством называется тип, у которого любые два экземпляра равны не более чем одним способом.
С другой стороны, для системы типов можно построить модель, в которой каждому типу сопоставляется множество. Впрочем, для программирования более полезны другие виды моделей:
тип как топологическое пространство (точнее, решётка, см. работы Даны Скотт) — позволяет адекватно говорить о функции f : A → B как о непрерывном отображении из A в B, потому что не всякая функция из множества A во множество B может быть программой
тип как идеал — то же, но с поддержкой полиморфизма (дженериков)
тип как интервал — то же, но с нормальной поддержкой полиморфизма и типов-дополнений (т.е. «всё, что не является элементом типа A»)
тип как отношение — для бесплатных теорем, бомба
Прибедняетесь.
Ньютон и Кеплер жили сильно раньше. Коперник — вообще полтысячилетия назад.
Благодарю за ответ. Хотя я и не увидел в нём ссылок на серьёзные работы, сделанные серьёзными людьми, а не только рассуждения анонимуса с неизвестной мне квалификации, на остальные вопросы я получил ответ.
P.S. Наука является деятельность, а любая деятельность обладает целью (или же является бесцельной, но это не случай науки). Субъект ставит (и в этом смысле её имеет) и достигает цель.
Предисловие: я не имею цель с вами спорить. Я аргументированно прокомментировал первоначальный наезд, а сейчас отвечаю за свои слова. Плохо понимаю ваш уровень вовлечённости в лингвистику и в науку в целом, поэтому, возможно, не понял подтекст вашего последнего комментария.
Обобщение сделано в контексте текущей беседы.
Зализняк — известный и признанный учёный в своей области. Поэтому позиция по умолчанию «умного дядьку надо слушать». Любая другая позиция требует пояснений, например:
«я тоже учёный в этой же области и мне виднее»
«более авторитетный учёный выразил несогласие и привёл более убедительные аргументы»
«я никаво ни слушаю, гы-гы-гы»
Вы знаете что-то такое, чего не знаю я, видимо. Что не так с БГ? Что не так с СПИ?
Например, я слушал его лекцию, посвященную СПИ, где он приводит (помимо других) аргумент о порядке слов в перфекте «творил есмь» / «есмь творил», закон которого был открыт в последние десятилетия, но который соблюдается в каждом случае употребления в СПИ. Мне показался аргумент любопытным и достаточно убедительным.
Я выразился неаккуратно. Цель и причина любительского словоблудия — дешевая агитация. Цель науки — изучение того, как наш мир функционирует. Использование же науки лежит вне научного метода, а именно, в смежных прикладных областях человеческой деятельности: инженерии, политике и т.п. Впрочем, без этого (эффективного) использования не было бы спроса на науку, а вместе с тем не было бы и самой науки за ненадобность.
Именно так. Не все ученые бывают правы.
Двойственные чувства вызывает этот комментарий.
С одной стороны, буквально на днях слушал лекцию Зализняка нашего уважаемого А.А., в которой он на вопрос о происхождении слова «счастье» выдал именно эту версию. Это в то время, как лекция была про научный метод и содержала направленную на Фоменко, Задорнова и прочих критику их вольный построений («задорновщины»).
А если предлагается с мнением Зализняка не считаться и «отказаться от использования историко-лингвистических/этимологических построений», то и других учёных тогда можно не слушать, дескать, «я отказался от теоретико-физических построений, чего и всем рекомендую». Странно это. Лично я не рекомендую так делать.
С другой стороны, этот параграф в тексте выглядит инородно. Он как будто бы пытается на основе этимологии вывести современный нам смысл и что-то этим обосновать или дополнить в нелингвистических исследованиях. Это похоже на примеры, которые в упомянутой лекции Зализняк приводил про «укров» и «эт-русков», когда любительская этимология используется для обоснования политических или социальных притязаний.
Почему так скромно получилось?
Не, это, конечно, сильно лучше, чем при стандартном подходе, но всё же скромно.
Если в игре есть экономика, то она устанавливает стоимость предмета. Но для этого она должна быть, включая 1) механику купли-продажи, 2) наличие спроса и предложение (достаточное число игроков). Если игроки разводятся по инстансам и вообще это одиночная РПГ, то экономики не будет.
Полезность метода вот в чём. Допустим, игроделы выпустили прототип игры, собрали данные от тестеров, понерфили-побалансировали характеристики, включая цену, выпустили в народ. А затем начали клепать контент, включая предметы в большом количестве. Какие характеристики установить, чтобы не надо было дополнительно балансировать их?
Предлагается все, кроме цены, взять с потолка, а цену рассчитать по формуле.
Я так вижу практическую значимость статьи. Другое дело, линейное приближение мне кажется плохим. Вон выше уже написали об этом, а кроме того в дуэлях единица урона может отделять победу, так что в тех случаях цена может быть очень нелинейной.
В последних рассуждениях я неявно предположил, что теория обладает экстенсиональностью, т.е. что из f(x) = g(x) для любого x следует f = g. Если это не так, всё усложняется. Замечу, что с этой же проблемой должен был столкнуться автор текста где-то в окрестности следующего абзаца:
Далее мои мысли:
Refined types — это да, подходящая тема. А зависимые типы интересны и сами по себе. А поскольку они требуют некий рантайм на уровне типов, то без явной типизации там очень сложно.
Наконец, автор предложил порассуждать насчёт соответствия Карри-Говарда. В то время как классическая логика старается говорить о высказываниях и задвинуть доказательства под ковёр (например, мало кого интересует, каким доказательством доказана теорема Пифагора во время использования, ведь важно только то, что оно где-то существует), в предложенном подходе будет наблюдаться ровно обратная ситуация: доказательства (=функции) есть, а высказываний (=типов) нет. Впрочем, я плохо представляю, какой логике соответствует система refined types, поскольку с ними не работал вплотную.
P.S. редактор Хабры преждевременно отправил сообщение. Поэтому прошу прощения за резкость в первом абзаце, я перечитал текст и увидел полезные ссылки и сравнения.
Несмотря на низкий интерес сообщества к этой теме, выскажу свои замечания насчёт того, что в определённых кругах всем известно, чтобы интересующиеся могли пойти читать серьёзную литературу, а те, кто в теме, могли соотнести сказанное в этой статье с другими близкими направлениями. Так сказать, восполню отсутствующий в тексте раздел Related Works.
В теории категорий известно, что морфизмы важнее объектов. Применимо к категории типов (как бы она ни определялась) это значит, что функции важнее типов. В частности, существует способ сформулировать понятие категории исключительно на морфизмах, вообще не прибегая к упоминанию объектов (см. МакЛейн «Категории для работающего математика», первые главы). Применимо к категории типов это значит, что можно говорить о типизации и о типах вообще не упоминая типы, а говоря только о функциях. Например, ℕ — это не отдельная сущность, а класс всех функций f (которые мы бы назвали функция от натурального аргумента f : ℕ → A), с которыми может компоноваться любая функция из другого класса всех функций g (которые мы бы назвали натуральнозначными g : B → ℕ). А поскольку функция идентичности id : ℕ → ℕ принадлежит обоим классам, то в целом можно её использовать как каноничный представитель класса и, таким образом, как функцию, которая указывает на тип.
С другой стороны, можно проделать обратный переход (от нетипизированной системы функций к типизированной). Пример такого перехода описан в работе Данны Скотт «Relating Theories of the λ-calculus», в работах Ламбека. Суть состоит в том, что в нетипизированном языке чистых(!) функций можно выделить класс функций A, удовлетворяющих A(x) = A(A(x)) для вообще любого выражения x (вообще любой функции). Для каждой пары таких A и B можно выделить класс функций f таких, что f(x) = B(f(A(x))) для любого x (вообще любого, без ограничений). Можно показать, что каждая функция A ведёт себя как тип, а каждая функция f из второго класса как типизированная f : A → B.
Звучит это очень интересно. Прототип бы ещё увидеть воочию — вообще было бы хорошо.
Есть ли какие-нибудь существующие аналоги подобным системам? Насколько я знаю, в рамках AGI подобные вещи в разных вариантах рассматривались, правда, применимо к решению практических задач.
В репозитории должны быть исходные файлы, а артефакты сборки/обработки/генерации на основе исходников следует версионировать отдельно (не абсолютное правило, но рекомендация на уровне «не устанавливайте туалет на кухне»).
README.md не является артефактом.
CHANGELOG.md может быть результатом генерации, но не на основе исходников.
В статье рассматривается именно случай генерации из файла, который, предположительно, уже лежит в репе.
Та же ситуация, что и с любыми другими артефактами сборки. Собственно, как было замечено на примере статики, вопрос шире обсуждаемой здесь темы. От себя скажу, что у нас сейчас ещё нет достаточно продвинутой системы версионирования, чтобы единообразно и систематически решать подобные задачи.
Исторически «щ» — лигатура, а «ъ» — такая же гласная, как «ь».
Синхронно «щ» никем не воспринимается как лигатура и ничем по своему статусу не отличается от, скажем, «ц». То же касается «ю» — кто вспомнит, лигатурой каких букв она является?
Впрочем, ничего из этого не относится к предмету вашей дискуссии.
Не надо обобщать. То, что многие не знают, зачем они что-то делают, не значит, что это занятие всем бесполезно.
Между тем специализированная база знаний — это очень полезная вещь для тех, кому надо.
Например, я веду учёт статей, чтобы при необходимости ссылаться на «уважаемые рецензируемые издания» или «достоверные первоисточники». Мол, широкоизвестный в узких кругах факт — это не моя выдумка из головы, вот тут [ссылка] об это написано. И как в посте написано, важно знать, зачем заметка нужна, как и когда (хотя бы в общих чертах) она будет использована.
Программы бывают разные и ЯП бывают разные. Если говорить о решении бизнес-задач, то я бы поспорил, что под МТ писать сильно проще, чем под КК. Вы сами-то пробовали хотя бы раз что-нибудь собственно под МТ написать? Для человека удобнее программировать в терминах функций и абстракций (распространение ФП и пр. тому подтверждение), поэтому λ-исчисление кажется более удачной моделью для homo sapiens. Причём
1) если имеющиеся компиляторы/интерпретаторы с GC, JIT и прочим имеют проблемы с производительностью и некоторые решение, то почему КК нельзя?
2) есть попытки построить квантовое λ-исчисление. Ещё видел библиотеку на Idris2, предоставляющую хорошо-типизированный интерфейс к квантовому вычислителю (сам вычислитель, правда, то ли эмулируется за отсутствием оного, то ли просто декларируется).
Если же говорить о низкоуровневом программировании, то ИМХО и программирование на классическом asm/логических вентилях, и программирование на гейтах — занятие специфичное, головоломистое.
Так занимаются же этим. Ну то есть я в настоящее время не слежу, но одно время бодро исследовали квантовые алгоритмы, предлагали набор теорем и алгоритмов, как Вы и говорите (ничего, что на Вы?).
Интересны конкретные системы применяемых правил и примеры того, что получается на выходе. Как следует составлять правила, чтобы, например, уровень был интересен для гриндеров? для азартных игроков? для тех или иных конкретных игровых целей?
Основная разница между приведённой мною ссылкой и этой темой в том, что мы хотим получить не только красивую/вычурную карту, но и играбельную, с вызовом и интересом. Какими правилами или их сочетаниями это можно достичь?
Благодарю за статью. Интересно было бы почитать про выработанную грамматику и типы приписываемых к вершинам и рёбрам семантических признаков.
На всякий случай (не ради рекламы, а чтоб польза была) оставлю ссылку на статью о сходной идеи с внушительной библиотекой разных грамматик: Стохастический язык программирования на основе алгоритмов Маркова
Странно, что автор только упоминает наркокартели и азартные игры, но не сравнивает психические, социальные и экономические механизмы, и гос. регулирование.
Между тем, проблема, мягко говоря, не нова. Опыта борьбы и эксплуатации подобной зависимости было достаточно, чтобы проецировать на современность, только форма и масштаб другие.
Что насчёт ключевых знаков? Как в этом случае размечаются ноты со случайной альтерацией и без? Бекар ставится автоматически?
Поправьте, если не прав, но всякие функции вроде
unsafeCoerceявляются встроенными хаками системы типов, когда она не может иначе выразить то, что хочется. Значит, нужно отбивать руки всем, кто использует её бездумно, а каждое употребление следует снабжать подробным комментарием, зачем эта функция используется. Запрещать отдельно использовать её дляRIOтогда избыточно — достаточно общего правила.Не об этом идёт речь. С этим-то вообще никто не спорит.
Проблема в следующем: вот некий модуль (собственный ли, из своей библиотеки, из 3rd-party библиотеки) реализует свои функции через
RIOс неким типомPermission; а зависящий от него модуль хочет ещё некоторые операции или дополнительные сорта прав. Что делать? РасширяетеRIOдля этого модуля, а с модулем-зависимостью как быть? Писать адаптер между первоначальнымRIOи новым. Или абстрагировать.По мнению комментатора выше, абстрагирование должно привести к системе эффектов (кажется, разумный вывод).
Прощай, модульная разработка.