Murat Kasimov

More about me

Я language (β)

/Я language (β)/Tutorials/Lambda calculus interpreter 1/

Full source codeTwitter discussionNext chapter

We start with the most classic way to define AST and then gradually move to more sophistacated ones.

For the sake of simplicity, let identifiers be a single latin character (so only 26 unique variables are available).

So a regular term is either an abstraction, an application or a variable:

: Term ~ Along `T'I` Latin `S'T'I'TT'I` Twice `S'T'I'TT'I` Flout `T'I` Latin

Since we never define our own datatypes here but rather construct from basic ones - patterns serve a role of constructors:

> Abstraction i ii = Clasp ( This ( Clasp ( This ( Along ( These ii i ) ) ) ) ) > Application i ii = Clasp ( This ( Clasp ( That ( Twice ( These i ii ) ) ) ) ) > Variable i = Clasp ( That ( Flout i ) )

We declare all three options as a covariant functor, therefore their Sum composition is also a covariant functor - we can use its parameter as an embedding if we apply it to a fixpoint combinator:

: Expression ~ Recursive Term

Using this version of AST we can declare (abstraction) identity function this way:

> ... = Recursive `har_` Abstraction `har'st` X >> `har'st` Recursive `ha` Variable `ha` X

And this is how we can provide an argument (application) to identity function:

> ... = Recursive `har___` Application >> `har__` Recursive `har_` Abstraction `har'st` X >>> `har'st` Recursive `ha` Variable `ha` X >> `har__'st` Recursive `ha` Variable `ha` Y

These chunks of code look a bit too verbose, we can come up with more specialised patterns:

> ABS i ii = Recursive ( Abstraction i ii ) > APP i ii = Recursive ( Application i ii ) > VAR i = Recursive ( Variable i )

Now both abstraction an application of identity function fit in one line:

> ABS `har'st` X `har'st` VAR `ha` X : Expression > APP `har_` ABS `har'st` X `har'st` VAR `ha` X `har_'st` VAR `ha` Y : Expression

In other words verbosity is not an issue... Our issue is that Term is a functor and Recursive Term is not!

There is a way to fix that without sacrificing expressibility.