Computation Types to Track Dependences
A main goal for F*’s effect system is to track dependences among the various parts of a program. For example, the effect system needs to ensures that the total part of a program that is proven to always terminate never calls a function in the divergent fragment (since that function call may loop forever). Or, that the runtime behavior of a compiled program does not depend on ghost computations that get erased by the compiler.
In a paper from 1999 called A Core Calculus of Dependency, Abadi et al. present DCC, a language with a very generic way to track dependences. DCC’s type system includes an indexed, monadic type \(T_l\), where the index \(l\) ranges over the elements of a lattice, i.e., the indexes are arranged in a partial order. DCC’s type system ensures that a computation with type \(T_l\) can depend on another computation with type \(T_m\) only if \(m \leq l\) in the lattice’s partial order. F*’s effect system is inspired by DCC, and builds on a 2011 paper by Swamy et al. called Lightweight Monadic Programming in ML which develops a DCC-like system for an ML-like programming language.
At its core, F*’s effect system includes the following three elements:
Computation Types: F*’s type system includes a notion of
computation type, a type of the form
M t where
M is an
effect label and
t is the return type of the computation. A term
e can be given the computation type
M t when executing
exhibits at-most the effect
M and (possibly) returns a value of
t. We will refine this intuition as we go along. In contrast
with computation types, the types that we have seen so far (
list int, other inductive types, refinement
types, and arrows) are called value types.
Partially Ordered Effect Labels: The effect label of a computation
type is drawn from an open-ended, user-extensible set of labels, where
the labels are organized in a user-chosen partial order. For example,
under certain conditions, one can define the label
M to be a
M < N. For any pair of labels
N, a partial function
lub M N (for least upper bound)
computes the least label greater than both
N, if any.
Typing Rules to Track Dependences: The key part of the effect
system is a rule for composing computations sequentially using
= e1 in e2. Suppose
e1 : M t1, and suppose
e2 : N t2
x:t1, then the composition
let x = e1 in e2 has type
L t2, where
L = lub M N—if
lub M N is not defined, then
let-binding is rejected. Further, a computation with type
t can be implicitly given the type
N t, when
M < N, i.e.,
moving up the effect hierarchy is always permitted. The resulting
typing discipline enforces the same dependence-tracking property as
DCC: a computation
M t can only depend on
N t when
lub M N =
In full generality, F*’s computation types are more complex than just
an effect label
M and a result type (i.e., more than just
t), and relying on F*’s dependent types, computation types do more
than just track dependences, e.g., a computation type in F* can also
provide full, functional correctness specifications. The papers
referenced below provide some context and we discuss various elements
of these papers throughout this part of the book.
Verifying Higher-order Programs with the Dijkstra Monad, introduces the idea of a Dijkstra monad, a construction to structure the inference of weakest preconditions of effectful computations.
This 2016 paper, Dependent Types and Multi-Monadic Effects in F*, has become the canonical reference for F*. It shows how to combine multiple Dijkstra monads with a DCC-like system.
Dijkstra Monads for Free presents an algorithm to construct Dijkstra monads automatically for a class of simple monads.
Dijkstra Monads for All generalizes the construction to apply to relate any computational monad to a specificational counterpart, so long as the two are related by a monad morphism.
Programming and Proving with Indexed Effects describes F*’s user-defined effect system in its most general form, allowing it to be applied to any indexed effects, including Dijkstra monads, but several other constructions as well.