This is a visualization tool for simply typed λ-calculus type derivation trees. This tool performs typechecking on the entered program code, while showing you the process in a form of building a type derivation tree.
Because "LAMBDA: Leading Advancements in Molecular Biochemistry and Dimensional Astrophysics." - Black Mesa
On a serious note, the main goal of this tool is to help shed some light at the fundamentals of typechecking in functional programming, and also help out people studying it.
Enter your λ-calculus program into the input field.
Shortcuts:
\l : λ
-> : →
|- : ⊢
Then you can proceed to the type derivation tree section where you can walk trough the construction of the tree. You can export the shown tree to LaTeX from here as well.
On the bottom part of the page there are sections for any created type variables and context substitutions for the currently selected step of the derivation tree.
The input has to be written in one of the two ways:
The second option is for cases when you dont have any context, so you can ommit the '⊢'.
The context is denoted as type declarations of variables separated by a comma. The individual declarations are denoted by the variable's name, a colon, and then the type of the variable.
<context> := <variable>:<type>, <variable>:<type>, ...
Variables' names MUST start with a lowercase letter. On the other hand, types' names MUST start with an uppercase letter. Both names can include numbers as well.
There are also function types, used for denoting... you guessed it... functions. Bellow is the general way to denote them.
<type> → <type>
You can string these together like this, too:
String → Nat → Bool → String
You can use brackets to enforce priority. The default priority of the type listed above looks like this:
String → (Nat → (Bool → String))
Let's get to the last piece of the puzzle, the term. There are multiple options when it comes to terms, the most basic of which are predefined constants and variables. This tool only recognizes constants in type 'Bool' (true, false) and 'Nat' (numbers from 0 and up). If you want to use a variable in your program, then you need to include the variable in context, for the input to be considered valid.
Next term option is application of terms, which is denoted just by writing two terms next to each other. This is how you feed arguments into functions. Bellow is an example of a program consisting of the application 'fun 3'. It is also an example for a variable term - 'fun', and a constant term - '3'. You can also see there, that the variable 'fun' is denoted in the context, so it can be used in the term of the program.
fun : Nat → Bool ⊢ fun 3 : Bool
There is a group of keywords that act like functions. These are:
iszero : Nat → Bool
succ : Nat → Nat
pred : Nat → Nat
Yet another form of a term is a conditional term. These terms consist of three another terms and generally look like this:
if <term> then <term> else <term>
And last but not least there are abstractions, which are essentially what we call an anonymous function. To write one, we start with the 'λ' and then we denote a name and a type for the function argument separated by a colon. Next we type a dot, after which we start denoting the term that makes the body of our function. To create a multi-argument function we can put one abstraction into another. Important thing to note is, that the argument name you choose for your abstraction MUST NOT be included in the context of your program. Bellow is an example of a program with multi-argument abstraction.
λb:Bool.λx:Nat.if b then succ x else pred x : Bool->Nat->Nat
Abstractions and conditional terms take everything that they can reach as a part of them. This means that they normaly swallow up any subsequent applications, so writing this:
... ⊢ fun if true then pred else succ 0 : ...
... is the same as writing this:
... ⊢ fun (if true then pred else succ 0) : ...
To combat this behaviour we can encapsulate these terms in brackets together with only the parts we want them to swallow up:
... ⊢ fun (if true then pred else succ) 0 : ...
Now that you can successfully enter syntactically correct programs, we can have a look at typing rules. These are the rules that decide wheter your program has no typing errors. Here they are all listed for you:
| (BOOL) | ||
| Γ ⊢ true:Bool |
| (BOOL) | ||
| Γ ⊢ false:Bool |
| (NAT) | ||
| Γ ⊢ 0:Nat |
| (ISZERO) | ||
| Γ ⊢ iszero:Nat→Bool |
| (SUCC) | ||
| Γ ⊢ succ:Nat→Nat |
| (PRED) | ||
| Γ ⊢ pred:Nat→Nat |
| x:T ∈ Γ | (VAR) |
| Γ ⊢ x:T |
| Γ ⊢ t1:Bool | Γ ⊢ t2:T | Γ ⊢ t3:T | (IF) | ||||
| Γ ⊢ if t1 then t2 else t3:T | |||||||
| Γ, x:T0 ⊢ t1:T1 | (ABS) |
| Γ ⊢ λx:T0.t1:T0→T1 |
| Γ ⊢ t1:T0→T | Γ ⊢ t2:T0 | (APP) | ||
| Γ ⊢ t1 t2:T | ||||
And that's it, now you can go and experiment to your heart's content.
Happy typechecking!