Success stories:
| ironfleet | |||
| rustbelt | |||
| fscq | File system | MIT | Coq |
| sel4 | |||
| certikos | |||
| compcert | C compiler | ||
| cakeml | Compiler for ML subset | HOL | |
| bedrock2 | |||
| iris |
Monadic => effectful
—
What does it mean for two monadic computations to be equivalent?
Cons of large step:
a := n
| a + a
| a - a
| a * a
b := true | false
| ¬b
| b ∧ b
| a = a | a ≠ a
| a ≤ a | a > a
c := skip
| x := a
| c ; c
| if b then c else c end
| while b do c end
⟦n⟧ = n
⟦a1 + a2⟧ = ⟦a1⟧ + ⟦a2⟧
⟦a1 - a2⟧ = ⟦a1⟧ - ⟦a2⟧
⟦a1 * a2⟧ = ⟦a1⟧ * ⟦a2⟧
⟦true⟧ = true
⟦false⟧ = false
⟦¬b⟧ = ¬⟦b⟧
⟦b1 ∧ b2⟧ = ⟦b1⟧ ∧ ⟦b2⟧
⟦a1 = a2⟧ = ⟦a1⟧ == ⟦a2⟧
⟦a1 ≠ a2⟧ = ¬(⟦a1⟧ == ⟦a2⟧)
⟦a1 ≤ a2⟧ = ⟦a1⟧ <= ⟦a2⟧
⟦a1 > a2⟧ = ⟦a1⟧ > ⟦a2⟧
(* st is state *)
⟦skip⟧(st) = st
⟦x := a⟧(st) = st[x ↦ ⟦a⟧]
⟦c1; c2⟧(st) = ⟦c2⟧(⟦c1⟧(st))
⟦if b then c1 else c2⟧(st) = if ⟦b⟧==true then ⟦c1⟧(st) else ⟦c2⟧(st)
⟦while b do c end⟧(st) = if ⟦b⟧==true then ⟦c;(while b do c end)⟧(st) else st
⟦while⟧ is not well founded.
Operational semantics (big-step, aka natural semantics):
--------------
(σ, skip) ⇓ σ
a⇓ₐv
------------------
(σ, x:=a) ⇓ σ[x↦v]
(σ1,c1)⇓σ' (σ',c2)⇓σ2
----------------------
(σ1, c1;c2)⇓σ2
b⇓true (σ,c1)⇓σ' b⇓false (σ,c2)⇓σ'
------------------------------ ------------------------------
(σ, if b then c1 else c2) ⇓ σ' (σ, if b then c1 else c2) ⇓ σ'
b⇓false (σ,c)⇓σ'
-------------------------------
(σ, while b do c end) ⇓ σ'
b⇓true (σ,c)⇓σ' (σ', while b do c end)⇓σ''
-----------------------------------------------------
(σ, while b do c end) ⇓ σ''
Think of monad as a generalized let.
'Well-behaved sequential composition'
Monad laws were not placed inside the Monad type class in the example shown. Why?
Common monads
Monad laws:
m: M A kb: A → M B kc: B → M C
(Think of monad being a box and <- as unboxing.)
–
A bunch of equational theory for the monadic rules which can then be used as rewrite rules to prove semantic equality of two programs.
Looping programs and diversions => itrees. Will see later.
–
Expression problem: Lack of modularity/extensability.
Inductive expr (opr: Type): Type :=
| Val: nat -> expr opr
| Do (op: opr) (k: nat -> expr opr).
(* k: a continuation accepting nat.
Assuming that we deal only with nat ops *)
Inductive plus: Type :=
| Add: nat -> nat -> plus.
We could write stuff like:
Do (Add 2 3) (fun n => Val n)
(* 5 *)
Evaluation (naïve version):
Fixpoint eval {opr: Type} (e: expr opr): nat :=
match e with
| Val n => n
| Do op k =>
match op with
| Add n1 n2 => eval (k (n1 + n2))
end
end.
Comment: This means weird syntax, but no gain
Evalution (via a handler):
(* eval_fold *)
Fixpoint evalf {opr: Type} (h: opr -> nat) (e: expr opr): nat :=
match e with
| Val n => n
| Do op k => evalf h (k (h op))
end.
(* Handler for [plus] *)
Definition hplus (op: plus): nat :=
match op with
| Add n1 n2 => n1 + n2
end.
Compute evalf hplus (Do (Add 2 3) (fun n => Val n)).
(* 5 *)
—
Sequential composition:
Fixpoint seq {opr: Type} (e: expr opr) (k: nat -> expr opr): expr opr :=
match e with
| Val n => k n
| Do op h => Do op (fun n => Do op (seq (h n) k))
end.
Notation "x <- e1;; e2 " := (seq e1 (fun x => e2)).
Operations as triggerable events:
op and return its value as an expr ??Definition trigger {opr: Type} (op: opr): Expr opr :=
Do op (fun n => Val n).
Example uses:
eval (trigger (Add 2 3))
(* 5 *)
eval (
x <- trigger (Add 2 3);;
y <- trigger (Add 4 5);;
trigger (Add x y)
)
(* 14 *)
Let's try adding another operation: Subtr.
Inductive subtr: Type :=
| Subtr: nat -> nat -> subtr.
Fixpoint hsubtr (op: subtr): nat :=
match op with
| Subtr n1 n2 => n1 - n2
end.
evalf hsubtr (trigger (Subtr 5 3))
(* 2 *)
evalf hsubtr (
x <- trigger (Subtr 5 3);;
y <- trigger (Subtr 2 1);;
trigger (Subtr x y)
)
(* 1 *)
—
Multiple operations:
Notation "opr1 +' opr2" := ((opr1 + opr2)%type).
(* Handler for add and sub *)
Definition hsum {opr1 opr2: Type} (h1: opr1 -> nat) (h2: opr2 -> nat)
(op: opr1 +' opr2): nat :=
match op with
| inl op' => h1 op'
| inr op' => h2 op'
end.
evalf (hsum hadd hsubtr) (
x <- trigger (inl (Add 2 3));;
y <- trigger (inr (Subtr x 3));;
trigger (inl (Add y 1))
)
(* 3 *)
Note: The Add and inl are duplicate essentially. Typeclasses to help it figure out could come in handy.
Generalizing instead of specializing results to nat.
(*
- E: opr ??
- R: final return type ??
*)
Inductive FFree (E: Type -> Type) (R: Type): Type :=
| Ret: R -> FFree E R
| Do: forall {X: opr},
E X -> (X -> FFree E R).
E X: E produces an X, which will be fed in to the continuation.
Same as expr from earlier, except for nat being generalized.
Inductive itree
| Ret: R -> itree
| Tau: itree
| Vis {Ans: Type} (event: E Ans) (k: Ans -> itree).
const5 := Ret 5. double := Vis Input (fun n > Ret 2*n).
silentloop : Tau silentloop
(* Result from event given to the system is the index Type *)
Inductive IOEvent: Type -> Type :=
| Out: nat -> IOEvent unit
| Inp: IOEvent nat.
CoFixpoint inoutloop :=
Vis Inp (fun n =>
Vis Out (fun _ => inoutloop)).
Inductive empty: Type -> Type :=
| Empty: fail void.
Definition fail :=
Vis empty (fun v => match x with end).
(* subst *)
CoFixpoint subst (x: itree) (k: X -> itree): itree :=
match x with
| Ret v => k v
| Vis ev kk => Vis ev (fun x => subst (kk x) k)
| Tau t => subst t k
end.
{inty rty: Type}
iter (t: itree) (k: inty -> itree) (init: inty)
x <- k init;;
match x with
| inl nval => Tau (iter t' k nval) (* init is like the initial state (like loop exit condition??) nval is the new state *)
| inr nval => Ret nval
end
fact (n: nat) :=
iter (fun n => fact (n-1)
itree E R: promises to deliver a value of type R
irrefutable pattern matching
t1 ~ t2t1 ≈ t2Monad laws hold upto strong bisimulation.
Nested coinductive inductive sth
Kleisli
DBT: bimap in file:///home/famubu/gits/nm/zdancewic-oplss24/terse/ITreesEquiv.html#slide-5
DBT: Why variant for MemE?
Desired function: S -> Inp -> (S, Out)
itree E R
| Vis: forall X, E X -> (X -> itree E R)
| Tau: itree E R