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

- Version 1.2 source (requires Standard ML of New Jersey, Version 0.93)
- Standard Prelude
- Examples
- Complete distribution (22K compressed tar file)