A game in a pure language (part 2): state

栏目: IT技术 · 发布时间: 4年前

内容简介:Myfirst post about this project was a general introduction and an overview of my impressions of Idris. In this one, I’ll go over some elementary facilities that enable creating stateful systems like games in a pure language. Also I finally published the ga

Myfirst post about this project was a general introduction and an overview of my impressions of Idris. In this one, I’ll go over some elementary facilities that enable creating stateful systems like games in a pure language. Also I finally published the game’s source code: github.com/corazza/game-idris (it’s last been tested in Idris 1.3.1).

A pure language has no implicit state or side effects (i.e. you can’t just take user input, mutate a variable such as health , and blit things to the screen directly), while games are programs that seem to be all about state, side effects, interactivity… Well, it turns out that explicit state and side effects, which pure languages can operate with, are good enough! But I didn’t really know much about that when starting this project.

I had some minimal Haskell knowledge, and while the Idris book does go over state management, the scope is mostly simple exercises where your state can be represented as a single Nat or something like that: definitely not a large system with multiple moving parts coming in and out of existence. The accent was definitely on correctness rather than performance and practical implementations.

Still though, those exercises really do form the basic building blocks that you need to understand before dealing with larger systems, so I’ll present two of them from the Idris book, along with Control.ST which is an out-of-the-box facility putting those ideas into practice:

Example 1: basic stateful operations in Haskell / Idris

A good starting example is a tree-labelling program, where the goal is to label each node of a binary tree in some order:

A game in a pure language (part 2): state

This is a good way to introduce state in functional programming because at first you’d naively reach for a stateless recursive solution to the problem. Which of course, exists and works, but is a bit convoluted and harder to scale into larger solutions:

treeLabelWith : (lbls : Stream labelType) ->
                (tree : Tree a) ->
                (Stream labelType, Tree (labelType, a))
treeLabelWith lbls Empty = (lbls, Empty)
treeLabelWith lbls (Node left val right)
  = let (lblThis :: lblsLeft, left_labelled) = treeLabelWith lbls left
        (lblsRight, right_labelled) = treeLabelWith lblsLeft right
          in
        (lblsRight, Node left_labelled (lblThis, val) right_labelled)

The problem here is in the return type, (Stream labelType, Tree (labelType, a)) : we don’t just return the labeled tree, but a new stream of labels. This is necessary because when labelling the left child recursively, we don’t know how many labels were consumed, so when resuming to label the root and the right child, we needed to be explicitly told where to continue from by the left-child recursive call. Of course, you can wrap this later, but the implementation isn’t really elegant.

A better solution would be to use Control.Monad.State in order to weave in an explicitly-stateful list of labels, allowing us to write nicer-looking code:

--              input  -> State (state type)       (return type of stateful computation)
treeLabelWith : Tree a -> State (Stream labelType) (Tree (labelType, a))
treeLabelWith Empty = pure Empty
treeLabelWith (Node left val right)
  = do left_labelled <- treeLabelWith left
       (this :: rest) <- get
       put rest
       right_labelled <- treeLabelWith right
       pure (Node left_labelled (this, val) right_labelled)

treeLabel : Tree a -> Tree (Integer, a)
treeLabel tree = evalState (treeLabelWith tree) [1..]

Now the implementation of labelling is more readable, because we don’t have to drag the state (labels) around explicitly. This is just an example of composing stateful operations, and it may appear that not much was achieved by modifying this isolated labelling function, however in a larger program writing this kind of monadic code is the only practical way to compose the system.

Example 2: verified state transitions

Imagine you’re programming an ATM. Such a machine obviously needs a high degree of assurance in its code’s correctness, so that you can’t e.g. give out money before the PIN has been checked, don’t eject a card when there is none inserted, etc. The cost of getting these state transitions wrong can be high, so in most other languages you’d invest in a variety of methods to proof it most of which in the end cash out in expensive work-hours. But whatever methods you eventually end up using, they will be lacking in a crucial aspect: they will never give complete assurance about the implementation, the code itself . The compiler will detect some bugs, the runtime, if it has a larger presence, will help in handling certain kinds of errors, but at the end of the day imperative languages and most pure functional ones rely on the programmer to correctly write the algorithm and differ only in degree with regards to the amount of help offered.

But Idris is different. Instead of trying to be really sure the implementation of your ATM is correct through external methods, dependent typing in Idris lets you encode state transitions in types , meaning that the compiler can formally prove, for each of your functions that handles the ATM’s state, that it does so according to rules that had been laid out before. This means that it’s impossible to compile code in which some minor, misplaced call in an infrequent branch messes up the ATM state.

Here’s how these state transitions are specified:

PIN : Type
PIN = Vect 4 Char

data ATMState = Ready | CardInserted | Session

data PINCheck = CorrectPIN | IncorrectPIN

-- commands that are composed into ATM-handling programs:
-- READ AS     return type -> begin state -> f computing the resulting state -> give an ATM command
data ATMCmd : (ty : Type)  -> ATMState    -> (ty -> ATMState)                -> Type where
  InsertCard  : ATMCmd  ()  Ready         (const CardInserted)
  GetPIN      : ATMCmd  PIN CardInserted  (const CardInserted)

  CheckPIN    : PIN -> ATMCmd PINCheck CardInserted
                          (\check => case check of
                                          CorrectPIN => Session
                                          IncorrectPIN => CardInserted)

  -- ... other commands, for example logging ...

The above snippet is part of a definition of a data type whose values are ATM commands, which are composed into ATM programs. The line GetPIN : ATMCmd PIN CardInserted (const CardInserted) means that GetPIN is a value representing an ATM command which returns a PIN, begins in the state CardInserted , and no matter what ( const ) remains in the CardInserted state. Now, were you to call (bind, more accurately) this GetPIN value while the ATM was in Ready state, the program wouldn’t compile!

CheckPIN is more interesting, however, because it showcases more of the mechanism enabling verification of complex state transitions.

CheckPIN : PIN -> ATMCmd PINCheck CardInserted
                    (\check => case check of
                                    CorrectPIN => Session
                                    IncorrectPIN => CardInserted)

Firstly, CheckPIN is a function which takes a PIN and returns an ATM command. That ATM command itself returns a PINCheck value–either CorrectPIN or IncorrectPIN , and has to start in the CardInserted state. Where things get interesting is that last constructor argument. In the prior two ATM commands, this was just const some_state , meaning a function which always evaluated to the same specified ATM state. The reasoning there was obvious: inserting a card gets us into the CardInserted state no matter what, and getting the PIN never changes the state from CardInserted .

But CheckPIN is different, in the sense that it represents a conditional state transition! Whether the ATM remains in the CardInserted state or moves into the Session state depends on the resulting PINCheck ! The practical result of this is that you are forced to match on the result, and the different branches of the match expression will have different types depending on this value: if you try executing a command that expects the operation to have succeeded, it wouldn’t typecheck unless it’s in the correct branch.

Here’s a much less complicated snippet which shows how this ATMCmd type is used:

atm : ATMCmd () Ready (const Ready)
atm = do InsertCard
         pin <- GetPIN
         pinOK <- CheckPIN pin
         case pinOK of
               CorrectPIN => do cash <- GetAmount
                                Dispense cash
                                EjectCard
               IncorrectPIN => EjectCard

I believe this code is rather beautiful and simple: there are no implementation details whatsoever, only logic–correct logic! All ATM programs care about is that they’re values of the type ATMCmd , that is, that they’re composed in a way that respects certain rules defined in their type.

Now all that is left is defining the implementation of ATMCmd values, a function called runATM for example, which takes an ATMCmd and ‘runs’ it. ‘Run’ in this context could mean several things, but in this example it means a mapping from ATMCmd ty in out to IO ty . But it could also mean a mapping from ATMCmd ty in out to ATM_internal ty , where ATM_internal is some special monad for communicating with the actual ATM machinery in a restricted, controlled manner. An example runATM :

runATM EjectCard = putStrLn "Card ejected"
runATM GetPIN = do putStr "Enter PIN: "
                   readVect 4
-- ...

That’s all there is to the implementation! The EjectCard case is especially curious, because you’d expect something that actually changes a state. But that’s part of the type specification! So the only thing left for the implementation is displaying a message. (In the real-world scenario we’d also call a function that would cause the ATM to eject the card.)

This is separation of logic and implementation to a quite high degree, and is a frequent pattern in stateful Idris code. When I wrote the scripting part of the game, I used something like this: there is a RuleScript monad which is simple and nice to write in, and there is a runScript function that maps its values into some lower-level representations (game state changes).

STrans and ST

The last exercise was about creating a custom type in order to model a stateful system and operations on it. That is an oft-repeated pattern, and STrans and its helper type constructor ST generalize it.

Lets look at ATMCmd again to see which parts generalize.

data ATMCmd : (ty : Type) -> ATMState -> (ty -> ATMState) -> Type where

It is a type constructor taking the following arguments:

  1. ty : Type : the return type of the ATM operation
  2. ATMState : a value of this type ( Ready | CardInserted | Session ) that represents the initial state the ATM is in
  3. (ty -> ATMState) : a function from the return type to ATMState , representing how the state of the ATM changes depending on the result of the operation

The result is a Type . For example ATMCmd () Ready (const CardInserted) is the type of the value InsertCard , which means that InsertCard :

Ready
CardInserted

The function (well, value) atm has type ATMCmd () Ready (const Ready) : it is the main ATM program, and its type means that an ATM always begins and ends in a Ready state–that this is actually respected by our implementations is guaranteed by the Idris compiler.

Again–what generalizes here? A lot! It turns out that many stateful programs can be composed from values that represent operations of a similar kind: they can return a value, there are preconditions (for example an ATMState ), and a function representing the postconditions of the operation. There are also functions that can utilize this type to compose two operations, respecting the proper chaining of the preconditions and postconditions. Of course this is what >>= does. (It was also defined for ATMCmd , but I left it out, you can see the code here: TODO LINK HERE)

This is pretty much what the type constructor STrans represents:

data STrans : (m : Type -> Type) -> (ty : Type) -> Resources -> (ty -> Resources) -> Type

There are two major differences: m : Type -> Type and Resources . Let’s explain them in order.

The context, m : Type -> Type

(For initial intuition, let m = IO . It at least makes sense: m and IO have the same type, Type -> Type .)

This is the biggest difference between hand-crafted implementations of stateful types like ATMCmd and STrans , but it’s very simple and logical. Lets introduce some motivation: say that you want to do some basic logging to stdout from your ATMCmd programs. How would you do that? You can’t just pepper it with putStrLn , that only works in IO ! You could add a Log function in the interface definition. Indeed that would work, but for anything else that you wanted to do, you’d have to implement a custom constructor. You could generalize this further, but at that point, it becomes sensible to do exactly what STrans does: introduce the notion of a context that your operations run in.

The main thing you can do with a context is lift values from it into your own type. Effectively this transforms a value like IO Int into a value like ATMCmd Int ... . So instead of directly calling putStrLn , which cannot be done, or implementing Log yourself, you can now just use a lift putStrLn . This is no longer a function in the IO monad, but a function that produces a value that fits your own type.

Resources

I won’t delve into the technical details here. STrans lets you create, update, and destroy resources which hold your state. Instead of just using a sum type for your state to describe its preconditions and postconditions, with resources the idea is that you store something quite complex (like the state of the game!) and assert its presence, something about it, update it, delete it, etc.

This is how you get something like “memory management”: if your program begins and ends without resources, then any resources you create, you must respectively destroy.

You can see this in action in this part of the code that begins and ends the game’s physical world:

startDynamics settings = with ST do
  world <- lift $ createWorld $ gravity settings
  -- create the physical state:
  pdynamics <- new (pdynamicsInStart world (timeStep settings))
  pure pdynamics

endDynamics dynamics = with ST do
  dynamics' <- read dynamics
  lift $ destroyWorld (world dynamics')
  -- destroy the physical state:
  delete dynamics

This is where the ST constructor also appears. It’s pretty much just a convenience, letting you write less verbose code. Instead of specifying a list of resources, and a function that computes the resulting list of resources, you can specify a list of resource transitions . As an example, the types of the above functions:

startDynamics : (settings : DynamicsSettings) -> ST m Var [add SDynamics]
endDynamics : (dynamics : Var) -> ST m () [remove dynamics SDynamics]

add and remove are functions that specify these resource transitions on the type level. The return type of startDynamics is Var , which TODO

So how does this all fit together?

The general idea was to split game state up into stateful systems along concern boundaries, mainly, Server , Client , and Dynamics (wrapper around the physics engine). The server owns the game logic and sends authoritative updates to the client; the client updates some internal states (e.g. for animation), processes SDL2 events and send the results to the server, and owns the UI and rendering logic. The ‘dynamics’ component, aside from owning the simulation and positional data of objects in the game, is also responsible for control logic (i.e. enabling movement, jumping) and producing physics-related events (collisions, query results).

All three of these major components are implemented as interfaces utilizing ST over some general context m . As seems to be idiomatic Idris, they have a single abstract implementation for any context that satisfies certain constraints. For example:

interface Server (m : Type -> Type) where
  -- ...

And the implementation:

(GameIO m, Rules m) => Server m where

This means that if you want to call functions defined under the Server interface, your context m must necessarily have implementations of GameIO and Rules (practically, this enables the implementation of Server to call functions in GameIO and Rules ).

The implementation of these subsystems, however, is largely not done inside stateful ST code. Most of it is implemented through query and update functions, operating on regular Idris data structures, that describe “atomic” operations which the stateful part of the code just glues together. Here’s an example stateful method that creates a physical object in the game:

createObject server creation object_description = with ST do
  id <- decideId server creation

  case createObjectCommand creation object_description id of
    Left e => pure $ fail $ e ++ " (createObject server)"
    Right command => with ST do
      updatePServer server $ addDynamicsCommand command
      updatePServer server $ addInSessionCommand $ Create id (ref creation) (render creation)

      addRules server id object_description creation

      pure $ Right id

While there are purely stateful operations called directly, such as decideId , most changes to the server state are done through the updatePServer operation (P stands for pure), which is a simple operation that takes a pure update ( PServer -> PServer ) and applies it to the server state. Then, helper functions can be written in a pure style to produce these PServer -> PServer updates. All major components are written in this manner.

That’s all for this post. Next, I hope to cover my favorite part: scripting.


以上就是本文的全部内容,希望本文的内容对大家的学习或者工作能带来一定的帮助,也希望大家多多支持 码农网

查看所有标签

猜你喜欢:

本站部分资源来源于网络,本站转载出于传递更多信息之目的,版权归原作者或者来源机构所有,如转载稿涉及版权问题,请联系我们

程序员之禅

程序员之禅

[德] Christian Grobmeier / 荣耀、朱艳 / 人民邮电出版社 / 2015-8 / 39.00元

禅是一种生活态度和生活方式。程序员是一份特别辛苦的职业,也是一个承受各种压力的群体。在物欲横流的今天,禅对于程序员有着特殊的意义和价值。 本书的作者是一名德国程序员老兵,深谙程序员的喜怒哀乐。他曾经发表了一篇题为“程序员之禅的十条法则”的博客文章,引发众多程序员热烈的讨论和强烈的共鸣。本书共10章,结合程序员日常生活和工作的方方面面,作者通过对禅的知识、理解、体验、思考和感悟,提出很多中肯的......一起来看看 《程序员之禅》 这本书的介绍吧!

HTML 编码/解码
HTML 编码/解码

HTML 编码/解码

SHA 加密
SHA 加密

SHA 加密工具

XML 在线格式化
XML 在线格式化

在线 XML 格式化压缩工具