The functional language lemon is based on the simply-typed lambda calculus augmented with sums, products, and the mu and nu constructors for least (inductive) and greatest (coinductive) solutions to recursive type equations. The term constructors of the language strictly follow the introduction and elimination rules for the corresponding types; in particular, the elimination for mu is iteration and the introduction for nu is coiteration (also called generation). It includes a small amount of polymorphism and type inference; lambda-bound variables do not need type annotations, but iteration and coiteration need to have their corresponding recursive types specified (this is a problem with the language rather than the implementation).
For example, the following program generates the stream of Fibonacci numbers starting with 1,1:
type nats = nu X. nat * X; -- nat stream is a pair of a nat and a stream
val fibs = <|nats, \p. <pi1 p, -- head of stream is next Fibo. number
<pi2 p, plus (pi1 p) (pi2 p)>>
-- "seed" for rest of stream
|> <1, 1>; -- initial seed for generation
Using iteration we may define a function which picks off the first n elements of a stream and returns them as a list:
val pick = \n. -- number of elements to pick
\ns. -- input stream
pi1 ([|nat, [\x. <nil, ns>, -- empty list on zero
\p. (\q. <cons (pi1 q) (pi1 p),
-- cons head of stream on list
pi2 q>) -- rest of stream for iteration
(unfold nats (pi2 p))]
-- get next stream element
|] n); -- iteration over n
We may combine these terms as follows (currently there is syntactic sugar for natural numbers but not for lists; formatting inserted by hand for clarity):
> pick 4 fibs;
it = fold mu X. 1 + nat * X (in2 (<3,
fold mu X. 1 + nat * X (in2 (<2,
fold mu X. 1 + nat * X (in2 (<1,
fold mu X. 1 + nat * X (in2 (<1,
fold mu X. 1 + nat * X (in1 (<>))>))>))>))>)) : mu X. 1 + nat * X