Murat Kasimov

More about me

Я language (β)

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

Full source code ⋅ Previous chapter ⋅ Next chapter

Okay, let's take a look at Instruction covariant functor coupled with a specialised natural transformation:

> `kyo` : ∀ a o , ∃ t' tt' . Instruction t' a `AR____` Along ( List `T'I` tt' Unit ) a `AR__` o `AR__` Instruction t' o

So we have t' and tt' functors yet to be picked - good news is that once particular t' is known we don't have much choice left!

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

Our modified lambda Term is either an abstraction or a application - a functor composition of Along (t) and Twice (tt) under Sum in disguise:

> `kyo` : ∀ a o , ∃ t tt ttt tttt . ( t `S'T'I'TT'I` tt ) a `AR____` ( ttt `S'T'I'TT'I` tttt ) a `AR__` o `AR__` ( t `S'T'I'TT'I` tt ) o

To use this monstrously looking source lax co-Kleisli operator we also need to pick (ttt) and (tttt) functors so that these transformations do exist:

> `kyo` : ∀ a o , ∃ t ttt . t a `AR____` ttt a `AR__` o `AR__` t o
> `kyo` : ∀ a o , ∃ tt tttt . tt a `AR____` tttt a `AR__` o `AR__` tt o

Good news is that Along (t) and Twice (tt) currently have only one transformation of this kind each:

> `kyo` : ∀ a o . Along i a `AR____` Along i a `AR__` o `AR__` Along i o
> `kyo` : ∀ a o . Twice a `AR____` Along ( Unit `S` Unit ) a `AR__` o `AR__` Twice o

How do these operate on values? Let's find out on elementary examples:

> Along `har_'st` X `hop` A `__kyo` Stage = Along `har___'st` Along `ha__` X `hop` A `hop_` A
> Twice `har_'st` X `hop` Y `__kyo` Stage = Twice `har___'st` Along `ha__` X `hop` This `hop__` Along `ha__` Y `hop` That

Along just copies a value attached to a parameter and Twice attaches an information about each parameter position - memorise it.

Finally, all functors have been chosen, let's create another alias for an extension of Term:

: Term ~ ( Along Latin `S'T'I'TT'I` Twice )
: Span ~ ( Along Latin `S'T'I'TT'I` Along ( Unit `S` Unit ) )

Coming back to this source lax co-Kleisli operator for Instruction from the beginning of this chapter with all unknown functors substituted:

> `kyo` : ∀ a o . Instruction Term a `AR____` Along ( List `T'I` Span Unit ) a `AR__` o `AR__` Instruction Term o

Before we switch to examples, it would be more convenient to use some new patterns, you'll get meaning of each of them shortly:

> ABS'ARG i = Clasp ( This ( Along ( These i ii ) ) )
> APP'FUN i = Clasp ( That ( Along ( These i ( This Unit ) ) )
> APP'ARG i = Clasp ( That ( Along ( These i ( That Unit ) ) )
> VAR'CTX i ii = Value ( Along ( These i ii ) )

To see how it works, let's take one of the simplest lambda expressions - identity abstraction (\x.x):

> Instruction @ Term ( ABS `har'st` X `har'st` VAR `ha` X ) `kyo` Trace = ???

Demonstrating whole AST doesn't make much sense since it left untouched except variables - let's see what happened to them:

\x.x - Regarding context of variable x, it is used in abstraction body with a parameter called x (ABS'VAR).

> VAR'CTX `har__'st` X `har__` ABS'VAR `ha` X `ryo` Enter @ List

New let's take a look at traced variables but this time in identity application ((\x.x)y):

> Instruction @ Term ( APP `har_` ABS `har'st` X `har'st` VAR `ha` X `har_'st` VAR `ha` Y ) `kyo` Trace = ???

Yep, this time we have two variables - x and y with a distinguished context:

(\x.x)y - Regarding context of variable x, it is used in application as a function (APP'FUN), in abstraction body with a parameter called x (ABS'VAR).

> VAR'CTX `har__'st` X `har__` APP'FUN `has` ABS'VAR `ha` X `ryo` Enter @ List

(\x.x)y - Regarding context of variable y, it is used in application as an argument (APP'ARG).

> VAR'CTX `har__'st` Y `har__` APP'ARG `ryo` Enter @ List

Using this type of information attached to every variable we also can say if it's either bound or free and if it's bound - how far binder is.

Yes, we are going to use De Bruijn indices.