@@ -352,7 +352,7 @@ than directly with ``delete``.
352352
353353We can complete ``getData`` as follows, using a pattern matching bind
354354alternative (see the Idris tutorial, :ref:`monadsdo`) rather than a
355−``case`` statement to catch the possibilty of an error with ``login``:
355+``case`` statement to catch the possibility of an error with ``login``:
356356
357357.. code-block:: idris
358358
@@ -367,7 +367,7 @@ alternative (see the Idris tutorial, :ref:`monadsdo`) rather than a
367367 disconnect st
368368
369369We can't yet try this out, however, because we don't have any implementations
370−of ``getData``! If we try to execute it in an ``IO`` context, for example,
370+of ``DataStore``! If we try to execute it in an ``IO`` context, for example,
371371we'll get an error saying that there's no implementation of ``DataStore IO``:
372372
373373.. code::
@@ -383,7 +383,7 @@ of ``DataStore``.
383383Implementing the interface
384384==========================
385385
386−To execute ``getData`` in ``IO``, we'll need to provided an implementation
386+To execute ``getData`` in ``IO``, we'll need to provide an implementation
387387of ``DataStore`` which works in the ``IO`` context. We can begin as
388388follows:
389389
@@ -526,7 +526,7 @@ like ``getData``, and constrain by only the interfaces we need, rather than
526526using a concrete context ``IO``.
527527
528528We'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.
529+transitions for a specific system like the data store in an interface.
530530However, realistic systems will need to *compose* state machines. We'll
531531either need to use more than one state machine at a time, or implement one
532532state machine in terms of one or more others. We'll see how to achieve this