Llama is a language that compiles directly to lambda calculus with almost no layer of abstraction


This code successfully compiles to:

(λmkpair.(λfirst.(λgetfirst.(λsecond.(λgetsecond.(λconcat.(λmap.(λsucc.(λpred.(λmult.(λowo.(λwew.concat (concat (map owo succ) " ") (map wew succ)) "Vgdqk ") "Gdmkn+") λm n f x.m (n f) x) λn f x.n 2 (λ_.x) λu.u) λn f x.n f (f x)) λs fn f x.s (λnm nx.f (fn nm) nx) x) λa b f x.a f (b f x)) λp.p second) 0) λp.p first) 0) λa b f.a b

And without literals:

(λmkpair.(λfirst.(λgetfirst.(λsecond.(λgetsecond.(λconcat.(λmap.(λsucc.(λpred.(λmult.(λowo.(λwew.concat (concat (map owo succ) (λf x.f (λf x.f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))))))))))))))))))))))) x)) (map wew succ)) λf x.f (λf x.f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (f (λf x.f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (f (λf x.f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (f (λf x.f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (f (λf x.f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (f (λf x.f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))))))))))))))))))))))) x)))))) λf x.f (λf x.f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (f (λf x.f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (f (λf x.f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (f (λf x.f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (f (λf x.f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (f (λf x.f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))))))))))))))))))))))))))))))))) x)))))) λm n f x.m (n f) x) λn f x.n (λg h.h (g f)) (λ_.x) λu.u) λn f x.n f (f x)) λs fn f x.s (λnm nx.f (fn nm) nx) x) λa b f x.a f (b f x)) λp.p second) λa b.b) λp.p first) λa b.a) λa b f.a b

Which reduces to "Henlo, Whirl"
Online compiler and solver soon(tm)


Variable names follow the regex [A-Za-z_][A-Za-z0-9_]*


Expressions are one of anything below, Long expressions (the body of a llama for example) consume multiple expressions until they hit the EOF or some token like )


Llamas work the same as lambdas in lambda calculus

λx.λy.λz.x looks like \x\y\z x in llama
syntax: \name lexpr


Applications work the same as usual, two expressions grouped together is an application

It is always left associative meaning a b c d = ((a b) c) d

syntax: expr expr


Variables are bound to the closest llama that matches their name, otherwise they are free and applications to it cannot be solved.

Binding should work exactly like it would in a high level programming language like Dart, where variables are bound based on where they were the application took place, not where it was subsituted into.

syntax: name


Parentheses allow you to group expressions together to explicitly control application order

example: a (b c)

syntax: (lexpr)


Comments start with // and continue until the end of line


~\flutter 1 // The one


The squiggly character is like parentheses that dont need to be closed

example: \f\x f(f(f(f x))) = \f\x f~f~f~f x

syntax: ~lexpr


This is the first major difference to lambda calculus, you can procedurally define variables to be used in code preceding it

Only valid inside of a long expression

example:~\a 1 ~\b (succ a) ~\b (succ b) b = 3 (succ not included by default)

syntax: ~\name expr lexpr

The way this works is it puts the lexpr as a body of a llama and applies your expr to it

~\a 1
~\b (succ a)
succ b  

turns into

        succ b
    ) succ a
) 1


Vectors can be created using square brackets

example: [1 2 3] = \f\x f 1~f 2~f 3 x

syntax: [expr...]


Numbers use basic church encoding so 1 means \f\x f x and 3 means \f\x f~f~f x


123 // decimal  
0x7B // hex  
0b1111011 // binary  
0o173 // octal  
'{' // character  


String literals are equivalent to a vector of char codes

Both character literals and strings support the common escapes \a \b \f \n \r \t \v \\ \" and also number escapes \123 \x7b \b1111011

example: "foo" = ['f' 'o' 'o']

Llama include

Used to include a whole file as a llama, the file must have a main body

syntax: ~"filename"


succ 1  
succ \"foo.lm" // result is 3  

Definition include

Unlike llama includes, definition includes import definitions and the file cannot have a main body

syntax: ~\"filename"


    \f\x a f ~b f x
concat "foo" "bar" // result is "foobar"