Efficient lambda encodings for Mendler-stylecoinductive types in Cedille

Chris Jenkins, Aaron Stump, Larry Diehl
August 30, 2020
University of Iowa, Dept. of Computer ScienceIntroduction

Coinductive types and their lambda encodings• Coinductive (coalgebraic) types classify (possibily) infinite objects.
They come with
• Destructors for making finite observations• Generators for their production (corecursion schemes)• And we often desire productivity for these corecursion
schemes (i.e., all finite observations are well-defined)• Lambda encodings are an identification of the codatatype with aparticular corecursion scheme• Codata are lambda expressions• Types defined impredicatively (“impredicative encodings”)• Productivity for a given scheme comes for free if the corresponding
encoding is definable in a total type theory
Why not adopt encodings where this matters? (total FP, ITPs)
1

Lambda encodings: some difficulties

Historically, lambda encodings for inductive types faced difficulties(efficiency and logical expressivity). Similarly for coinductive types.

Efficiency of corecursion for streams (in # of observations)• Church: constructors incur linear overhead
Constructors trigger re-generation of codata• Parigot: flat linear overhead
Additional case distinction for each observation
Overhead can be much worse for other coinductive types. . .

2Datatypes as primitives

Inefficiency, and the lack of (co)induction in CC (logicalexpressivity), motivates the development of the calculus of(co)inductive constructions (CIC), where primitive (co)inductive
datatypes are added to the theory.
Primitive datatypes with induction swell the TCB (positivity
checking, possibly termination checking). Support for moreexpressive (co)recursion schemes may require further changes tothe meta-theory.

3

Lambda encodings: some remedies

CDLE
The calculus of dependent lambda eliminations (CDLE) is aformally small extension of Curry-style CC that addresses theforegoing issues for lambda encodings directly• induction is derivable generically for many encodings• it possible to define efficient encodings for inductive types
Cedille is a higher-level language with special syntax for inductive
types elaborated to lambda terms in CDLE.
What about coinductive types?

4Lambda encodings: some remedies

CDLE
The calculus of dependent lambda eliminations (CDLE) is aformally small extension of Curry-style CC that addresses theforegoing issues for lambda encodings directly• induction is derivable generically for many encodings• it possible to define efficient encodings for inductive types
Cedille is a higher-level language with special syntax for inductive
types elaborated to lambda terms in CDLE.
What about coinductive types?

4This talk

A Mendler-style encoding for codata in CDLE that is• Generic: works for any positive datatype signature• Efficient: no penalty for constructors• Expressive: supports a combined course-of-values coiteration andprimitive corecursion scheme
Missing: true coinduction (bisimilarity ⇒ equality), with a counter-result
wrt CDLE’s primitive equality type. Indexed corecursion for reasoning issupported (see the paper).

5

Focus of the talk

Focus: How we guarantee efficiency for just the primitive
corecursion scheme.
• How the Mendler-style helps• Monotone fixed point types (Matthes, 1998)• Proof-irrelevant type inclusions (CDLE)

6

Mendler-style schemes forcorecursion

What are “Mendler-style” corecursion schemes

For every “classic” structured corecursion scheme, there is an equivalentMendler-style scheme

Advantages of the Mendler-style• More idiomatic for FPers
Explicit corecursive calls, like general corecursion• Avoids intermediate structures in more complex schemes
No build up / tear down assists in efficiency gain

7

Coiteration (streams)

Classic
h:S →A t:S →S
coit h t : S → Stream A

head (coit h t s)
tail (coit h t s)

hs
coit h t (t s)Conceptually: t : S → S is a “state transition”

Mendlerh : S → A t : ∀R.(S → R) → S → R
mcoit h t : S → Stream A

head (mcoit h t s)
tail (mcoit h t s)

htt (mcoit h t) s|{z}
R:=Stream A

Conceptually: t : ∀R.(S → R) → S → R is a “generator transformer”

8Primitive corecursion (streams)“Short-circuit” generation by returning a pre-made stream

Classic
h : S → A t : S → Stream A + S
corec h t : S → Stream A
head (corec h t s)
tail (corec h t s)

hscase (t s) of in1 (x) ⇒ x | in2 (y ) ⇒ corec h t yObservations require additional case distinction

Mendlerh:S →At : ∀R.(Stream A → R) → (S → R) → S → R
mcorec h t : S → Stream A

head (mcorec h t s)
tail (mcorec h t s)

hst (λ x. x) (mcorec h t) s
| {z }

R:=Stream A

Additional β-redex can be removed in CDLE

9

Monotone recursive types and proof
irrelevant type inclusions in CDLE

Review: recursive types
The impredicative encoding obtained from a direct reading of mcorec
requires recursive types.
h:S →At : ∀R.(Stream A → R) → (S → R) → S → R
mcorec h t : S → Stream A

Recursive types
For a type scheme F , a recursive type µF is one such that:• exists roll : F (µF ) → µF
• and exists unroll : µF → F (µF )• such that unroll (roll t) reduces to t (β-law)

10

Positive recursive types

Unrestricted recursive types lead to non-termination, with theculprits schemes F with negative occurrences of their typeargument.
Can use syntactic notion of positivity to recover termination, or. . .
Monotone fixedpoint types• f monotone iff ∀x, y .x ≤ y =⇒ f (x) ≤ f (y )• Generalize monotonicity to type theory
Need to interpret ≤, =⇒11

Representing monotonicity

Can interpret monotonicity in System F, but for recursive types
this leads us back to Church encodings (β-law not satisfied).
CDLE twist: proof-irrelevant type inclusions
PreorderSystem FCDLEs≤t
S →TCast S T∀x, y .x ≤ y =⇒ f (x) ≤ f (y )∀X , Y .(X → Y ) → F X → F Y∀X , Y .Cast X Y ⇒ Cast (F X ) (F Y )12Erasure and irrelevance in CDLE

• CDLE is Curry-style: type annotations are external to the “real”
term language (untyped lambda calculus) and are all erased• Definitional equality is “up to erasure”|Λ X . λ x : X . x| = λ x. x = |λ x : T . x|
• Term arguments to functions can also be irrelevant• t : T 0 ⇒ T means t is a function taking a T 0 argument, but
the T it returns does not depend on the choice of thisargument• for t 0 : T 0 , application t -t 0 : T , and |t -t 0 | = |t|13

Proof irrelevant type inclusions

Type inclusions Cast S T are a derived notion in CDLE.
For brevity they are presented axiomatically (full defs. in appendix).

Cast S T (elimination, erasure)c : Cast S T
elimCast -c : S → T|elimCast -c| = λ x. x

Takeaway: type inclusions are computationally irrelevant!

14

Monotonicity

Mono F =df ∀X , Y .Cast X Y ⇒ Cast (F X ) (F Y )We can deriveMono F (elimination, erasure)m : Mono F c : Cast S T
elimMono -m -c : F S → F T|elimMono -m -c| = λ x. x

Takeaway: monotonicity witnesses are computationally irrelevant!

15

Recursive types

Rec (constructor, destructor, erasure)m : Mono F
roll -m : F (Rec F ) → Rec F|roll -m| = λ x. x

m : Mono F
unroll -m : Rec F → F (Rec F ) |unroll -m| = λ x. x

• roll and unroll are part of a two-way type inclusion between
F (Rec F ) and Rec F• β-law easily satisfied!

16

The generic encoding

Generic variant Mendler encoding
F : ? → ? and monoF : Mono F are parameters to the development
For simplicity, the below encoding has support for CoV coiteration
removed (see paper for full definition).

Generic codatatype Nu
CoAlg S C =df
Nu =df∀ R. (Cast C R) ⇒ (S → R) → S → F R
Rec λ C . ∃ X . X × CoAlg X C|{z}positive in C

• S is the “state space”, C is the fixedpoint parameter• Existential encoding is standard for codata(Church: ∃ X . X × (X → F X ))17

Efficient destructor

The type scheme in the definition of Nu is positive, so we can use
roll and unroll to define the generator and destructor
satisfying:
Generator and destructor
c : CoAlg S Nu
unfoldM c : S → Nu
erased!

outM (unfoldM c s)z }| {|c -castRefl{z} (unfoldM c) s
R:=Nu

No overhead for primitive corecursion!

18

Efficient codata constructor

inM:

F Nu → Nu
F Nu→F Rz}|{=df unfoldM (F Nu) Λ R. Λ c. λ g . elimMono -monoF -c
Ordinarily, use g : F Nu → R to corecursively re-generate. But• c : Cast Nu R and monoF : Mono F• so |elimMono -monoF -c| = λ x. x
Consequently, outM (inM t)t for all t• No re-generation of codata (Church)• No traversal over F with fmap (Church and Parigot)⇒ no penalty for constructors!
19

Conclusion

Summary and proviso• Generic derivation of codata in CDLE supporting an
expressive corecursion scheme efficiently.
• Required a different approach than used for efficient inductivetypes – monotone recursive types á la Matthes• Termination guarantee in CDLE is somewhat subtle• Holds for closed terms which can be assigned a function typeThis includes all (closed) (co)data. Computing with openterms is in general unsafe• The features used to guarantee efficiency contribute to theproviso

20Future work

• Ongoing work on an encoding with coinduction “up to” anequivalence relation derived from binary parametricty
Rather than CDLE’s primitive equality type (used in thecounter-example)• Design of a nice surface-language syntax for codata(copattern matching, coercive subtyping using type inclusions)Mendler-style formulation helps bridge the gap between syntax
and semantics: productivity checking reduced to type checking
while maintaining a familiar style of explicit corecursive calls

21Thanks!

22