Murat Kasimov

More about me

Я language (β)

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

Full source codePrevious chapterNext chapter

In previous chapter we defined lambda term using this Sum functor composition where each functor encodes type of term - Along is for abstraction, Twice is for application, Flout is for variable:

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

Let's look at each of these functors' supertypes to check out their contents:

: Supertype ( Along `T'I` i `T'I` parameter ) ~ ( parameter `P` i ) : Supertype ( Twice `T'I` parameter ) ~ ( parameter `P` parameter ) : Supertype ( Flout `T'I` i `T'I` parameter ) ~ ( i )

If we feed functor to a fixpoint combinator its parameters become subexpressions but Flout doesn't have any - this is where we have a stopping point i.e. it serves as a leaf in our improvised Abstract Syntax Tree.

So that if we exclude Flout from this term we are stuck with infinetely coinductively defined expression:

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

Some primitives give us ability to control unrestricted recursion, Instruction is one of them:

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

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

> ... = Impel `har_` Abstraction `har'st` X `har'st` Value `ha` X

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

> ... = Impel `har___` Application `har__` Impel `har_` Abstraction `har'st` X `har'st` Value `ha` X `har__'st` Value `ha` Y

As previously, we can come up with more specialised patterns:

> ABS i ii = Impel ( Abstraction i ii ) > APP i ii = Impel ( Application i ii ) > VAR i = Value i

... so that these code snippets look completely identical!

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

However despite the superficial similarity, there is one big improvement - our AST is a functor now!

> Instruction ( ABS `har'st` X `har'st` VAR `ha` X ) `yo` Upper = Instruction ( ABS `har'st` X `har'st` VAR `ha` Upper `ha` X ) > Instruction ( ABS `har'st` X `har'st` VAR `ha` X ) `yo` Lower = Instruction ( ABS `har'st` X `har'st` VAR `ha` Lower `ha` X ) > Instruction ( ABS `har'st` X `har'st` VAR `ha` X ) `yo` Exist = Instruction ( ABS `har'st` X `har'st` VAR `ha` Exist `ha` X ) > Instruction ( ABS `har'st` X `har'st` VAR `ha` X ) `yo` Same `ho'ut'st` None = Instruction ( ABS `har'st` X `har'st` VAR `ha` None ) > Instruction ( ABS `har'st` X `har'st` VAR `ha` X ) `yo` Same `ho'ut'st` Y = Instruction ( ABS `har'st` X `har'st` VAR `ha` Y )

As you can see whenever we map we only affect variables without touching actual expression - that's the purpose of being a functor.

Pretty often when we buld new functors from more primitive ones - assosiated natural transformations come for free. Let's traverse our AST!

> Instruction @ Term `har__` ABS `har'st` X `har'st` VAR `ha` X >> `yokl_` Forth `ha` Await `ha` output `ha` Glyph `ha` Letter `ha` Upper > Instruction @ Term `har__` APP `har_` ABS `har'st` X `har'st` VAR `ha` X `har_'st` VAR `ha` Y >> `yokl_` Forth `ha` Await `ha` output `ha` Glyph `ha` Letter `ha` Upper

Challenge: what is going to be printed to a console output if you run it? Run executables to check the answers.