The Pie Reference

After installing Pie from the Racket package database, open DrRacket. Change the first line to read #lang pie, and then start typing. If DrRacket’s "Background Expansion" feature is enabled, the type checker will run every time the file is modified, whether or not it is run. Otherwise, invoke the type checker using the "Run" button. It may be convenient to enable the option in DrRacket to show gold highlighting on errors, because it causes type errors to be highlighted while typing.

Alternatively, it is also possible to use any editor to create a Pie program, and then save it to a file. Run the file with the command-line version of Racket to test it.

The Todo List for DrRacket is supported by Pie. Each TODO in the program is listed.

2 General-Purpose Expressions

type annotation
(the type expr)

Asserts that expr is a type. This can be necessary when there is insufficient information for Pie to discover an expression’s type.

Examples:

> nil
Can't determine a type
> (the (List Nat)
    nil)
(the (List Nat)
  nil)
> (cons 2 (same 2))
Can't determine a type
> (the (Σ ((n Nat))
         (= Nat n n))
    (cons 2 (same 2)))
(the (Σ ((n Nat))
      (= Nat n n))
  (cons 2
    (same 2)))
> (the (Σ ((n Nat))
         (= Nat n 2))
    (cons 2 (same 2)))
(the (Σ ((n Nat))
      (= Nat n 2))
  (cons 2
    (same 2)))

incomplete expression
TODO

TODO represents a part of a program that is not yet written, corresponding to the empty boxes in The Little Typer. Users may optionally leave a note or other expression behind as a reminder.

3 Types, Constructors, and Eliminators

3.1 Absurd

type constructor
Absurd

Absurd is a type with no values.

eliminator
(ind-Absurd target motive) → motive
target : Absurd
motive : U

Given an Absurd expression, ind-Absurd can have any type at all.

Example:

> (the (→ Absurd
         Nat)
    (λ (nope)
      (ind-Absurd nope Nat)))
(the (→ Absurd
       Nat)
  (λ (nope)
    (ind-Absurd (the Absurd nope)
       Nat)))

3.2 Trivial

type constructor
Trivial

Trivial is a type with exactly one value.

constructor
sole : Trivial

sole is the only Trivial value, and every Trivial expression is the same Trivial as sole.

Examples:

> sole
(the Trivial sole)
> (check-same (→ Trivial
                Trivial)
    (λ (x)
      sole)
    (λ (y)
      y))

3.3 Atoms

type constructor
Atom

Atoms are like Lisp symbols.

constructor
(quote atom) → Atom
atom : identifier

Each atom is a constructor. quote is always written with a single tick mark.

Examples:

> 'grønkål
(the Atom 'grønkål)
> 'agurk
(the Atom 'agurk)

3.4 Natural Numbers

type constructor
Nat

The natural numbers, called Nat, are all the numbers greater than or equal to zero.

constructor
zero : Nat

zero is the smallest Nat.

constructor
(add1 n) → Nat
n : Nat

add1 makes a Nat one larger.

eliminator
(which-Nat target base step) → X
  target : Nat
  base : X
  step : (-> Nat X)

which-Nat is a case operator on Nat.

Examples:

> (which-Nat 0 0 (λ (smaller) smaller))
(the Nat 0)
> (which-Nat 17 0 (λ (smaller) smaller))
(the Nat 16)

eliminator
(iter-Nat target base step) → X
  target : Nat
  base : X
  step : (-> X X)

iter-Nat applies step to base target times.

Example:

> (iter-Nat 5
    0
    (λ (x)
      (add1 (add1 x))))
(the Nat 10)

eliminator
(rec-Nat target base step) → X
  target : Nat
  base : X
  step : (-> Nat X X)

rec-Nat is primitive recursion on Nat. If target is zero, then the whole expression is base. If target is (add1 n), then the whole expression is (step n (rec-Nat n base step)).

eliminator
(ind-Nat target motive base step) → (motive target)
  target : Nat
  motive : (-> Nat U)
  base : (motive zero)
   step :
(Π ((n Nat))
  (-> (motive n)
    (motive (add1 n))))

ind-Nat is induction on Nat. motive is an (→ Nat U), and the whole expression’s type is (motive target). ind-Nat computes identically to rec-Nat; the type is, however, more expressive.

3.5 Pairs

type constructor
(Σ ((x A1) (y A2) ...) D)

The values of (Σ ((x A)) D) are (cons a d), where a is an A and the type of d is found by consistently replacing x with a in D.

(Σ ((x A1) (y A2) ...) D) is an abbreviation for the nested Σ-expressions

(Σ ((x A1))
  (Σ ((y A2))
    ...
    D))

type constructor
(Sigma ((x A1) (y A2) ...) D)

Sigma is an alias for Σ

type constructor
(Pair A D)

A shorter way of writing (Σ ((x A)) D) when x is not used.

constructor
(cons a d) → (Σ ((x A)) D)
a : A
d : D^

cons is the constructor for Σ. D^ is the result of consistently replacing each x in D with a.

eliminator
(car p) → A
p : (Σ ((x A)) D)

The first projection of a pair. If p is a (Σ ((x A)) D), then (car p) is an A. Furthermore, (car (cons a d)) is a.

eliminator
(cdr p) → D
p : (Σ ((x A)) D)

The second projection of a pair. If p is a (Σ ((x A)) D), then (cdr p) is a D where each x has been replaced by (car p). Furthermore, (cdr (cons a d)) is d.

3.6 Functions

type constructor
(Π ((x X1) (y X2) ...) B)

Function types are written with Π. All functions take exactly one argument, and what appears to be a multiple-argument function or function type is actually a Curried function. In other words, (Π ((x X1) (y X2) ...) B) is an abbreviation for

(Π ((x X1))
  (Π ((y X2))
    ...
    B))

The type of a function application is found by substituting the actual argument for the argument name in the return type.

Examples:

> ((the (Π ((n Nat))
          (= Nat n n))
     (λ (n)
       (same n)))
   5)
(the (= Nat 5 5)
  (same 5))
> ((the (Π ((n Nat))
          (= Nat n n))
     (λ (n)
       (same n)))
   15)
(the (= Nat 15 15)
  (same 15))

type constructor
(Pi ((x X1) (y X2) ...) B)

Pi is an alias for Π.

type constructor
(∏ ((x X1) (y X2) ...) B)

∏ is an alias for Π that is easier to type on some keyboards.

type constructor
(→ X1 X2 ... B)

→, pronounced "arrow", is shorter way of writing (Π ((x X1) (x X2) ...) B) when the identifiers x ... are not used.

type constructor
(-> X1 X2 ... B)

-> is an alias for →.

constructor
(λ (x1 x2 ...) b)

Functions are constructed with λ. (λ (x1 x2 ...) b) is a (Π ((x1 X1) (x2 X2) ...) B) if when x1 is a X1, x2 is a X2, ..., then b is a B.

What may appear to be multiple-argument functions are actually nested one-argument functions.

Examples:

> (the (→ Atom Atom
         Atom)
     (λ (food beverage)
       food))
(the (→ Atom Atom
       Atom)
  (λ (food beverage)
    food))
> (the (→ Atom
         (→ Atom
           Atom))
     (λ (food)
       (λ (beverage)
         food)))
(the (→ Atom Atom
       Atom)
  (λ (food beverage)
    food))
> (check-same (→ Atom Atom
                Atom)
    (λ (food)
      (λ (beverage)
        beverage))
    (λ (food beverage)
      beverage))

constructor
(lambda (x1 x2 ...) b)

lambda is an alias for λ.

3.7 Lists

type constructor
(List E)

(List E) is the type of lists in which all entries are Es.

constructor
nil : (List E)

Examples:

> (the (List Atom) nil)
(the (List Atom)
  nil)
> nil
Can't determine a type
> (the (List (→ Nat
               Nat))
    nil)
(the (List (→ Nat
             Nat))
  nil)

constructor
(:: e es) → (List E)
e : E
es : (List E)

Examples:

> (:: 0 (:: 1 (:: 2 nil)))
(the (List Nat)
  (:: 0
    (:: 1
      (:: 2 nil))))
> (:: 0 (:: 'one (:: 2 nil)))
Expected
  (List Atom)
but given
  (List Nat)

eliminator
(rec-List target base step) → X
  target : (List E)
  base : X
  step : (-> E (List E) X X)

rec-List is primitive recursion on lists. If target is nil, the result is base. If target is (:: e es), then the result is (step e es (rec-List es base step)).

Examples:

> (rec-List (the (List Atom) nil)
    zero
    (λ (e es len-1)
      (add1 len-1)))
(the Nat 0)
> (rec-List (:: 'rødbeder
              (:: 'gulerødder
                (:: 'kartofler nil)))
    zero
    (λ (e es len-1)
      (add1 len-1)))
(the Nat 3)

eliminator
(ind-List target motive base step) → (motive target)
  target : (List E)
  motive : (-> (List E) U)
  base : (motive nil)
   step :
(Π ((e E)
    (es (List E)))
  (-> (motive es)
    (motive (:: e es))))

ind-List is induction on lists. When target is a (List E), t the whole expression’s type is (motive target), the type of base is (motive nil), and the type of step is

(Π ((e E)
    (es (List E)))
  (→ (motive es)
    (motive (:: e es))))

. ind-List computes just like rec-List.

Examples:

> (ind-List (:: 'ananas
              (:: 'granatæble
                nil))
    (λ (es)
      Nat)
    zero
    (λ (e es len)
      (add1 len)))
(the Nat 2)
> (ind-List (:: 'ananas
              (:: 'granatæble
                nil))
    (λ (es)
      (= (List Atom) es es))
    (same nil)
    (λ (e es es=es)
      (cong es=es
        (the (→ (List Atom)
               (List Atom))
          (λ (xs)
            (:: e xs))))))
(the (= (List Atom)
       (:: 'ananas
         (:: 'granatæble nil))
       (:: 'ananas
         (:: 'granatæble nil)))
  (same (:: 'ananas
          (:: 'granatæble nil))))

3.8 Vectors

type constructor
(Vec E len)

A (Vec E len) is a list that contains precisely len entries, each of which is an E.

constructor
vecnil : (Vec E zero)

vecnil is an empty Vec.

Examples:

> (the (Vec Nat zero) vecnil)
(the (Vec Nat 0)
  vecnil)
> (the (Vec Atom zero) vecnil)
(the (Vec Atom 0)
  vecnil)
> (the (Vec Atom 4) vecnil)
vecnil requires that the length be zero, not
  4
> vecnil
Can't determine a type

constructor
(vec:: e es) → (Vec E (add1 k))
e : E
es : (Vec E k)

Examples:

> (the (Vec Nat 2) (vec:: 17 (vec:: 6 vecnil)))
(the (Vec Nat 2)
  (vec:: 17
    (vec:: 6 vecnil)))
> (the (Vec Nat 3) (vec:: 17 (vec:: 6 vecnil)))
vecnil requires that the length be zero, not
  1
> (vec:: 17 (vec:: 6 vecnil))
Can't determine a type

eliminator
(head es) → E
es : (Vec E (add1 k))

head finds the first entry in a non-empty Vec.

Examples:

> (head (the (Vec Atom 1) (vec:: 'æbler vecnil)))
(the Atom 'æbler)
> (head (the (Vec Atom 0) vecnil))
Expected a Vec with add1 at the top of the length, got zero

eliminator
(tail es) → (Vec E k)
es : (Vec E (add1 k))

tail finds the all but the first entry in a non-empty Vec.

Examples:

> (tail (the (Vec Atom 2) (vec:: 'pærer (vec:: 'æbler vecnil))))
(the (Vec Atom 1)
(vec:: 'æbler vecnil))
> (tail (the (Vec Atom 0) vecnil))
Expected a Vec with add1 at the top of the length, got zero

eliminator
(ind-Vec target-1 target-2 motive base step)
→ (motive target-1 target-2)
  target-1 : Nat
  target-2 : (Vec E target-1)
   motive :
(Π ((k Nat))
  (→ (Vec E k)
    U))
  base : (motive zero vecnil)
   step :
(Π ((k Nat)
    (e E)
    (es (Vec E k)))
  (→ (motive k es)
    (motive (add1 k) (vec:: e es))))

Induction on vectors is used to prove things about any vector. target-1 is the length, and target-2 is the vector itself. The motive is a

(Π ((k Nat))
(→ (Vec E k)
U))

The base is a (motive zero vecnil), and the step is a

(Π ((k Nat)
    (e E)
    (es (Vec E k)))
  (→ (motive k es)
    (motive (add1 k) (vec:: e es))))

3.9 Either

type constructor
(Either L R)

Either represents that there are two possibilities: either an L with left on top, or an R with right on top.

constructor
(left l) → (Either L R)
l : L

Examples:

> (the (Either Nat Atom) (left 3))
(the (Either Nat Atom)
(left 3))
> (the (Either Nat Atom) (left 'rosenkål))
Expected Nat but given Atom

constructor
(right r) → (Either L R)
r : R

Examples:

> (the (Either Nat Atom) (right 'blomkål))
(the (Either Nat Atom)
(right 'blomkål))
> (the (Either Nat Atom) (right 8))
Expected Atom but given Nat

eliminator
(ind-Either target motive on-left on-right) → (motive target)
  target : (Either X Y)
  motive : (→ (Either X Y) U)
   on-left :
(Π ((l L))
  (motive (left l)))
   on-right :
(Π ((r R))
  (motive (right r)))

Induction on Either consists of showing how to fulfill the motive for both constructors.

Examples:

> (ind-Either (the (Either Nat Atom) (left 5))
     (λ (e)
       Nat)
     (λ (n)
       n)
     (λ (a)
       17))
(the Nat 5)
> (ind-Either (the (Either Nat Atom) (right 'peberfrugt))
     (λ (e)
       Nat)
     (λ (n)
       n)
     (λ (a)
       17))
(the Nat 17)

3.10 Equality

type constructor
(= X from to)

The equality type’s values are evidence that from and to are equal.

constructor
(same e) → (= X e e)
e : X

If e is an X, then (same e) is an (= X e e), because e is the same X as e.

Example:

> (the (= Nat 2 2) (same 2))
(the (= Nat 2 2)
(same 2))

eliminator
(replace target motive base) → (motive to)
  target : (= X from to)
  motive : (→ X U)
  base : (motive from)

If target is an (= X from to), motive is an

(→ X
U)

and base is a (motive from), then (replace target motive base) is a (motive to).

eliminator
(symm target) → (= A to from)
target : (= A from to)

If target is an (= A from to), then (symm target) is an (= A to from).

Example:

> (the (Π ((x Nat)
           (y Nat))
         (→ (= Nat x y)
           (= Nat y x)))
    (λ (x y p)
      (symm p)))
(the (Π ((x Nat)
         (y Nat))
      (→ (= Nat x y)
        (= Nat y x)))
  (λ (x y p)
    (symm p)))

eliminator
(trans target-1 target-2) → (= X from to)
target-1 : (= X from middle)
target-2 : (= X middle to)

trans is used to "glue together" evidence of equality. If target-1 is an (= X from middle) and target-2 is an (= X middle to), then (trans target-1 target-2) is an (= X from to).

eliminator
(cong target fun) → (= Y (fun from) (fun to))
target : (= X from to)
fun : (→ X Y)

cong shows that all functions respect equality. In particular, if target is an (= X from to) and fun is an

(→ X
Y)

then (cong target fun) is an

(= Y (fun from) (fun to))

eliminator
(ind-= target motive base) → (motive to target)
  target : (= A from to)
   motive :
(Π ((x A))
  (-> (= A from x)
    U))
  base : (motive from (same from))

The induction principle on equality evidence takes a target which is an (= A from to), a motive which is a

(Π ((x A))
(-> (= A from x)
U))

and a base which is a (motive from (same from)). The entire expression is then a (motive to target).

3.11 Universe

type constructor
U

The universe describes all types except itself and those types that could contain U.

Examples:

> (the U Nat)
(the U Nat)
> (the U U)
U is a type, but it does not have a type.
> (the U (List Atom))
(the U
(List Atom))
> (the U (List U))
U is a type, but it does not have a type.

4 Declarations

In addition to expressions, Pie has three syntactic forms that are only valid at the top level of a program.

4.1 Definitions

declaration
(claim x type)

Before using define to associate a name with an expression, it is first necessary to associate the expression’s type with the name using claim.

declaration
(define x expr)

Associate the expression expr with the name x, after having already claimed its type.

4.2 Testing Pie programs

declaration
(check-same type expr1 expr2)

Check that expr1 is the same type as expr2, and fail if not.

Examples:

> (check-same Nat 4 4)
> (check-same Atom 'kirsebær 'kirsebær)
> (check-same Atom 4 'four)
Expected Atom but given Nat
> (check-same Atom 'kirsebær 'hindbær)
The expressions
'kirsebær
and
'hindbær
are not the same Atom

Because of the η-rules for Π and Absurd, every proof of a negation is the same as every other proof. This is useful when testing programs that produce proofs.

Example:

> (check-same (→ (→ (= Nat 2 3)
                   Absurd)
                 (→ (= Nat 2 3)
                   Absurd)
                (→ (= Nat 2 3)
                  Absurd))
    (λ (f g)
      f)
    (λ (f g)
      g))

top ← prev up next →

1	Using Pie in Dr Racket
2	General-Purpose Expressions
3	Types, Constructors, and Eliminators
4	Declarations