Example: add monad file

Author: clarus

monad_examples.v

@@ -0,0 +1,147 @@
+Require Import Coq.Strings.String.
+Require Import Coq.ZArith.ZArith.
+
+Open Scope Z.
+
+(* pure function example *)
+Definition plus_two (n : nat) : nat :=
+  n + 2.
+
+(* Functions with side effects: not possible in Coq but possible in other programming languages *)
+(* side-effect 1 : input-output operation *)
+(* Definition get_current_time_in_seconds : nat :=
+  Time.get_current_time (). *)
+
+(* side-effect 2: modify a state *)
+
+(* Definition global_bar := 2.
+
+Definition increment () : unit :=
+  global_var += 1.
+
+(* side-effect 3: propagate an error *)
+
+(* side-effect: errors *)
+Definition divide_by_zero n :=
+  n / 0. *)
+
+(* To represent side effects in purely functional language: monads *)
+
+(* Monads *)
+(* M A: monadic type: "computations that returns a value of type A" *)
+(* Two primitive operations *)
+(* return/pure: A -> M A : to convert pure operations to monadic operations *)
+(* bind: M A -> (A -> M B) -> M B : to sequence two monadic operations *)
+
+(* Example of monads: *)
+(* Error *)
+Inductive ErrorMonad (A : Set) : Set :=
+| Success (value : A)
+| Error (message : string).
+Arguments Success {_}.
+Arguments Error {_}.
+
+Definition pure_error_monad {A : Set} (value : A) : ErrorMonad A :=
+  Success value.
+
+Definition bind_error_monad {A B : Set} (first : ErrorMonad A) (second : A -> ErrorMonad B) : ErrorMonad B :=
+  match first with
+  | Success value => second value
+  | Error message => Error message
+  end.
+
+Definition division_by_something (z1 z2 : Z) : ErrorMonad Z :=
+  if z2 =? 0 then
+    Error "division by zero"
+  else
+    Success (z1 / z2).
+
+(* a1 / a2 + b1 / b2 *)
+Definition sum_of_two_divisions (a1 a2 b1 b2 : Z) : ErrorMonad Z :=
+  bind_error_monad (division_by_something a1 a2) (fun x =>
+    bind_error_monad (division_by_something b1 b2) (fun y =>
+      pure_error_monad (x + y)%Z
+    )
+  ).
+
+Compute sum_of_two_divisions 4 3 2 1. (* => Success value *)
+Compute sum_of_two_divisions 4 0 2 1. (* => Error message *)
+
+(* IO example *)
+Inductive PossibleIO : Set -> Set :=
+| GetTime : PossibleIO Z
+| ReadFile (filename : string) : PossibleIO (option string)
+| WriteFile (filename : string) (new_content : string) : PossibleIO bool.
+
+(* With the IO monad, everything is data, we do not actually compute anything *)
+Inductive IO (A : Set) : Set :=
+| Pure (value : A)
+| Impure (io : PossibleIO A)
+| Bind {B : Set} (first : IO B) (second : B -> IO A).
+Arguments Pure {_}.
+Arguments Impure {_}.
+Arguments Bind {_ _}.
+
+Definition get_time : IO Z :=
+  Impure GetTime.
+
+Definition read_file_and_return_duration (filename : string) : IO Z :=
+  Bind get_time (fun initial_time =>
+  Bind (Impure (ReadFile filename)) (fun _ =>
+  Bind get_time (fun final_time =>
+    Pure (final_time - initial_time)
+  ))).
+
+(* The output is very verbose, as this is the code above that is printed expanding all the
+   definitions, but nothing is computed. *)
+Compute read_file_and_return_duration "example.txt".
+
+(* We can still specify things about programs in the IO monands, even if we cannot compute. Here is
+   an example of a simple function that checks if a computation is actually just a pure value
+   without any IO. *)
+Definition is_IO_without_IO {A : Set} (computation : IO A) : bool :=
+  match computation with
+  | Pure _ => true
+  | _ => false
+  end.
+
+Compute is_IO_without_IO get_time. (* => false *)
+Compute is_IO_without_IO (Pure (1 + 2)%Z). (* => true *)
+
+(* State monad *)
+(* The idea is to add the input state as an additional parameter to the functions, and the output
+   state as an addition result *)
+Definition StateMonad (State : Set) (A : Set) : Set :=
+  State (* input *) -> A * State (* output *).
+
+(* We assume that our state is a global variable of type [Z] *)
+Definition State : Set :=
+  Z.
+
+(* We do not change the state in the pure operator *)
+Definition pure_state {A : Set} (value : A) : StateMonad State A :=
+  fun state => (value, state).
+
+(* We propagate the updated state in the bind operator *)
+Definition bind_state {A B : Set} (first : StateMonad State A) (second : A -> StateMonad State B) : StateMonad State B :=
+  fun state =>
+    let (value, new_state) := first state in
+    second value new_state.
+
+(* We can now define the increment operation *)
+Definition increment : StateMonad State unit :=
+  fun state => (tt, state + 1).
+
+(* We can apply the increment three times *)
+Definition increment_three_times : StateMonad State unit :=
+  bind_state increment (fun _ =>
+  bind_state increment (fun _ =>
+  bind_state increment (fun _ =>
+    pure_state tt
+  ))).
+
+Definition initial_state : State :=
+  12.
+
+Compute increment initial_state. (* => (tt, 13  ) *)
+Compute increment_three_times initial_state. (* => (tt, 15) *)