Write a category-theoretic description

[colltoaction]

At its core, yaml.yaml just wants to be a functor that maps between the yaml and lambda categories.

---

With yaml we get a human friendly data serialization standard for all programming languages. More specifically I see:

• specification
• syntax
• (de)serializers
• performance
• community
• advanced editors
• online editors

On the other hand, the yaml spec is pretty dense and we don't want to deal with everything from the beginning.

---

The mapping to lambda is not just for the math, but we actually want to run software in a computer. In #2 I took a lambda calculus interpreter written in Rust and I was able to map simple documents to lambda terms.

A different approach could map between languages (transpiling). Haskell seems to be the closest but I'm not familiar with the syntax or tooling.

[colltoaction]

I'm reading de Bruijn and I think we can use it to define a functor between the YAML number scalars and Lambda calculus in de Bruijn notation categories.

[colltoaction]

Chapter 5 in de Bruijn indices
https://web.engr.oregonstate.edu/~walkiner/teaching/cs581-fa20/slides/5.LambdaCalculus.pdf

[colltoaction]

https://www.win.tue.nl/automath/archive/pdf/aut029.pdf

LAMBDA CALCULUS NOTATION WITH NAMELESS DUMMIES,
A TOOL FOR AUTOMATIC FORMULA MANIPULATION,
WITH APPLICATION TO THE CHURCH-ROSSER THEOREM
N. G. DE BRUIJN
(Comrnunicatod at tho mooting of Juno 24, 1972)
In ordinary lambda calculus the occurrences of a bound variable are made
recognizable by the use of one and the same (otherwise irrelevan+) name at all
occurrences. This convention is known to cause considerable trouble in cases of
substitution. In the present paper a different notational system is developed, where
occurrences of variables are indicated by integers giving the "distance" to the
binding L instead of a name attached to that A. The system is claimed to be efficient
for automatic formula manipulation as well as for metalingual discrission. As an
example the most essential part of a proof of the Church-Rosser theorem is presented
in this namefree calculus.

[colltoaction]

We can think of the de Bruijn notation as a lower level lambda calculus form. Closer to the machine.

This is explained in the previous paper. It could be useful to write the first bootstrapping tools as in #5.

[colltoaction]

Maybe a list is de Bruijn notation and a mapping classical notation

[colltoaction]

Different approaches for mixing named and nameless variables appear in the literature:

• https://blog.jez.io/variables-and-binding/
• https://www.cs.ru.nl/~james/RESEARCH/haskell2004.pdf

In this paper, we name free variables (ie, variables bound in the context) so that we can refer to them and rearrange them without the need to count; we give bound variables de Bruijn indices to ensure a canonical means of reference where there’s no ‘social agreement’ on a name