9.1. Hoare State Monad (Swierstra)

Wouter Swierstra use the example of relabelling binary to illustrate the Hoare state monad.

 original tree                   relabelled tree (start 10)
   *                                         *
 /   \                                     /   \
a     *                                   10    *
    /   \                                     /   \
   b      c                                  11   12

9.1.1. Without Monad

class Tree (A: Any) :=
    leaf: A -> Tree             -- information in the leaves
    node: Tree -> Tree -> Tree

relabel {A: Any}: Tree A -> ℕ -> (Tree ℕ, ℕ) :=
    case
        λ (leaf _) n :=
            (leaf n, succ n)
        λ (node t1 t2) n :=
            let (t11,n1) := relabel t1 n
                (t22,n2) := relabel t2 n1
            :=
                (node t12 t22, n2)

9.1.2. With Monad

-- State Monad
SM (S A: Any): Any :=
    S → (A,S)

return {S A: Any} (a: A): SM S A :=
    λ s := (a,s)

(>>=) {S A B: Any} (m: SM S A) (f: A → SM S B): SM S B :=
    λ s :=
        let (a,s) := m s
        :=
            f a s

get {S: Any}: SM S S :=
    λ s := (s,s)

put {S: Any} (s: S): SM S Unit :=
    λ _ := (unit, s)


relabel {A: Any}: Tree A → SM ℕ (Tree ℕ) :=
    case
        λ (leaf _) :=
            do
                n := get
                put (succ n)
                return (leaf n)
        λ (node t1 t2) :=
            do
                t1 := relabel t1
                t2 := relabel t2
                return (node t1 t2)

9.1.3. Hoare Monad

Definition of the Hoare state monad:

Pre (S: Any): Any :=
    S → Prop

Post (S A: Any): Any :=
    S → A → S → Prop

HM
    {S A: Any}
    (Q: Pre S)
    (R: Post S A)
    : Any
:=
    all ((refine s0 _): Refine Q)
    : Refine (λ (a,s1) := R s0 a s1)


Top {S: Any}: Pre S :=
    λ _ := True

The return function:

return
    {S A: Any}
    (a: A)
    : HM (Top {S}) (λ s₀ b s₁ := s₀ = s₁ ∧ a = b)
:=
    case
        λ (refine s _) := refine (a,s) (identical, identical)

The bind function:

JoinPre {S A: Any} (Q1: Pre S) (R1: Post S A) (Q2: A → Pre S): Pre S
    -- The precondition 'Q1' and the postcondition 'R1' imply the
    -- precondition 'Q2'.
:=
    λ s₀ :=
        Q1 s₀
        ∧
        all a s₁: R1 s₀ a s₁ → Q2 a s₁

JoinPost {S A B: Any} (R1: Post S B) (R2: A → Post S B): Post S B
    -- A predicate on 's₀', 'b' and 's₂' such that
    -- there are some intermediate result 'a' and some intermediate state
    -- 's₁' such that the first postcondtion 'R1 s₀ a s₁' and the second
    -- postcondition 'R2 a s₁ b s₂' are satisfied.
:=
    λ s₀ b s₂ :=
        some a s₁:
            R1 s₀ a s₁
            ∧
            R2 a s₁ b s₂

(>>=)
    {S A B: Any}
    {Q1: Pre S}
    {R1: Post S A}
    {Q2: A → Pre S}
    {R2: A → Post S B}
    (m: HM Q1 R1)
    (f: all x: HM (Q2 x) (R2 x))
    : HM (JoinPre Q1 R1 Q2) (JoinPost R1 R2)
:= case
    λ (refine s₀ (q₀, fp)) :=
        let
            (refine (a,s₁) (r₁: R1 s₀ a s₁)) :=
                m (refine s₀ q₀)
        :=
            inspect
                f a s₀
            case
                λ (refine (b,s₂) (r₂: R2 a s₁ b s₂) :=
                    refine (b,s₂) (exist (exist (r₁, r₂)))

Get and put

get
    {S: Any}
    : HM (Top {S}) (λ s₀ s s₁ := s₀ = s₁ ∧ s = s₁)
:=
    case
        λ (refine s _) :=
            refine (s,s) (identical, identical)

put
    {S: Any}
    (s: S)
    : HM (Top {S}) (λ _ _ s₁ := s = s₁)
:=
    case
        λ (refine s _) :=
            refine (unit,s) identical

Adaption of pre- and postconditions:

adapt
    {S A: Any}
    {Q1 Q2: Pre S}
    {R1 R2: Post S A}
:   (all s: Q2 s → Q1 s)
    → (all s₀ a s₁: R1 s₀ a s₁ → R2 s₀ a s₁)
    → HM Q1 R1
    → HM Q2 R2
:=
    λ fq fr m (refine s₀ q₀) :=
        let
            (refine (a,s₁) r₁ :=
                m (refine s₀ (fq s₀))
        :=
            refine (a,s₁) (fr s₀ a s₁)

9.1.4. Certified Relabelling

flatten {A: Any}: Tree A → List A
:= case
    λ (leaf a) :=
        [a]
    λ (node t1 t2) :=
        flatten t1 + flatten t2


size {A: Any}: Tree A → ℕ
    -- The number of leaf nodes in a tree.
:= case
    λ (leaf _) :=
        1
    λ (node t1 t2) :=
        size t1 + size t2


seq: ℕ → ℕ → List ℕ
    -- seq start n = [start, 1+start, 2+start, ... (n - 1) + start]
:= case
    λ start zero :=
        []
    λ start (succ n) :=
        start :: seq (succ start) n


relabel
    {A: Any}
    :   Tree A
        → HM
            (Top {ℕ})
            (λ n₀ t n₁ :=
                size t + n₀ = n₁)
:= case  -- INCOMPLETE!!!!
    λ (leaf _) :=
        (do
            n := get
            put (succ n)
            return (leaf n))
        adapt
            (λ _ _ := (
                trueValid,                  -- precondition of 'get'
                λ _ _ := (
                    trueValid,              -- precondition of 'put'
                    λ _ _ := trueValid      -- precondition of 'return'
            )))
            (λ  n₀
                t
                n₄
                (exist (exist (
                    (eqN0N1,eqN0N),
                    (exist (exist (
                        eqN2SuccN,
                        (exist (exist (
                            (eqN2N3,eqLeafNT)
                )))))))))
             :=
                identical
             )

    λ (node t1 t2) :=
        (do
            u1 := relabel t1
            u2 := relabel t2
            return (node u1 u2)
        adapt
            (λ _ _ := (
                trueValid,                  -- precondition of 'relabel'
                λ _ _ := (
                    trueValid,              -- precondition of 'relabel'
                    λ _ _ := trueValid      -- precondition of 'return'
            )))
            ()

9.1.5. Some Analysis

We need the following ingredients:

• a state S

• a precondition which is a predicate over the state i.e. Predicate S which is equivalent to S -> Prop.

  Pre (S: Any): Any :=
      S -> Prop
  

• a transition relation

  Tra {S: Any} (P: Pre S) (A: Any): Any :=
      Refine P -> (A, S) -> Prop
  

  i.e. a transition relation Tra P A which maps each state satisfying P, an element of type A and a state S into a proposition. An element T of type Tra P A maps each state satisfying the precondition P into a predicate over the computed element of type A and the poststate.

With this we define the Hoare state monad:

HM {S A: Any} (Q: Pre S) (T: Tra Q A): Any :=
    all (s: Refine Q):  Refine (T s)

-- compare this with the normal state monad

M (S A: Any): Any :=
    S -> (A, S)

An element of type Refine Q is a state together with a proof that the state satisfies the precondition Q. An element of type Refine (T s) is a pair of type (A, S) together with a proof that the pair satisfies the postcondition T s.

9.1.6. Example: Open File Descriptors

Many IO functions can be called only with an open file descriptor. E.g. a read or a write function to a file can be called only with a file descriptor which is open for read or write. The state of IO be described e.g. by

State: Any :=
    List ((FD, String, Mode))
    --     |   |       ^ read, write, ...
    --     |   *- file name
    --     *- file descriptor

In order to keep things simple we tacitely assume that a filedescriptor is never entered twice i.e. that the list represents a finite map from filedescriptors to pairs of filename and io mode.

The IO monad has three arguments: The result type, a precondition and a transition relation:

IO {A: Any} (Q: PR) (T: TR A): Any

-- where
PR: Any :=
    State -> Prop

TR (A: Any): Any :=
    State -> A -> State -> Prop

An IO action of type IO Q T can be started in a state s₀ satisfying Q s₀. In case of success it returns an object a in a state s₁ such that TR s₀ a s₁ is satisfied.

open
    (fn: String) (m: mode)
    : IO
        Top
        (Open fn m)
      where
        Top _ :=
            True       -- trivial precondition
        Open fn m s0 fd s1 :=
            s1 = (fd, fn, m) :: s0

9.1.7. Example: Open File Descriptors (2)

PROBLEM:

with the following code: It is not expressible, that all successful open return a file descriptor which is different from all other open file descriptors.

IO {A: Any} (Q: Predicate State) (t: A -> State -> State): Any

section {A B: Any}
:=
    return: A -> IO Top (\ _ s := s)

    (>>)
        (m: IO Q t)
        (f: all (a: A): IO (Q2 a) (t2 a))
        : (all a s: Q s -> Q2 a (t a s))
          -> IO Q (\ a s := t2 a (t a s))

open
    (fn: String) (m: Mode)
    : IO
        Top
        (\ fd s := (fd, fn, m) :: s)

type OpenRead: File -> State -> Prop :=
    basic {fd} {fn} {s}:
        OpenRead fd ((fd, fn, read) :: s)
    next {fd} {fd2} {fn} {m} {s}:
        fd /= fd2 -> OpenRead fd s -> OpenRead fd ((fd2, fn, m) :: s)

getc (fd: File): IO (OpenRead fd) (\ _ s := s)

9.1.8. Example: Open File Descriptors (3)

type Mode := [read, write]

type
    FD: Mode -> List Mode -> Any
    -- An object of type 'FD read lst' is a valid open filedescriptor for
    -- reading in the list 'lst' of modes.
:=
    start {m} {l}:
        FD m (m :: l)

    next {m0} {m1} {l}:
        FD m0 l -> FD m0 (m1 :: l)

(-):
    all {m} (l: List Mode): FD m l -> List Mode
:= case
    \ (m :: l)   start      := l

    \ (m :: l)   (next fd)  := m :: (l - fd)

-- builtins

IO {il ol: List Mode}: Any -> il ol

open {l} (name: String) (m: Mode) : IO (FD m (m :: l)) l (m :: l)

close {m} {l} (fd: FD m l) : IO Unit l (l - fd)

getc {l} (fd: FD read l): IO Char l l