custom syntactic sugar layer over lambda calculus.
Go to file
trans_soup f389d3092d mention new special lines in README. 2023-11-11 18:39:17 +01:00
lib add `id`, `omega`, and `K` to prelude. 2023-11-11 18:37:01 +01:00
src create `prelude` "module". 2023-11-11 18:34:58 +01:00
README.md mention new special lines in README. 2023-11-11 18:39:17 +01:00
ideas.md add ideas list. 2023-11-07 03:54:38 +01:00

README.md

catgirl calculus interpreter

a collection of tools, including a REPL, for catgirl calculus; a language that's basically a layer of syntactic sugar over the untyped lambda calculus.

modules

the parser takes catgirl calculus source code and turns it into a syntax tree.

the compiler takes that tree and turns it into a Map of functions; the functions are represented in the format described here.

the transpiler takes a compiled function, and returns a javascript function (not javascript source code).

the reducer takes a single compiled function application and repeatedly performs beta-reduction for as long as it remains an application. it's currently eagerly evaluated, and uses naive recursion (no trampolining), so e.g. calling the omega combinator with itself as argument causes a stack overflow.

the REPL works like you'd expect from a REPL. it takes a line of input, executes the line, and prints the result.

the REPL uses nodejs to run in the terminal, but changing that probably wouldn't be too hard. everything else is plain js.

language overview

in brief:

catgirl calculus programs run line by line, in order.

empty lines are ignored. lines starting with # are comments and are ignored.

lines structured like this:

name = expression

are binding lines. the names are tokens. tokens have these restrictions:

  • may not contain whitespace.
  • may not contain these characters: ().
  • may not start with these characters: #!.
  • may not equal =.
  • may not be a right-arrow (defined below).

binding lines associate an expression with a name. a name that has already been bound can later be bound to something else.

a right-arrow is any of these:

->
=>
>
→

they mean the same thing and may be used interchangeably.

expressions are either tokens, functions, or applications. tokens are described above. in expressions, only tokens that have previously been bound to a name may be used.

functions are structured like this:

a b c d → expression

they must have at least one argument. they are curried.

applications are structured like this:

function argument

where both the function and the argument are expressions.

when taking a catgirl calculus program as a single function (rather than a collection of functions), the program is the function that is bound to the token main when all the lines have been executed. IO can be done by passing input to a program and using its return value as output.

example programs

church booleans and logic gates:

true = a b → a
false = a b → b

not = a → a false true
and = a b → a b false
or = a b → a true b

implementation-specific special lines

here are the commands that are specific to this REPL:

  • !.exit exits the REPL.
  • !.clear clears the console.
  • !.env prints out all the named functions.
  • !.env_raw prints out all the named functions, without any special rendering.
  • !.load prelude runs the program exported by lib/prelude.mjs.

disclaimer

the parsing might be somewhat unreliable, especially with functions being defined inside of other function definitions. if a seemingly valid line yields an error, you can try extracting sub-functions into named functions and use those instead.