What is Tapas, and what is it for?

Disclaimer. This post does not exist to justify the existence of Tapas (hereinafter "the Library"). Its sole purpose is to illustrate how a range of verification problems can be approached from the perspective of parametricity, and how the Library can be used to obtain some useful results about them in a relatively uniform way. How the Library compares with other parametricity-based libraries is a question orthogonal to this post. The author is still trying to understand the ingenious designs behind those libraries, and therefore makes no warranty of novelty, express or implied.

Tagless final form

Let's start with a seemingly unrelated question: how do we usually write a program with several effects? An obvious and very direct choice is to cook up a stack of monad transformers; if some of the effects are to stay uninterpreted, perhaps something like a freer monad. Here is a toy withdrawal that reads the fee from an environment, keeps the balance as state, and fails when the balance is too low:

def withdraw (amount : Nat) : ReaderT Nat (StateT Nat (Except String)) Unit := do
  let fee ← read
  modify (· - fee)  -- the fee is charged up front
  if (← get) < amount then throw "insufficient funds"
  modify (· - amount)

That is certainly one option. Another is to write the program in tagless final form, taking the effects it uses as type class parameters. (Haskell programmers may know this as mtl style.) In fact, Lean itself works this way. Its core library provides classes such as MonadStateOf and MonadReaderOf, which supply monadic operations like get and read, and much of Lean's own metaprogramming code is written against classes like these: logInfo, for instance, works in any m with [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]. In this form, the example becomes

def withdraw {m : Type → Type} [Monad m]
    [MonadReaderOf Nat m] [MonadStateOf Nat m] [MonadExceptOf String m]
    (amount : Nat) : m Unit := do 
    /- exactly the same body as above -/

One benefit of this is that we get different concrete programs by instantiating m with different monads.⁵ The most obvious candidates are different transformer stacks, and the choice is not innocent: it is folklore that the stack a program runs in can change what it does. For example, the two stacks below differ only in the order of StateT and ExceptT. Withdrawing 500 with a fee of 1 from a balance of 100 fails under both, but only the second still returns a balance afterwards, with the fee already deducted:

-- `StateT` outside `Except`: a failed run returns no state at all
#eval ((withdraw (m := ReaderT Nat (StateT Nat (Except String))) 500).run 1).run 100
-- Except.error "insufficient funds"

-- `ExceptT` outside `StateM`: the state survives the failure
#eval (((withdraw (m := ReaderT Nat (ExceptT String (StateM Nat))) 500).run 1).run).run 100
-- (Except.error "insufficient funds", 99)

Based on a trick distilled from Veil, Tapas generates the tagless final form automatically, so that users do not have to spell out these type class parameters themselves.¹ With the infer_effects decorator, a signature may mention m without declaring it:

infer_effects
def withdraw (amount : Nat) : m Unit := do
  /- exactly the same body as above -/
-- withdraw : {m : Type → Type u} → [Monad m] →
--   [MonadReaderOf Nat m] → [MonadStateOf Nat m] → [MonadExceptOf String m] →
--   Nat → m Unit

Up to a universe level, this is the signature we wrote by hand, and the two definitions are in fact equal by rfl. The decorator accepts whatever def accepts, including recursion, where, let rec and mutual blocks, and effects propagate through calls.⁴

Getting different programs out of one definition is only half of the story. The other half, and the subject of the rest of this post, is relating them.

What we want to prove

Sometimes we care about a property relating monadic programs that have the same structure but run in different monads, say m and m'. Such a property can be phrased as a relation R : m α → m' α → Prop, given for every value type α.² For example:

• R may connect symbolic, uninterpreted effects with executable programs. Suppose m contains an uninterpreted effect such as nondeterministic choice (as an operation of a freer monad, say), which we can reason about with a weakest precondition calculus, while m' runs executable programs that answer every choice with a single concrete value. We may then want to prove that every specification satisfied in m is also satisfied in m', as long as answering a choice does nothing else (Extraction).
• R may express a data refinement. Suppose m is StateM Abs and m' is StateM Con, where Abs is an abstract model of some data structure and Con is a concrete implementation of it. We may then want to prove that, starting from initial states related by a refinement relation, the two programs return the same value and end in states that are still related (Store).
• R may express an erasure property. Suppose some ghost operations in m, which only update ghost state, are interpreted as pure () in m'. We may then want to prove that the two programs compute the same results once the ghost state is discarded; in other words, that the program in m' is the program in m with its ghost operations erased (Ghost).

A common way to handle such properties is to first turn the monadic structure into an AST, for instance a freer monad or an interaction tree, and then prove by induction (or coinduction) that, the programs in m and m', obtained by folding the same AST, satisfy R.

As disclaimed at the very beginning, this post makes no warranty of novelty. Still, the author's (not particularly reliable) intuition says that this approach has at least a few inconveniences, which the other approach introduced below avoids to some extent. They are listed here for the reader to judge. Some of them rely on material from later sections, so on a first reading, feel free to skim them and come back afterwards:

• The guarantee is about programs obtained by folding the AST rather than those written directly. For a program written directly, say in tagless final form, relating it to the fold of its reified AST takes a roundtrip theorem, and that theorem is itself an instance of the program's parametricity (toFinal_toFreer_rel in the Freer example). So parametricity is hard to avoid, and it might as well be applied to R directly.
• The type of an AST may forget information that only matters once the two sides are related. In the Extraction example, a choice is requested by the type of its answer, and the type of a reified program does not say which types it chooses from. Folding it into an executable program therefore needs a handler answering every type, which is impossible for a type without values. The signature of a program in tagless final form does record these types, so an execution only has to answer those.
• In Lean, a freer monad may not be directly usable when m and m' allow partial_fixpoint: being inductive, its trees are all finite, leaving nothing to stand for divergence. Interaction trees do have room for divergence, but using them brings in more involved machinery such as coinduction.

The other approach

The other approach supported by Tapas, such as it is, has three parts. The first is the tagless final form inference from the first section: from now on, we assume that every monadic program under consideration is in tagless final form, with its underlying monad as a parameter. Before introducing the other two parts, some intuition may help. Suppose the tagless final monadic programs we consider are built from pure and bind alone, and that R : m α → m' α → Prop satisfies the following two conditions:

• for every x, R (pure x : m α) (pure x : m' α) holds;

• for every x : m α, x' : m' α, f : α → m β and f' : α → m' β, if

  • R x x' holds, and
  • R (f y) (f' y) holds for every y,

  then R (x >>= f) (x' >>= f') holds.

In this case, you can imagine that, given a tagless final monadic program p, some form of induction on the structure of p yields R (p (m := m)) (p (m := m')).

From the perspective of logical relations, this conclusion is essentially the fundamental theorem for the logical relation derived from the type of p, or in other words, the parametricity of p. The other two parts of the approach are, respectively, the mechanism that generates the concrete statement of that logical relation, and the mechanism that proves the parametricity.

Of course, a program may use more than pure and bind. When m implements effects such as state or reader, it may also provide primitive operations like get and read, through type classes like MonadStateOf and MonadReaderOf. These operations need to be related as well; how this is done is the topic of the next section.

Logical relation

Tapas can generate relations for type classes like Monad and MonadStateOf. The generation is mostly recursive and mechanical, and is based on a designated representation parameter, the parameter allowed to differ between the two sides; in our setting, it is the monad parameter m. The relations of Monad and of Lean's common effect classes come pre-generated, and for a class of your own, the command derive_effect_rel C generates one. For a type class C ps whose representation parameter is m : Type u → Type v, the generated declaration is

class C.Rel {ps} {m' : Type u → Type v'} (R : ∀ ⦃α⦄, m α → m' α → Prop)
    [left : C ps] [right : /- C ps, with m replaced by m' -/] : Prop

where {ps} binds the parameters of C, including m. Each field type of C is translated into a relational property, which becomes a field of C.Rel. Here are a few simple principles to give the idea; for the details, see the documentation and the comments in the source code.

• A binder whose type does not mention m is introduced once and shared by both sides, becoming an argument of what is being translated (which may be the field itself or one of its arguments).
• If the conclusion of a field f has type m α, it is translated into R (left.f ...) (right.f ...). For example, pure : {α : Type u} → α → m α is translated into ∀ {α : Type u} (a : α), R (pure a) (pure a).
• A binder whose type mentions m is duplicated, with one copy for each side, and the relation at its type, itself computed recursively, becomes a premise. For example, bind : {α β : Type u} → m α → (α → m β) → m β is translated into

  ∀ {α β : Type u} (x : m α) (x' : m' α), R x x' →
    ∀ (f : α → m β) (f' : α → m' β), (∀ (a : α), R (f a) (f' a)) →
      R (x >>= f) (x' >>= f')
  

By now, it is not hard to see that these two relational properties are exactly what the previous section needed for proving parametricity, and Tapas generates them automatically from the Monad class, which is, well, nice. Concretely, they are two of the fields of Monad.Rel.³ Classes like MonadStateOf go through the same translation; for instance, MonadStateOf.Rel asks for R get get and ∀ s, R (set s) (set s).

For a concrete type T, Tapas can also derive, with derive_type_rel T (repr := m), the logical relation between terms of T with respect to a representation parameter. For a type T ps, the declaration is always

def T.Rel {ps} (left : T.{ls} ps) (right : T.{ls'} ps) : Prop

The core of the translation is the same as for type classes. The difference lies in what gets related: there, each field of the instance left with the same field of right; here, the two given terms left and right themselves. For example, take the type of a tagless final monadic program:

def Tp := {m : Type → Type u} → [Monad m] → [MonadStateOf Nat m] → m Unit

Then Tp.Rel is defined as

fun left right =>
  ∀ {m : Type → Type u} {m' : Type → Type u'}
    (R : ⦃a : Type⦄ → m a → m' a → Prop)
    [inst : Monad m] [inst' : Monad m'], Monad.Rel R →
    ∀ [inst_1 : MonadStateOf Nat m] [inst'_1 : MonadStateOf Nat m'],
      MonadStateOf.Rel R →
        R (@left m inst inst_1) (@right m' inst' inst'_1)

R is inserted here because m is the representation parameter. Since m is bound inside Tp rather than being a parameter of it, Tp.Rel quantifies over every such R, instead of taking one as a parameter as C.Rel does. The instance binders follow the third principle above, each becoming a pair together with a premise.

Parametricity

For a tagless final monadic program p, the command derive_parametric p derives its parametricity, as a theorem p.parametric: it proves Tp.Rel @p @p, where Tp is the type of p. (No Tp or derive_type_rel is needed beforehand; the relation is read off the type of p directly.) The proof procedure is rather heuristic and may fail on some programs, so we will not go into it here.

Since the conclusion of Tp.Rel is R applied to the results of p in the two monads, we only need to prove the premises about R and the particular m and m' beforehand, such as Monad.Rel R and MonadStateOf.Rel R. After that, for every program p whose parametricity can be derived, we know that its instantiations at m and m' satisfy R, without going through any intermediate representation such as a freer monad or an interaction tree. In a sense, this is translation validation: the guarantee is established program by program, by a proof the kernel checks, rather than once and for all.

This remains true for programs defined by partial_fixpoint. Their tagless final form is inferred by a variant of the decorator, infer_effects_partial, which adds the two order parameters a least fixpoint needs, [∀ α, CCPO (m α)] and [MonoBind m], and also gives while and repeat loops a least-fixpoint semantics:

infer_effects_partial
def collatz (n : Nat) : m Nat := do
  modify (· + 1)  -- count the calls
  if n ≤ 1 then return n
  else if n % 2 = 0 then collatz (n / 2)
  else collatz (3 * n + 1)
partial_fixpoint
-- collatz : {m : Type → Type u} → [Monad m] →
--   [∀ α, CCPO (m α)] → [MonoBind m] → [MonadStateOf Nat m] →
--   Nat → m Nat

#guard (collatz 27 (m := StateT Nat Option)).run 0 = some (1, 112)

derive_parametric collatz

derive_parametric handles such programs without needing interaction trees or coinduction. Each side computes its least fixpoint in its own monad, where divergence is simply the least element (none in Option, for instance), and the two fixpoints are related directly (Fixpoint.lean). The price is an extra condition: R must be admissible, i.e., closed under suprema of chains, so collatz.parametric has one more premise than usual, ∀ ⦃α⦄, AdmissibleRel R. The order parameters CCPO and MonoBind of the two sides need no relational premise. In Ghost, for instance, a program with a while loop runs in StateT Nat Option with its ghost state and in Option with its ghost operations erased, since Id has no room for divergence; the admissibility of the erasure relation between the two is proved once and for all by Erase.admissible.

The three applications above are all handled this way. Each of them proves the premises for its relation once: Monad.Rel, MonadStateOf.Rel and the relation of the choice interface in Extraction, the last one for each executable way of answering choices; Monad.Rel and the relation of the store interface in Store; Monad.Rel and the relation of the ghost interface in Ghost. Every program is then covered by a single application of its parametricity theorem. In Store, for instance, the refinement certificate of a program is literally transfer.parametric amount R monadRel storeRel.

Summary

That more or less covers what Tapas offers. For the rest, have a look at the examples listed in the README, some of which were briefly introduced above.

Looking back, you may notice that this post only talks about applications to monads. Tapas itself is not specific to monads, as the first two examples in the README show, but are there other applications as interesting as the monadic ones? Perhaps, perhaps not; the author has not had the time to think that far. That is a question for another day.