Pull to refresh
35
0

Программист-теоретик

Send message

Если в игре есть экономика, то она устанавливает стоимость предмета. Но для этого она должна быть, включая 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 и новым. Или абстрагировать.

По мнению комментатора выше, абстрагирование должно привести к системе эффектов (кажется, разумный вывод).

И наверное действительно нет смысла писать разные монады для разных блоков. Скорее просто можно ограничить в правах всё приложение

Прощай, модульная разработка.

У darcs были проблемы с подлежащей теорией. Они там раза два меняли коней на переправе, переписывая основные компоненты чуть ли не с нуля, чтобы закрыть неконсистентность. У pijul в этом плане больше шансов.

Как мне кажется, основная проблема darcs была в том, что люди были не очень готовы к нему: когда darcs стал стабильным, общий запрос был на СКВ ревизионного типа, потому что все СКВ того времени были такими.

При этом я обожаю darcs.

Во-первых, на картинке показаны два примера: первый (верхний) Истина+Ложь=Истина, второй (нижний) Ложь+Истина=Ложь, а должно быть как в оригинале Ложь+Ложь=Ложь.

Во-вторых, очень раздражает оригинальный стиль изложения и обилием воды и бесполезных цитат-вставок. Переводчик не хочет начать выбрасывать этот мусор? И ему работы меньше будет, и текст объективно от этого станет лучше. Впрочем, и за такой перевод спасибо.

В-третьих, я не понял технический аспект осуществления вычисления. Как это выглядит? Есть видео, например? Чтоб было понятно, что эта часть складывания оригами соответствует программированию, а вот эта часть — вычислению.

Я так понимаю, статья рассчитана на тех, кто с логикой плохо знаком. Кажется, вполне очевидные вещи написаны.

Впрочем, если придираться, я бы поспорил насчёт абзаца

Давайте покажу на примере. Для этого вернёмся к задачке из начала.

Не обоснован переход между тем, что говорится выше (про выводимость/доказуемость высказываний) и ниже (про общезначимость в мира/моделях). Классики, конечно, клали штопор на различие, а конструктивисты бы поспорили в логичности приведённых рассуждений. И, кстати, не то, чтоб совсем безосновательно.

Конструктивист бы сказал, что в задаче про девушек недостаточно данных. Впрочем, если замужество Светланы разрешимо, то задача решается (причём без рассмотрения «миров»). А разрешимо ли оно — вопрос к предметной области. Сожительство считается замужеством? Давняя или недавняя смерть мужа? Его кома? День развода? День свадьбы? Регистрация замужества на территории непризнанного государства? В загсе, который не признаётся церковью (как в нач. XX века)? В церкви, которую не признаёт государство? А классику плевать, он рассматривает «миры», в которых

каждая из них может быть как замужем, так и незамужней

в смысле «в половине миров она замужем, а в другой половине — незамужняя».

Во французском wifi произносится как вифи (пример). Так что кому хаханьки, а кому нормативное произношение.

Лично меня цепляет слово «латекс» применимо к системам вёрстки, а не к материаловедению.

А что с нодой не так-то? Как ещё в беглой русской речи (когда происходит оглушение звонких и редукция почти всего в конце слов) произнести Node или NodeJS так, чтобы поняли; чтобы не спутали с note, no, No-JS или чем-то ещё?

В начале я старался произносить чётко с английским выговором, но всё равно переспрашивали. Потом говорил «Ноуд, Эн-Оу-Ди-И-и-и-и». А потом забил, ведь «нода» хорошо произносится и, что примечательно, такой способ заимствования (вставлять «а» в окончание) вполне в духе русского языка.

По моему мнению, централизованные решения проблем (вроде глобального рейтинга узлов, чёрных списков, всеобщего бана) в распределённых системах имеют характерные для централизованных систем недостатки и снижают преимущества распределённых систем на порядок.

Вместо этого, почему бы не вести распределённый реестр источников/краулеров с пометкой «доверенный/спам-бот». Версионировать его в распределённой СКВ (подходит ли git для этого?). Когда обнаружится, что «слово + сайт» — фейковое, можно посмотреть цепочку: кто краулер, кто добавил его в реестр.

Как вы понимаете, у меня proof-of-concept нет, всё это пустые слова на настоящий момент, но я сторонник мнения, что децентрализацию нужно проводить до конца.

1
23 ...

Information

Rating
3,915-th
Location
Красноармейск, Донецкая обл., Украина
Registered
Activity