Efficient lambda encodings for Mendler-style coinductive types in Cedille

Summarizing, in this paper we:

• •

  generically derive Mendler-style lambda encodings for coinductive datatypes in CDLE using derivable monotone recursive types;

• •

  show that codata so derived forms an adequate basis for functional programming due to the expressive course-of-values corecursion scheme it supports for generating codata and their efficient codata constructors (in the sense that the run-time overhead of every use of a constructor is constant in the number of observations made on the codata);

• •

  show that our derived codata supports a proof principle in the form of indexed course-of-values corecursion, which suffices for proving many standard examples of coinductive properties such as relational properties over corresponding elements of two streams;

• •

  and describe a negative result concerning Lambek’s lemma that indicates the impossibility of coinduction in the sense of “bisimilarity implying equality” (with respect to CDLE’s built-in equality) for this encoding; this in turn explains the use of monotone recursive types, as the lack of such a coinduction principle raises fundamental difficulties in adapting for this encoding previous approaches for deriving efficient encodings for inductive types in CDLE.

The remainder of this paper is organized as follows: in Section 2 we review CDLE and Mendler-style corecursion schemes; in Section 3 we detail the generic derivation of coinductive data, discussing its strengths and the above-mentioned negative result; in Section 4 we give concrete examples of programming with streams using expressive corecursion schemes supported by our derived codatatypes; in Section 5 we argue that the indexed coiteration scheme they support enables proofs of many properties of interest for coinductive types such as streams; in Section 6 we discuss related and future work; and we conclude in Section 7. All code found in listings can be found at https://github.com/cedille/cedille-developments and is checkable by the Cedille tool, and implementation of CDLE available at https://github.com/cedille/cedille/releases.

In Figure 4, our variant Mendler-style $F$-coalgebra, CoAlgM, generalizes the description given in Section 2.3 to type families X: I $\to$ $\star$. CoAlgM takes an additional type family argument C, and describes a family of polymorphic functions whose arguments facilitate a combined course-of-values corecursion scheme for codata. The variable C stands in for occurrences of the generic codatatype Nu – which itself recursively defined in terms of CoAlgM. In the body of the definition, the first additional argument is a cast from C to the quantified R, enabling corecursion by allowing us to produce (for any i of type I) some term of type R i from some pre-existing codata of type C i, rather than via ch. The second argument is an abstract constructor: given some collection of subdata of type F $\cdot$R i (for any i), it builds a value of type R i. This additional argument enables course-of-values coiteration: for each single step of codata generation, an arbitrary number of observations that will be made of the codata can be constructed. The remaining arguments are the same as for ordinary Mendler-style $F$-coalgebras: ch is the handle for making coiterative calls, and the argument of type X i is the value from which we are to coiteratively construct the result of type F $\cdot$R i.

Type family NuF is defined using the standard type for lambda encodings of existentials and products, and its body is more naturally read as $\exists$ X: I $\to$ $\star$. X i $\times$ CoAlgM $\cdot$C $\cdot$X. This is similar to the standard definition of the greatest fixpoint of F (Section 2.3, see also [39]). NuF is parameterized by a type family C: I $\to$ $\star$ standing in for recursive reference to a fixpoint of itself. That fixpoint is Nu, defined as Rec $\cdot$I $\cdot$NuF.

As discussed earlier, recursive types must be restricted in some fashion to positive (monotonic) type schemes only. The term monoNuF in Figure 5 (definition omitted, indicated by <..>) proves that the type scheme NuF is positive; it uses evidence monoCoAlgM that CoAlgM is positive in its first argument. To show that a type scheme is positive (Mono, Section 2.2), we use intrMono and may then assume two type families C1 and C2 and a cast c between them. Aside from monoCoAlgM, in code listings we omit monotonicity proofs as once the general principle is understood these can be quite tedious to work through.

For monoCoAlgM, the goal is to show there is a cast from CoAlgM $\cdot$C1 $\cdot$X to CoAlgM $\cdot$C2 $\cdot$X (for any X of kind I $\to$ $\star$). This is done with intrCast (also in Section 2.2), whose first argument is simply a function of this type and whose second is a proof that this function is extensionally equal to ${\lambda}\,\mathit{x}.\,x$. For the functional argument, it is simply a matter of deriving a Cast $\cdot$I $\cdot$C1 $\cdot$R (needed for the assumed coa of type CoAlgM $\cdot$C1 $\cdot$R) from the given c’ of type Cast $\cdot$C2 $\cdot$R and c of type Cast $\cdot$C1 $\cdot$C2, which we have by castTrans, the composition operator for casts. This new cast is given to coa as an erased argument, so the function simply erases to $\lambda$ coa. coa, and therefore the proof that this is extensionally equal to ${\lambda}\,\mathit{x}.\,x$ is trivial ($\lambda$ coa. $\beta$), since it is intensionally equal to it.

With these proofs that NuF is a positive type scheme, we can define the rolling and unrolling operations nuRoll and nuUnroll for the recursive type family Nu.

We now discuss the definitions given in Figure 6. Function unfoldM is the generator for our Mendler-style codata. For any type family X of kind I $\to$ $\star$, given some coa of type CoAlgM $\cdot$Nu $\cdot$X and some x of type X i (for arbitrary i of type I), we generate a term of type Nu i by first invoking nuRoll, which obligates us to produce some argument of type NuF $\cdot$Nu i. Unfolding the definition of NuF, we provide for this an encoded existential: a function polymorphic over a type family Y of kind I $\to$ $\star$ taking another function f of type $\forall$ X: I $\to$ $\star$. X i $\to$ CoAlgM $\cdot$Nu $\cdot$X $\to$ Y i and applying f to the given x and coa.

Our generic constructor inM is defined in terms of unfoldM. The coalgebra given to unfoldM ignores its argument ch and instead casts (using cm, the module parameter that proves monotonicity of F, and c, the coalgebra’s assumed Cast $\cdot$I $\cdot$Nu $\cdot$R) the assumed x of type F $\cdot$(Nu $\cdot$F) to the type F $\cdot$R. Avoidance of ch, the coalgebra’s handle for coiterative calls, ensures that inM is efficient – future observations of the codata constructed with inM will not needlessly rebuild the sub-components of the codata with which it was constructed. This discussion is made more concrete in Section 3.1.

Finally, outM is our generic destructor for codata. Given some co of type Nu i, we use the unrolling operation for recursive type Nu on co to produce a term of type NuF $\cdot$Nu i. Unfolding the definition of NuF, we provide the resulting expression a function which assumes a type family X of kind I $\to$ $\star$, a term x of type X i, and a coalgebra coa of type CoAlgM $\cdot$(Nu $\cdot$F) $\cdot$X. In the body of this given function, we eliminate coa by instantiating its type argument to Nu $\cdot$F and giving it a cast from Nu $\cdot$F to Nu $\cdot$F (using castRefl), the constructor inM, a handle for making coiterative calls unfoldM coa, and the assumed x. We can show in Cedille that the computation rules expected of our derived codatatype Nu and generator unfoldM (Section 2.3) hold by $\beta$-equivalence (the cast argument, corresponding to ${\lambda}\,\mathit{x}.\,x$ in the computation rule for the corecursion scheme, is erased; inM corresponds to $\mathit{out}^{-1}$):

reduce :  X: I  .  coa: CoAlgM Nu X.  i: I.  x: X i.
  { outM (unfoldM coa x)  coa inM (unfoldM coa) x }
=  X.  coa.  i.  x.  .

In Figure 8, StreamF is the signature for streams of elements of type A (where A is a module parameter; it is implicitly quantified over in all definitions in the figure), defined in terms of Pair (Figure 3); the definition of StreamF is more recognizable in the form $R\mapsto A\times R$. Term monoStreamF is a witness to the fact that StreamF is positive (definition omitted, indicated by <..>).

The import of module nu/nu instantiates that module’s parameters with index type Unit, signature functor StreamF, and positivity proof monoStreamF. Type Stream is the greatest fixpoint of StreamF with a fixed index of unit. Destructors head and tail are defined in terms of the generic destructor out and pair projections fst and snd. The generator unfoldStream has a first argument of type StreamCoAlg $\cdot$X, which specializes CoAlgM such that the type families for the codatatype and carrier ignore their Unit indices. The body of the definition of unfoldStream is omitted, as it is somewhat cluttered by type annotations to replace the assumed i: Unit with the constant unit in the type of the coalgebra given to unfoldM. We define this function so that the following examples may use it, and not be themselves so cluttered.

Our first function map is an example of coiteration over streams. First, note that this and following functions occur in a different module than the definition of Stream, so now the element type must be given explicitly both for Stream and unfoldStream. With a function f of type A $\to$ B, in the body of map we generate using unfoldStream a stream with elements of type B from: a coalgebra wherein map (of type $\forall$ i: Unit. Stream $\cdot$A $\to$ R i) can be used for corecursive calls; and a seed value xs of type Stream $\cdot$A. In the body of the given coalgebra, we construct a StreamF $\cdot$A by supplying for the head f (head xs) and for the tail map -i (tail xs) (of type R i).

In a high-level surface language supporting copatterns [2], the definition of map might look like:

head (map f xs) = f (head xs)
tail (map f xs) = map f (tail xs)

Function mapHd is an example of corecursion. Recall that the corecursion scheme supports an alternative for generating codata: it may be given directly in a coalgebra, rather than being generated from coiteration. This mirrors the situation for iteration (where predecessors must be iteratively rebuilt) and recursion (where they are available “for free”) for inductive types. In the definition, with function f of type A $\to$ A, we produce the desired stream by providing for its head f (head xs) and for its tail tail xs, after coercing its type to the desired R i using the given cast c from Stream $\cdot$A to R i.

Using a high-level surface language, the definition of mapHd might look like:

head (mapHd f xs) = f (head xs)
tail (mapHd f xs) = tail xs

mapHd’ f xs = go (in1 xs) where
  go : Sum (Stream A) (Stream A)  Stream A
  head (go (in1 ys)) = f (head ys)
  head (go (in2 ys)) = head ys
  tail (go (in1 ys)) = go (in2 (tail ys))
  tail (go (in2 ys)) = go (in2 (tail ys))

Our final example exch, a function which swaps the positions of every two elements of a stream, demonstrates the course-of-values coiteration scheme, wherein each step of generating codata may describe an arbitrary number of the observations made of that codata (pairwise exchange only requires the construction of one additional observation at each step). In the coalgebra given in the definition of exch, we make three local definitions (using Cedille’s syntax $[x:T=t_{\_}1]-t_{\_}2$, to be read $\texttt{let}\ x:T=t_{\_}1\ \texttt{in}\ t_{\_}2$; we use an additional space to distinguish hyphens used for local definitions from hyphens used in erased applications). These local definitions are: hd1, the second element of the stream xs; hd2, the first element; and tl2, the exchange of elements of the second tail of xs. These definitions are then incorporated into the produced stream, where in the tail we use the abstract constructor v of type $\forall$ i: Unit. StreamF $\cdot$A $\cdot$R i $\to$ R i.

In a higher-level language, exch can be written using nested copatterns (because each step of generation produces a static number of future observations; course-of-values coiteration permits this number to be dynamically computed at each step):

head (exch xs)        = head (tail xs)
head (tail (exch xs)) = head xs
tail (tail (exch xs)) = exch (tail (tail xs))

The signature for generalized stream relations, StreamRelF, takes a type family R: Pair $\cdot$Stream $\cdot$Stream $\to$ $\star$ (standing in for recursive occurrences of the greatest fixpoint of StreamRelF itself) and a pair p: Pair $\cdot$Stream $\cdot$Stream of the two streams to be related, and in the body is defined as the type of pairs of proofs that the first elements of the two streams are related by Rel and proofs that the tails of the streams are related by R. This type scheme is positive in R, as proven by monoStreamRelF (definition omitted). We instantiate the generic codata derivation with these definitions and define StreamRel as the greatest fixpoint of StreamRelF. Destructors headRel and tailRel are given (their definitions are similar to head and tail for streams and so are omitted), as well as the simplified generator unfoldStreamRel: the properties we shall prove using StreamRel require only indexed coiteration, so unfoldStreamRel forgoes the facilities for more advanced generation schemes (namely, indexed course-of-values coiteration) in order to simplify their proofs.

To prove reflexivity of StreamRel assuming reflexivity of Rel, we use for the generator the type family of proofs that two streams are equal. In the body of the coalgebra given to unfoldStreamRel we have the following obligations: for the head we must prove Rel (head xs) (head ys), given by rewriting (with $\rho$, Figure 1) by the assumed g: {xs $\simeq$ ys} and using the assumption that Rel is reflexive; for the tail we must prove R (tail xs) (tail ys), given by providing the coinductive hypothesis ch with a proof that {tail xs $\simeq$ tail ys}.

To prove symmetry of StreamRel assuming symmetry of Rel, we use for the generator the type family, over streams ys and xs, of proofs that xs is related to ys. In the body of the coalgebra given to unfoldStreamRel we have the following obligations: for the head we must prove Rel (head ys) (head xs), given by invoking the proof sym that Rel is symmetric on a proof of Rel (head xs) (head ys) which we extract from the head of the assumption g: StreamRel xs ys; for the tail we must prove R (tail ys) (tail xs), given by providing the coinductive hypothesis ch with a proof of StreamRel (tail xs) (tail ys), extracted from the tail of g.

To prove transitivity of StreamRel assuming transitivity of Rel, we use for the generator the type family (locally named X) over streams xs and zs of proofs that there exists a ys: Stream such that StreamRel xs ys and StreamRel ys zs. In the body of the coalgebra given to unfoldStreamRel, we first unpack the existential g to access these assumptions directly. For the head (locally named hd) we must prove Rel (head xs) (head zs), given by invoking the proof tra that Rel is transitive on proofs that Rel (head xs) (head ys) and that Rel (head ys) (head zs). For the tail (locally named tl) we must prove R (tail xs) (tail zs), given by invoking the coinductive hypothesis ch on a proof that their exists some stream ys’ such that StreamRel (tail xs) ys’ and StreamRel ys’ (tail zs); tail ys is such a stream, with the required proofs extracted from the tails of the proofs that StreamRel xs ys and StreamRel ys zs.