If you run main, the REPL will start and ask you for a term in the simply typed lambda calculus. Examples: > \x:x. x Terms Types ---------------- x x \x -> x x -> x > \x:x. x x Type error