@@ -383,6 +383,154 @@ of ``DataStore``.
383Implementing the interface
383Implementing the interface
384==========================
384==========================
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
390+.. code-block:: idris
392+ implementation DataStore IO where
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
399+.. code-block:: idris
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
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``:
415+.. code-block:: idris
417+ Store x = State String
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.
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``:
429+.. code-block:: idris
431+ --------------------------------------
432+ DataStore_rhs_2 : STrans IO Var [] (\result => [result ::: State String])
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
438+.. code-block:: idris
440+ connect = do store <- new "Secret Data"
443+For ``disconnect``, we only need to delete the resource:
445+.. code-block:: idris
447+ disconnect store = delete store
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:
453+.. code-block:: idris
455+ readSecret store = read store
457+We'll do ``logout`` next and return to ``login``. Checking the hole
458+reveals the following:
460+.. code-block:: idris
463+ --------------------------------------
464+ DataStore_rhs_6 : STrans IO () [store ::: State String] (\result => [store ::: State String])
466+So, in this minimal implementation, we don't actually have to do anything!
468+.. code-block:: idris
470+ logout store = pure ()
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:
476+.. code-block:: idris
478+ login store = do putStr "Enter password: "
480+ if p == "Mornington Crescent"
482+ else pure BadPassword
484+For reference, here is the complete implementation which allows us to
485+execute a ``DataStore`` program at the REPL:
487+.. code-block:: idris
489+ implementation DataStore IO where
490+ Store x = State String
491+ connect = do store <- new "Secret Data"
493+ disconnect store = delete store
494+ readSecret store = read store
495+ login store = do putStr "Enter password: "
497+ if p == "Mornington Crescent"
499+ else pure BadPassword
500+ logout store = pure ()
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):
508+ *Login> :exec run getData
509+ Enter password: Mornington Crescent
510+ Secret is: "Secret Data"
512+ *Login> :exec run getData
513+ Enter password: Dollis Hill
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.
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``.
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
387.. |login| image:: ../image/login.png
535.. |login| image:: ../image/login.png
388 :width: 500px
536 :width: 500px