Lazy Lambda Interpreter

O — CPS language with general recursion

Definition

Simple Lambda Calculus

The untyped lambda language O is the simplest language used in OM to generate backend programs. This subset of OM is used as the output of type erasure.

I ::= #identifier T ::= I | ( T ) | T T | λ I → T

AST

data o: Type := (var: name → o) (app: o → o → o) (lambda: name → o → o → o)

Erased

Terms in untyped lambda pure language.

$ om print fst erase a "#List/Cons" ( λ Head → ( λ Tail → ( λ Cons → ( λ Nil → ((Cons Head) ((Tail Cons) Nil)))))) ok

Extract

Erlang extracted code. For other targets you may want to read Code Extract notes.

'Cons'() -> fun (Head) -> fun (Tail) -> fun (Cons) -> fun (Nil) -> ((Cons(Head))((Tail(Cons))(Nil))) end end end end.

Resources

  1. Om archives.
  2. Inf archives.
  3. Git sources.
  4. Inf git sources.