PAL cheat sheet ×

Define a type system as inference rules, then ask PAL to infer types with it.

Statements

type Bool              -- declare a type
type Arrow<a, b>       -- a type with parameters
data List<a> = Nil | Cons(a, List<a>)  -- an inductive type, with RecList
expr True : Bool       -- axiom: a constant and its type
rule Not:              -- an inference rule
  x : Bool             --   premises, one per line
->
  Not(x) : Bool        --   conclusion
infer Not(True)        -- infer an expression's type
check Not(True) : Bool -- expect a type (type variables may be renamed)
fails Not(Not)         -- expect a type error

Types must be declared before use, with the right number of arguments. A definition that breaks this, or a rule whose premise uses a variable missing from its conclusion, is rejected.

Dependent types

rule Vec:                    -- a type can mention expressions
  n : Nat
  a : Type
->
  Vec(n, a) : Type
App(f, a) : u[x := a]        -- u with a for x, in a rule's type
reduce Beta: App(Lam(x, t, b), a) ~> b[x := a]
def Two := Succ(Succ(Zero))  -- a name for a term
def Double(n) := Plus(n, n)  -- with parameters

Expressions and types are the same terms: C(…) and C<…> are equal. A premise x : t |- u : … in a rule for Pi(x, t, u) makes x bound in u. Types are equal up to bound names and up to reduce.

Proof search

find Implies<a, a>     -- find a term of this type: Lam(x, x)
find Implies<a, a> 10  -- search up to 10 rules deep (default 6)

PAL searches backwards from the type through your rules, up to 6 rules deep. With types as propositions, the term is a proof.

Metatheory

value Succ(n)          -- a pattern of values
test preservation      -- reduction keeps the type
test progress 2000     -- a term that does not reduce is a value

A test generates well-typed closed terms from your rules (5000 tries if you give no number) and shows the smallest counterexample. Tests are slow, so this page runs them only when you press Run tests.

Premises

x : T                  -- x must have type T
x : A |- body : B      -- check body with x : A in scope
x : A, y : B |- e : C  -- several hypotheses
x : gen A |- body : B  -- x is polymorphic in body
x : lin A |- body : B  -- body uses x exactly once (aff: at most once)
share t : A            -- shares the variables in scope (e.g. If branches)
x => T                 -- infer the type of x
x <= T                 -- check x against T

⊢ works in place of |-. A rule with a <= conclusion, like Lam(x, b) <= Arrow<a, b>, is used only when the expected type is known.

Naming

• Uppercase: constructors and concrete types, e.g. Add(x, y), Maybe<Num>
• lowercase: variables and type variables, e.g. x, a
• Comments start with --

Errors

Type mismatch	Two different types had to be equal
Arity mismatch	A rule exists, but for a different number of arguments
Unknown expression	No rule, no expr, and not a bound variable
Infinite type	A type would contain itself (a ~ Arrow<a, b>)
No typing rule matched	A constant was given arguments
undeclared type	Declare it first with type
undeclared constructor	Declare it first with expr or a rule
Stuck substitution	In u[x := e], u is still unknown
Reduction limit	The reductions of a term do not stop
Scope error	A variable would be used outside its binder

This page

• The program is checked from the top on every edit
• The part of the program at fault is underlined; click an error to jump to it. Tab indents
• Open derivation under a result to see how PAL proved it, or copy it as LaTeX
• Copy LaTeX over the results copies all your rules as a LaTeX document
• definitions shows or hides type, expr, rule, reduce, def and value results
• Examples loads an example program. Share copies a link that opens your program

New to type systems? Read the tutorial →