$ stack build
$ stack run untyped
$ stack run simply
$ stack run systemF
- write
λ
as\
- write
Λ
as/
- Simple Types:
Nat
andBool
- System F Types:
Nat
andBool
- write normal numbers like
23
- write Booleans like
True
andFalse
- write System F type parameters as upper case letters
(Λ T . (λ i : T . i))
- write System F type arguments as
[Nat]
- you can omit redundant parentheses both in expressions and in type annotations
:step
for the next step of the evaluation:type
for type annotation of the current expression:isnormal
for checking if the expression is in the normal form:applyto
for adding an argument to the current expression:normalize
for the evaluation until the normal form is reached:reset
for inputting different expression:bye
for exiting the program
[enter λ expression]
:$ a b c (d e f g) h i
Following example starts with submitting the (\ f : Bool -> Bool -> Bool . (\ b : Bool . f b b))
expression.
It is then applied to (\ t : Bool . (\ f : Bool . t))
.
The resulting application
is then applied to the True
.
Each change results in printing the current expression together with it's type.
At the end we just normalize the whole term and check the result.
[enter λ-> expression]
λ-> >> (\ f : Bool -> Bool -> Bool . (\ b : Bool . f b b))
(λ f : Bool -> Bool -> Bool . (λ b : Bool . f b b)) :: (Bool -> Bool -> Bool) -> Bool -> Bool
[enter command or λ-> expression]
λ-> >> :applyto
λ-> >> (\ t : Bool . (\ f : Bool . t))
(λ f : Bool -> Bool -> Bool . (λ b : Bool . f b b)) (λ t : Bool . (λ f : Bool . t)) :: Bool -> Bool
[enter command or λ-> expression]
λ-> >> :applyto
λ-> >> True
(λ f : Bool -> Bool -> Bool . (λ b : Bool . f b b)) (λ t : Bool . (λ f : Bool . t)) True :: Bool
[enter command or λ-> expression]
λ-> >> :normalize
True :: Bool
On the other hand following example just shows step by step evaluation of the well typed term.
[enter λ-> expression]
λ-> >> (\ a : Bool -> Nat . (\ b : Bool . a b)) (\ e : Bool . 23) True
(λ a : Bool -> Nat . (λ b : Bool . a b)) (λ e : Bool . 23) True :: Nat
[enter command or λ-> expression]
λ-> >> :step
(λ b : Bool . (λ e : Bool . 23) b) True
(λ b : Bool . (λ e : Bool . 23) b) True :: Nat
[enter command or λ-> expression]
λ-> >> :step
(λ e : Bool . 23) True
(λ e : Bool . 23) True :: Nat
[enter command or λ-> expression]
λ-> >> :step
23
23 :: Nat
[enter λ2 expression]
λ2 >> (\ a : forall A . A -> A -> A . a) (/ B . (\t : B . (\f : B . t)))
(λ a : (forall A . A -> A -> A) . a) (Λ B . (λ t : B . (λ f : B . t))) :: (forall A . A -> A -> A)
[enter λ2 expression]
λ2 >> (\ a : forall A . A -> A -> A . a) (/ B . (\t : B . (\f : B . t))) [Nat]
(λ a : (forall A . A -> A -> A) . a) (Λ B . (λ t : B . (λ f : B . t))) [Nat] :: Nat -> Nat -> Nat
[enter command or λ2 expression]
λ2 >> :step
(Λ B . (λ t : B . (λ f : B . t))) [Nat]
(Λ B . (λ t : B . (λ f : B . t))) [Nat] :: Nat -> Nat -> Nat
[enter command or λ2 expression]
λ2 >> :step
(λ t : Nat . (λ f : Nat . t))
(λ t : Nat . (λ f : Nat . t)) :: Nat -> Nat -> Nat
[enter command or λ2 expression]
λ2 >> :applyto
λ2 >> 23
(λ t : Nat . (λ f : Nat . t)) 23 :: Nat -> Nat
[enter command or λ2 expression]
λ2 >> :step
(λ f : Nat . 23)
(λ f : Nat . 23) :: Nat -> Nat
[enter command or λ2 expression]
λ2 >> :applyto
λ2 >> 42
(λ f : Nat . 23) 42 :: Nat
[enter command or λ2 expression]
λ2 >> :step
23
23 :: Nat
More coming (hopefully) soon.