Dijkstra Monads for Free

Sales pitch

Previously, in order to define a new effect, you had to do:

let st_pre_h  (heap:Type)          = heap -> GTot Type0
let st_post_h (heap:Type) (a:Type) = a -> heap -> GTot Type0
let st_wp_h   (heap:Type) (a:Type) = st_post_h heap a -> Tot (st_pre_h heap)

inline let st_return        (heap:Type) (a:Type)
                            (x:a) (p:st_post_h heap a) =
     p x
inline let st_bind_wp       (heap:Type) 
			    (r1:range) 
			    (a:Type) (b:Type)
                            (wp1:st_wp_h heap a)
                            (wp2:(a -> GTot (st_wp_h heap b)))
                            (p:st_post_h heap b) (h0:heap) =
     labeled r1 "push" unit
     /\ wp1 (fun a h1 ->
       labeled r1 "pop" unit
       /\ wp2 a p h1) h0
inline let st_if_then_else  (heap:Type) (a:Type) (p:Type)
                             (wp_then:st_wp_h heap a) (wp_else:st_wp_h heap a)
                             (post:st_post_h heap a) (h0:heap) =
     l_ITE p
        (wp_then post h0)
	(wp_else post h0)
inline let st_ite_wp        (heap:Type) (a:Type)
                            (wp:st_wp_h heap a)
                            (post:st_post_h heap a) (h0:heap) =
     forall (k:st_post_h heap a).
	 (forall (x:a) (h:heap).{:pattern (guard_free (k x h))} k x h <==> post x h)
	 ==> wp k h0
inline let st_stronger  (heap:Type) (a:Type) (wp1:st_wp_h heap a)
                        (wp2:st_wp_h heap a) =
     (forall (p:st_post_h heap a) (h:heap). wp1 p h ==> wp2 p h)

inline let st_close_wp      (heap:Type) (a:Type) (b:Type)
                             (wp:(b -> GTot (st_wp_h heap a)))
                             (p:st_post_h heap a) (h:heap) =
     (forall (b:b). wp b p h)
inline let st_assert_p      (heap:Type) (a:Type) (p:Type)
                             (wp:st_wp_h heap a)
                             (q:st_post_h heap a) (h:heap) =
     p /\ wp q h
inline let st_assume_p      (heap:Type) (a:Type) (p:Type)
                             (wp:st_wp_h heap a)
                             (q:st_post_h heap a) (h:heap) =
     p ==> wp q h
inline let st_null_wp       (heap:Type) (a:Type)
                             (p:st_post_h heap a) (h:heap) =
     (forall (x:a) (h:heap). p x h)
inline let st_trivial       (heap:Type) (a:Type)
                             (wp:st_wp_h heap a) =
     (forall h0. wp (fun r h1 -> True) h0)

new_effect {
  STATE_h (heap:Type) : result:Type -> wp:st_wp_h heap result -> Effect
  with return_wp      = st_return heap
     ; bind_wp      = st_bind_wp heap
     ; if_then_else = st_if_then_else heap
     ; ite_wp       = st_ite_wp heap
     ; stronger     = st_stronger heap
     ; close_wp     = st_close_wp heap
     ; assert_p     = st_assert_p heap
     ; assume_p     = st_assume_p heap
     ; null_wp      = st_null_wp heap
     ; trivial      = st_trivial heap
}

With Dijkstra Monads for Free, you only need to do:

let st (h: Type) (a: Type) =
  h -> M (a * h)

val return_st: h:Type -> a:Type -> x:a -> st h a
let return_st h a x = fun s -> x, s

val bind_st: h:Type -> a:Type -> b:Type -> f:st h a -> g:(a -> st h b) -> st h b
let bind_st h a b f g = fun s0 ->
  let tmp = f s0 in
  let x, s1 = tmp in
  g x s1

let get (h: Type) (_:unit): st h h =
  fun x -> x, x

let put (h: Type) (x: h): st h unit =
  fun _ -> (), x

reifiable reflectable new_effect_for_free {
  STATE (h: Type): a:Type -> Effect
  with repr     = st h
     ; bind     = bind_st h
     ; return   = return_st h
  and effect_actions
       get      = get h
     ; put      = put h
}

(see examples/dm4free).

This page describes the user-facing side of Dijkstra Monads for Free, i.e. how to actually use it from within F*. This is still experimental! Please make sure you have read the companion paper first.

Embedding the definition language in F*

The paper describes in §4 the definition language DM. Specifically, DM features τ-arrows that indicate monadic computations, and n-arrows that indicate regular computations.

We embed DM in the existing syntax of F*. DM terms are first type-checked by F★ for consistency and well-formedness. Then, they are re-checked by a standalone bidirectional type-checker that interprets them as terms in DM, and performs the *-translation and elaboration (see src/typechecker/dmff.fs).

In order to indicate τ-arrows, a special monad (an alias for Tot) is defined in prims.fst:

effect M (a:Type) = Tot a

since effects can only appear on the right-hand side of an arrow, a τ-arrow is simply an arrow whose return computation is in M.

let st (h: Type) (a: Type) =
  h -> M (a * h)

For terms to be successfully type-checked by the DMFF type-checker, they must be fully annotated, and properly curried. This works:

val return_st: h:Type -> a:Type -> x:a -> st h a
let return_st h a x = fun s -> x, s

this most likely won't, because there's no M anywhere that indicates where the monadic effect is meant to take place.

let return_st h a x s = x, s

binds and returns

The bidirectional type-checker needs to know what is a bind and what is a return in order to accurately compute the *-translation and elaboration of monadic combinators. We use M t to denote an expression whose type is a monadic computation of type t. We use N t to denote an expression whose type is a non-monadic computation t.

The judgement is of the form e -> M t, e', meaning that e is inferred to have type M t, and interpreted as e', a term that has explicit binds and returns. The other judgement is e <- M t, e', meaning that e is checked.

The two essential typing rules are as follows:

LET

e1 -> M t1, e1
e2 <- M t2, e2
--------------------------------------------
let x = e1 in e2 -> M t2, bind e1 to x in e2 

e -> N t, e
------------------
e <- M t, return e

In plain English: let-binding an expression that returns an M is interpreted as a bind; returns are inserted as needed to make the continuation of a let-binding a monadic expression too.

As an example, this term:

val bind_st: h:Type -> a:Type -> b:Type -> f:st h a -> g:(a -> st h b) -> st h b
let bind_st h a b f g = fun s0 ->
  let tmp = f s0 in 
  let x, s1 = tmp in
  g x s1

is interpreted as

val bind_st: h:Type -> a:Type -> b:Type -> f:st h a -> g:(a -> st h b) -> st h b
let bind_st h a b f g = fun s0 ->
  bind f s0 to tmp in
  let x, s1 = tmp in
  return (g x s1)

note that the interpretation inserts return at depth; an alternate, less elegant choice, would've been to intepret this as:

val bind_st: h:Type -> a:Type -> b:Type -> f:st h a -> g:(a -> st h b) -> st h b
let bind_st h a b f g = fun s0 ->
  bind f s0 to tmp in
  return (let x, s1 = tmp in
    g x s1)

Please note that the scrutinee of a match does not get the bind-insertion treatment. This means that the bidirectional type-checker will not pick up a bind in let x, y = e in because it really is match e with | x, y ->!

Elaboration of other effect combinators

See src/typechecker/dmff.fs. Most importantly, you can use the following names after the effect has been defined:

• STATE?.pre, STATE?.post, STATE?.wp: extracted from the CPS'd version of repr
• STATE?.repr: the elaborted version of repr with a full type that mentions its wp