@@ -383,6 +383,154 @@ of ``DataStore``.
383383Implementing the interface
384384==========================
385385
386+To execute ``getData`` in ``IO``, we'll need to provided an implementation
387+of ``DataStore`` which works in the ``IO`` context. We can begin as
388+follows:
389+
390+.. code-block:: idris
391+
392+ implementation DataStore IO where
393+
394+Then, we can ask Idris to populate the interface with skeleton definitions
395+for the necessary methods (press ``Ctrl-Alt-A`` in Atom for "add definition"
396+or the corresponding shortcut for this in the Idris mode in your favourite
397+editor):
398+
399+.. code-block:: idris
400+
401+ implementation DataStore IO where
402+ Store x = ?DataStore_rhs_1
403+ connect = ?DataStore_rhs_2
404+ disconnect store = ?DataStore_rhs_3
405+ readSecret store = ?DataStore_rhs_4
406+ login store = ?DataStore_rhs_5
407+ logout store = ?DataStore_rhs_6
408+
409+The first decision we'll need to make is how to represent the data store.
410+We'll keep this simple, and store the data as a single ``String``, using
411+a hard coded password to gain access. So, we can define ``Store`` as
412+follows, using a ``String`` to represent the data no matter whether we
413+are ``LoggedOut`` or ``LoggedIn``:
414+
415+.. code-block:: idris
416+
417+ Store x = State String
418+
419+Now that we've given a concrete type for ``Store``, we can implement operations
420+for connecting, disconnecting, and accessing the data. And, since we used
421+``State``, we can use ``new``, ``delete``, ``read`` and ``write`` to
422+manipulate the store.
423+
424+Looking at the types of the holes tells us how we need to manipulate the
425+state. For example, the ``?DataStore_rhs_2`` hole tells us what we need
426+to do to implement ``connect``. We need to return a new ``Var`` which
427+represents a resource of type ``State String``:
428+
429+.. code-block:: idris
430+
431+ --------------------------------------
432+ DataStore_rhs_2 : STrans IO Var [] (\result => [result ::: State String])
433+
434+We can implement this by creating a new variable with some data for the
435+content of the store (we can use any ``String`` for this) and returning
436+that variable:
437+
438+.. code-block:: idris
439+
440+ connect = do store <- new "Secret Data"
441+ pure store
442+
443+For ``disconnect``, we only need to delete the resource:
444+
445+.. code-block:: idris
446+
447+ disconnect store = delete store
448+
449+For ``readSecret``, we need to read the secret data and return the
450+``String``. Since we now know the concrete representation of the data is
451+a ``State String``, we can use ``read`` to access the data directly:
452+
453+.. code-block:: idris
454+
455+ readSecret store = read store
456+
457+We'll do ``logout`` next and return to ``login``. Checking the hole
458+reveals the following:
459+
460+.. code-block:: idris
461+
462+ store : Var
463+ --------------------------------------
464+ DataStore_rhs_6 : STrans IO () [store ::: State String] (\result => [store ::: State String])
465+
466+So, in this minimal implementation, we don't actually have to do anything!
467+
468+.. code-block:: idris
469+
470+ logout store = pure ()
471+
472+For ``login``, we need to return whether logging in was successful. We'll
473+do this by prompting for a password, and returning ``OK`` if it matches
474+a hard coded password, or ``BadPassword`` otherwise:
475+
476+.. code-block:: idris
477+
478+ login store = do putStr "Enter password: "
479+ p <- getStr
480+ if p == "Mornington Crescent"
481+ then pure OK
482+ else pure BadPassword
483+
484+For reference, here is the complete implementation which allows us to
485+execute a ``DataStore`` program at the REPL:
486+
487+.. code-block:: idris
488+
489+ implementation DataStore IO where
490+ Store x = State String
491+ connect = do store <- new "Secret Data"
492+ pure store
493+ disconnect store = delete store
494+ readSecret store = read store
495+ login store = do putStr "Enter password: "
496+ p <- getStr
497+ if p == "Mornington Crescent"
498+ then pure OK
499+ else pure BadPassword
500+ logout store = pure ()
501+
502+Finally, we can try this at the REPL as follows (Idris defaults to the
503+``IO`` context at the REPL if there is an implementation available, so no
504+need to give the ``m`` argument explicitly here):
505+
506+.. code::
507+
508+ *Login> :exec run getData
509+ Enter password: Mornington Crescent
510+ Secret is: "Secret Data"
511+
512+ *Login> :exec run getData
513+ Enter password: Dollis Hill
514+ Failure
515+
516+We can only use ``read``, ``write``, ``new`` and ``delete`` on a resource
517+with a ``State`` type. So, *within* the implementation of ``DataStore``,
518+or anywhere where we know the context is ``IO``, we can access the data store
519+however we like: this is where the internal details of ``DataStore`` are
520+implemented. However, if we merely have a constraint ``DataStore m``, we can't
521+know how the store is implemented, so we can only access via the API given
522+by the ``DataStore`` interface.
523+
524+It is therefore good practice to use a *generic* context ``m`` for functions
525+like ``getData``, and constrain by only the interfaces we need, rather than
526+using a concrete context ``IO``.
527+
528+We've now seen how to manipulate states, and how to encapsulate state
529+transitions for a specific system like the data store inn an interface.
530+However, realistic systems will need to *compose* state machines. We'll
531+either need to use more than one state machine at a time, or implement one
532+state machine in terms of one or more others. We'll see how to achieve this
533+in the next section.
386534
387535.. |login| image:: ../image/login.png
388536 :width: 500px