Definition

Following the definition of the operational package, interfaces in FreeSpec are parameterized inductive types whose terms purposely describe the primitives the interface provides.

Given i : interface, a term of type i α identifies a primitive of i expected to produce a result of type α. The simpler interface is the empty interface, which provides no primitives whatsoever.

Another example of general-purpose interface we can define is the STORE s interface, where s is a type for a state, and STORE s allows for manipulating a global, mutable variable of type s within an impure computation.

According to the definition of STORE s, an impure computation can use two primitives. The term Get : STORE s s describes a primitive expected to produce a result of type s, that is the current value of the mutable variable. Terms of the form Put x : STORE s unit describe a primitive which does not produce any meaningful result, but is expected to update the current value of the mutable variable. The use of the word “expected” to describe the primitive of STORE s is voluntary. The definition of an interface does not attach any particular semantics to the primitives it describes. This will come later, and in fact, one interface may have many legitimate semantics. Impure computations are likely to use more than one interface, but the impure monad takes only one argument. We introduce iplus (denoted by <+> or ⊕) to compose interfaces together. An impure computation parameterized by i ⊕ j can therefore leverage the primitives of both i and j.

Polymorphic Interface Composites

When defining general-purpose impure computations that we expect to reuse in different context, we want to leave the interface as a parameter, and rather express the constraints in terms of interface availability. We tackle this challenge by means of interface composites.

• We say an interface composite ix provides a concrete interface i when there exists a function inj_p : ∀ α, i α → ix α.
• Conversely, we can determine if a primitive of an interface composite ix is forwarded to a concrete interface i when there exists a function proj_p : ∀ α, ix α → option (i a).

We encode this mechanics using two type classes: MayProvide, and Provide.

We provide a default instance for MayProvide in the form of a function proj_p which always return None. We give to this default instance a ridiculously high priority number to ensure it is selected only if no other instances are found.

It is expected that, for an interface composite ix which provides i and may provide j, inj_p and proj_p do not mix up i and j primitives. That is, injecting a primitive e of i inside ix, then projecting the resulting primitive into j returns None as long as i and j are two different interfaces.

Manipulating MayProvide, Provide and Distinguish manually quickly becomes verbose, especially due to the combinatorial nature of Distinguish. In an attempt to make things easier for FreeSpec users, we provide ProvideN and StrictProvideN (with N from 2 to 5). ProvideN can be used to define impure computations which use N interfaces, while StrictProvideN can be used to reason about said computations (StrictProvideN requires the N interfaces to be different, thanks to the Distinguish type class).

Composing Interfaces

We provide the iplus operator to compose interface together. That is, iplus can be used to build concrete (as opposed to polymorphic) interface composite.

For iplus to be used seamlessly as a concrete interface composite, we provide the necessary instances for the MayProvide, Provide and Distinguish type classes. Note that these instances always prefer the left operand of iplus. For instance, considering a situation where there is an instance for Provide ix i and an instance for Provide jx i, the instance of Provide (ix + jx) i will rely on ix. The main use case for iplus is to locally provide an additional interface. For instance, we can consider a with_state function which would locally give access to the STORE interface, that is with_state : ∀ ix s α, s → impure (ix + STORE s) α → impure ix α. In such a case, the interface made locally available shall be the right operand of iplus. This way, functions such as with_state are reentrant. If we take an example, the following impure computation:

with_state true (with_state false get)

will return false (that is, the variable in the inner store).

By default, Coq's inference algorithm for type classe instances inference is a depth-first search. This is not without consequence in our case. For instance, if we consider the search of an instance for MayProvide (i + j) j, Coq will first try iplus_right_MayProvide (as explained previously), meaning he now search for MayProvide i j. It turns out such an instance exists: default_MayProvide. To circumvent this issue, we write a dedicated tactic find_may_provide which attempts to find an instance for MayProvide (?ix + ?jx) ?i with refl_MayProvide, iplus_left_MayProvide and iplus_right_MayProvide.