Efficient Lambda Encodings for Mendler-Style Coinductive Types in Cedille

Preliminaries

Derived Constructs

Figure 3: Derived datatypes: Pairs and the Unitary Type

Mono, Internalized Positivity

F : (I → U) → I → U, Mono I F

Rec, A Recursive Type Former

F : (I → U) → I → U, Rec I F  (μ)

Ordinary F-Coalgebras

F : C → C, λ(X : U).X → F X

Mendler-Style F-Coalgebras

coalgm = λ(X : U).λ(R : U).(X → R) → X → F(R)

Final Mendler F-Coalgebras

anamorphism

X → νF

Nu = (X : U) × X × coalgm(X),

(Y : U) → ((X : U) → X → CoAlgM(X) → Y) → Y

Mendler-Style Coiteration

out : νF → F(νF),

Mendler-Style Corecursion

Mendler-Style Course-of-Values Coiteration

Generic Lambda Encoding for Codata

Functional Programming With Streams

Coinductive Proofs of Properties of Streams