Написание приложений JavaScript, которые ведут себя так, как вы хотите, сложно. Поскольку JavaScript динамически типизирован, программист обычно не получает от интерпретатора указания, если в его программе есть ошибка.

В этой статье я собираюсь продемонстрировать способ разработки приложений JavaScript с использованием функционального языка программирования с зависимой типизацией Idris. Зависимый тип - это тип, определение которого зависит от другого значения. Вы можете определять очень точные типы в Idris и обнаруживать множество ошибок во время компиляции. Идрис особенно хорош для написания программ на основе конечных автоматов. Я покажу, как создать простую боевую игру, используя Идрис, и внутренне смоделировать игру как конечный автомат. Благодаря мощным возможностям Idris по проверке типов, мы определим конечный автомат, который гарантирует, что возможны только легальные переходы между состояниями в соответствии с определенными нами правилами.

Для этой задачи мы будем использовать следующие инструменты: Idris, JavaScript и HTML, а также мобильный фреймворк Onsen UI для стилизации. Мы напишем всю логику приложения в Idris, а затем с помощью флага компилятора --codegen javascript скомпилируем код в файл JavaScript, который затем можно будет использовать, как в любом обычном веб-приложении.

Сначала мы создадим файл с именем Battle.idr, в который будем писать весь код Идриса. Это скомпилировано с помощью:

idris --codegen javascript -o battle.js Battle.idr

Эта команда компилирует код Идриса и выводит файл JavaScript с именем battle.js.

Игра

(Полный исходный код этой статьи доступен здесь.)

Игра представляет собой простую текстовую игру, в которой игрок должен победить врага, используя разные движения. Игрок может сделать три разных хода: удар, пинок и магия. У врага тоже есть эти ходы. Игрок и противник по очереди делают ходы, пока у одного из них не кончится здоровье. Если они оба используют одно и то же движение, ни один из них не пострадает. Если один использует удар ногой, а другой - удар кулаком, бьющий игрок теряет одно очко здоровья. Если один использует удар, а другой - магию, пользователь магии теряет одно очко здоровья. Если один боец ​​использует магию, а другой - удар ногой, пинающий игрок теряет одно очко здоровья.

Игра может находиться в одном из четырех состояний в любой момент времени:

  • Безопасно: игра еще не началась.
  • Not Dead: игра началась, и ни один из игроков не выиграл.
  • Мертвый: ваше здоровье упало до нуля. Вы проиграли игру.
  • Выиграли: здоровье вашего оппонента упало до нуля. Вы выиграли игру.

Мы можем представить эти состояния в Идрисе, определив новый тип:

Первая строка определяет новый тип, а следующие строки определяют конструкторы, которые создают значения этого типа. Safe, Dead и Won - конструкторы, не принимающие аргументов. NotDead берет: health, текущее здоровье игрока; и enemy, текущее здоровье оппонента, оба являются натуральными числами.

Операции

Теперь, когда у нас есть состояния нашей игры, нам нужно определить операции для перехода между состояниями. Идрис позволяет нам выразить, в каком состоянии должна находиться игра, прежде чем мы сможем выполнить операцию, и в каком состоянии игра должна находиться после выполнения операции. Поэтому мы можем сделать буквально невозможным выполнение операции, когда это было бы недопустимо. Например, мы можем гарантировать, что невозможно перейти в состояние Won, то есть выиграть игру, если здоровье врага не равно нулю. Определим тип операции:

BattleCmd - это тип всех операций, которые могут изменить состояние игры. Его первый параметр - это тип значения, возвращаемого командой. Второй параметр - это предварительное условие - состояние, в котором должна находиться игра, прежде чем операция может быть выполнена. Его третий параметр - постусловие - состояние, в котором игра должна оставаться после завершения выполнения команды. Фактически, этот параметр является функцией, которая принимает значение, возвращаемое командой, и сама возвращает состояние постусловия. Это полезно, потому что мы можем захотеть войти в другое состояние в зависимости от того, что было возвращено командой. Теперь мы можем определить некоторые операции:

Давайте рассмотрим их более внимательно:

  • Start переводит игру из состояния Safe в состояние NotDead. NotDead инициализируется начальным здоровьем игрока и начальным здоровьем врага, оба из которых равны 10. Start не возвращает значения, поэтому возвращаемый тип - (), тип отряда.
  • Die имеет NotDead 0 _ в качестве предварительного условия, что означает, что для запуска Die игра должна находиться в состоянии NotDead, а здоровье игрока должно быть равно нулю. После выполнения игра должна находиться в состоянии Dead.
  • Win требует, чтобы здоровье игрока было больше нуля (S k означает преемник некоторого натурального числа k - другими словами, некоторое число больше нуля) и чтобы здоровье врага было равно нулю. Если это условие выполнено, Win может быть выполнено, и игра перейдет в состояние Won.

Остальные три команды охватывают три хода, которые игрок может сделать, чтобы атаковать врага. Каждый требует, чтобы состояние было NotDead и чтобы у врага и игрока было немного оставшегося здоровья. Значение, возвращаемое этими командами, имеет тип EnemyResponse и представляет ход, который враг выбирает сделать в ответ на игрока. Постусловие - это функция, которая принимает этот ответ и определяет, каким должно быть состояние после этого. Эти три функции очень похожи, поэтому в качестве примера мы рассмотрим только функцию Kick:

  • Если ответ врага был Kick, то оба игрока использовали один и тот же ход, поэтому здоровье обоих игроков должно оставаться одинаковым.
  • Если противник использовал Punch, здоровье врага должно уменьшиться на единицу, а здоровье игрока должно остаться прежним, потому что по правилам нашей игры удары ногами лучше, чем удары руками.
  • Если противник использовал Magic, здоровье игрока падает на единицу, а здоровье врага остается прежним, потому что магия лучше ударов ногами.

Для удобства мы также определили Log для печати сообщений, а также Pure и >>=, которые позволяют нам легко писать последовательности команд, используя do-notation Идриса. Давайте сделаем это:

Эта функция определяет последовательность команд, которые: запускают игру; логировать сообщение о том, что игра началась. Обратите внимание, что если мы попытаемся сделать следующее, Идрис выдаст ошибку при проверке типа:

Причина ошибки в том, что в точке, где мы пытаемся использовать Win, здоровье врага равно 10, а не нулю, поэтому предварительное условие Win не выполняется. Другими словами, Идрис обнаружил ошибку в программе во время компиляции!

Пользовательский интерфейс

До сих пор мы определили возможные состояния игры и команды для перехода между этими состояниями. Давайте ненадолго выпрыгнем из земли Идриса и создадим пользовательский интерфейс, используя HTML с пользовательским интерфейсом Onsen.

Во-первых, базовая HTML-страница с импортом для пользовательского интерфейса Onsen, наша скомпилированная программа Idris и файл с некоторыми вспомогательными функциями JavaScript, которые мы определим позже:

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

Для кнопок мы будем использовать компонент ons-button. Он работает так же, как и обычный button компонент. Чтобы стили работали правильно, они должны быть определены внутри тега ons-page. Кнопки должны быть закреплены внизу страницы - для этого мы можем использовать ons-bottom-toolbar:

Вверху страницы будет отображаться статус. Чтобы исправить текст в верхней части экрана, нужно использовать ons-toolbar:

Наконец, нам нужен способ отображения журнала сообщений, которые будут генерироваться во время работы игры. Мы будем использовать компонент ons-list для хранения всех сообщений, где каждое сообщение - это ons-list-item. Позже мы будем динамически добавлять сообщения в список по мере их создания с помощью JavaScript. На данный момент тело пользовательского интерфейса должно быть следующим:

Управление государством

Теперь, когда у нас есть интерфейс и абстрактная логика игры, нам нужно объединить две части.

Состояние JavaScript

Во-первых, нам нужно где-нибудь сохранить состояние игры в виде объекта JavaScript. В других приложениях конечных автоматов в Идрисе, таких как приложение командной строки, нам не нужно явно писать состояние где-либо, потому что программа выполняется в цикле и, следовательно, может «удерживать» состояние. Однако JavaScript немного сложнее, потому что он управляется событиями. Когда пользователь нажимает кнопку, нам нужно запустить функцию Idris, которая повлияет на состояние игры, но эта функция завершится, когда работа будет выполнена, в отличие от приложения командной строки, которое будет зацикливаться и ждать дополнительных данных. Из-за этого нам нужно удерживать состояние где-то между вызовами функций и убедиться, что мы правильно читаем и записываем состояние в начале и в конце каждой функции.

Итак, давайте сначала создадим файл helpers.js для хранения конкретного состояния игры. В него мы добавим следующее:

Это состоит из трех частей:

  • state, объект, содержащий текущее состояние игры. Он инициализируется как пустой объект.
  • Функции для управления state. Функции, которые записывают информацию о состоянии, добавляют атрибуты к объекту состояния, соответствующие имени текущего состояния (например, "DEAD", "NOTDEAD"), и любую дополнительную информацию, необходимую для воссоздания состояния в Идрисе (например, здоровье игрока в состоянии NotDead).
  • Объект верхнего уровня gameState, который предоставляет все функции для управления состоянием. Объект state является частным для этой функции верхнего уровня, поэтому конкретное состояние игры не может быть случайно изменено другой функцией.

Звонок из Идриса

Затем нам нужен способ вызова функций, определенных в helpers.js из кода Идриса.

Мы можем вызывать функции JavaScript из кода Идриса, используя Интерфейс внешних функций Идриса (FFI). Для этого есть специальная функция foreign. Вот функция onClick, которая принимает селектор запросов JavaScript как строку и функцию обратного вызова и добавляет прослушиватель событий щелчка к выбранному элементу:

Важными частями здесь являются: второй аргумент foreign, строка, содержащая запускаемый JavaScript; и третий аргумент, который является типом вызываемой функции JavaScript. В строке кода JavaScript специальные символы %0 и %1 означают замену нулевого и первого аргументов соответственно.

Нам нужно добавить функцию-оболочку для каждой функции в helpers.js:

Сохраняя это в безопасности

Теперь у нас есть способ манипулировать конкретным состоянием игры с помощью функций Идриса и сохранять его между вызовами функций. Похоже, это именно то, чего мы не хотим в чистом функциональном языке программирования, но в данном случае это неизбежное зло. Тем не менее, мы можем, по крайней мере, попытаться быть более безопасными в использовании этих функций управления состоянием, используя инструменты, которые предоставляет нам Идрис.

Мы хотим убедиться, что каждый раз, когда мы выполняем какое-либо действие, которое манипулирует состоянием игры, мы не забываем: читать состояние; запустить действие игры в этом состоянии; и запишите получившееся игровое состояние. Мы можем добиться этого, добавив несколько новых состояний в BattleState и команды в BattleCmd:

  • Ready - это состояние системы до считывания каких-либо данных о состоянии игры.
  • Done - это состояние после того, как состояние игры было записано обратно.
  • ReadError вводится, если возникла проблема с чтением состояния игры.
  • ReadState пытается прочитать состояние игры. Если это было успешно, следующим состоянием будет состояние загрузки; в противном случае он переходит в состояние ReadError.
  • WriteState записывает состояние обратно и переходит в Готово.
  • GiveUp может быть выполнен только в ReadError и переходит в Done.

Обратите внимание, что мы также определили новый тип Writable. Этот тип используется для отделения состояний, используемых для представления игры, таких как Dead и NotDead, от состояний, используемых для чтения и записи, таких как Ready и Done. Мы используем Writable в определениях ReadState и WriteState, чтобы убедиться, что мы никогда случайно не запишем или не прочитаем состояние игры как нечто бессмысленное, например Ready. Если у вас есть значение типа Writable someState, это означает, что someState - это состояние, которое представляет, что происходит в игре, а не состояние, которое представляет, где программа находится в процессе чтения / записи. Мы также должны определить экземпляр Show для Writable, чтобы мы могли легко получить строковое представление состояния игры:

С этими новыми состояниями мы можем писать команды типа:

BattleCmd () Ready (const Done)

Любое значение этого типа описывает последовательность действий, которые переходят из состояния Ready в состояние Done. Поскольку единственный способ перейти от Ready - вызвать ReadState, а единственный способ перейти к Done - вызвать WriteState, значения этого типа всегда будут сначала читать состояние, а писать состояние последним.

Действия в реальном мире

На данный момент у нас есть некоторые функции Idris, которые вызывают функции JavaScript, которые манипулируют постоянным состоянием, и способ определения последовательностей абстрактных команд, которые гарантируют, что мы не забываем правильно читать и записывать состояние, но мы не сказали, что на самом деле должно произойти. при выполнении команды. Для этого мы определим функцию runCmd', которая переводит значения типа BattleCmd в операции ввода-вывода. Здесь могут пригодиться вспомогательные функции JavaScript, определенные в предыдущем разделе:

Для некоторых команд, которые перемещаются между состояниями игры, таких как Start и Die, нет необходимости выполнять операции ввода-вывода, поэтому правая часть этих уравнений - pure (), что фактически означает «ничего не делать». Punch, Kick и Magic требуют, чтобы мы возвращали случайно сгенерированный ход для врага, поэтому мы вызываем enemyResponse, одну из вспомогательных функций JavaScript, заключенных в Идрис. Команды, относящиеся к состоянию чтения и записи, также вызывают вспомогательные функции.

У нас есть все необходимое, чтобы заставить программу работать в реальном мире. Одна вещь, которую мы не сделали, - это использовать состояния Ready и Done, чтобы гарантировать, что действия ввода-вывода, которые мы получаем от runCmd', всегда включают состояние чтения и записи в их голове и хвосте. Мы можем добиться этого, спрятав runCmd' внутри блока where другой функции runCmd:

Теперь единственный способ превратить последовательности команд в действия реального мира - это включить в последовательность действия, которые читают и записывают состояние.

Команды пользователя

Теперь давайте определим тип для всех различных команд, которые может выполнять пользователь. Для каждой кнопки в пользовательском интерфейсе есть одна команда:

Теперь мы можем создать функцию, которая принимает пользовательскую команду и возвращает последовательность действий, которые должны быть выполнены для этой команды:

(В правой части каждого уравнения есть символ «?», Который указывает на «дыру» в Идрисе - значение, которое временно остается неопределенным во время разработки.)

В этом приложении нет строгой необходимости беспокоиться о типе команды пользователя. Как я сейчас покажу, Input используется только для связывания слушателя действия с функцией обратного вызова, и мы могли бы просто связать их напрямую. Но если мы используем Input, мы четко указываем, какие именно действия может выполнять пользователь. Что еще более важно, мы можем проверить, что actions является общим, т.е. имеет четко определенное поведение для каждого значения Input, поэтому мы знаем, что каждой пользовательской команде соответствует BattleCmd.

Как бить, бить и использовать магию

В последнем разделе мы оставили дыры для функций, запускаемых, когда пользователь нажимает кнопки удара, удара или магии, поэтому давайте вернемся и определим их как doKick, doPunch и doMagic. Эти три функции очень похожи, поэтому я рассмотрю только doKick подробно.

  • Just (state ** w) <- ReadState | Nothing => GiveUp считывает состояние игры из объекта JavaScript или переходит к GiveUp, если произошла ошибка.
  • Совпадаем по состоянию с case state of. Если состояние не NotDead с ненулевым здоровьем игрока и врага, запишите состояние обратно и выйдите.
  • Мы распечатываем сообщение с Log "you kicked!", а затем фактически выполняем команду Kick, фиксируя ее возвращаемое значение - атаку, которую использовал противник - в res.
  • Совпадаем по res.
  • Если res был ударом ногой, ни один из игроков не должен терять здоровье (здесь у нас нет выбора; это обеспечивается системой типов), поэтому мы регистрируем, что противник нанес удар, показываем состояние игры и пишем состояние обратно к объекту JavaScript. Обратите внимание, что для вызова ShowStatus и WriteState нам нужно передать Writable значение состояния, которое мы хотим показать или записать. Это гарантирует, что мы сможем писать или показывать только состояние игры.
  • Если res был ударом, противник теряет одно очко здоровья (опять же, нам не нужно здесь ничего делать, потому что это изменение состояния закодировано в типе). Проверяем, не упало ли здоровье врага до нуля; если это так, мы переходим в состояние Won с помощью команды Win. В любом случае состояние отображается в пользовательском интерфейсе и записывается обратно в объект JavaScript.
  • Если res был магией, на этот раз игрок теряет одно очко здоровья, и мы проверяем, упало ли здоровье игрока до нуля. Если это так, мы вызываем Die, чтобы перейти в состояние Dead. Как всегда, состояние отображается в пользовательском интерфейсе и записывается обратно в объект JavaScript.

Щелкнув все вместе

Теперь осталось только добавить несколько дополнительных функций, чтобы склеить все вместе, и основную функцию, чтобы мы могли запустить программу.

Есть еще несколько вспомогательных функций, которые нужно добавить в helpers.js:

Обратите внимание, что они определены вне функции gameState - этим новым функциям не требуется доступ к состоянию игры.

Затем есть соответствующие обертки Idris для этих новых функций:

Наконец, нам понадобятся эти три функции, чтобы выполнить некоторую настройку в начале игры:

  • doAction связывает пользовательскую команду с соответствующими действиями ввода-вывода.
  • setUp создает начальное постоянное состояние и добавляет слушателей к кнопкам действий пользователя в пользовательском интерфейсе для каждого из различных движений, которые пользователь может выполнить.
  • main запускает setUp после того, как все было инициализировано.

Теперь, если мы скомпилируем Battle.idr и откроем battle.html в браузере, мы сможем увидеть готовое приложение. Попробуйте сыграть в игру. Вы заметите, что после того, как игра была выиграна или проиграна, три кнопки действий больше ничего не делают - точно так, как мы определили в командах абстрактного конечного автомата!

Заключение

Написание приложений JavaScript с использованием Idris, безусловно, требует более предварительной работы, но я думаю, что это более чем компенсируется возросшей уверенностью программиста в правильности своего приложения. На то, чтобы понять, как написать этот пример программы, у меня ушло больше времени, чем если бы я написал ее на простом JavaScript, но у меня также не было никаких серьезных ошибок. В том редком случае, когда мне удавалось получить ошибки через средство проверки типов, обычно это происходило из-за того, что я что-то напутал в HTML или JavaScript. Небольшая боевая игра в этой статье - это всего лишь игрушечная программа, но я надеюсь, что я продемонстрировал один из способов использования Идриса для создания приложений JavaScript, которые делают то, что вы от них хотите.