Pie Language Overview

This guide provides a concise introduction to the Pie language for users with experience in other theorem provers such as Coq, Lean, Agda, or Idris.

What is Pie?

Pie is a small dependently-typed programming language designed for education, as described in "The Little Typer" by Daniel P. Friedman and David Thrane Christiansen. Unlike industrial-strength proof assistants, Pie focuses on clarity and simplicity while still demonstrating the core concepts of dependent types.

Key Features

• A minimalist dependently-typed programming language
• Bidirectional type checking
• Normalization by evaluation (NbE)
• Tactical theorem proving (In progress)
• S-expression syntax inspired by Lisp/Scheme

Type System

Universe Hierarchy

Pie has a single universe level, with U being the type of types:

; In Pie
U  ; The type of types

; Equivalent in other systems
Type   ; Lean
Set    ; Agda
Type 0 ; Coq
Type   ; Idris

Core Types

Dependent Function Types (Π-types)

; In Pie
(Π ((x Nat)) (Vec Atom x))  ; Type of functions from n:Nat to (Vec Atom n)
(-> Nat Nat)                ; Non-dependent function type, sugar for (Π ((x Nat)) Nat)

; Equivalent in other systems
(n : Nat) -> Vec Atom n     ; Idris, Lean
(n : Nat) → Vec Atom n      ; Agda
forall (n : nat), Vector atom n  ; Coq

Dependent Pair Types (Σ-types)

; In Pie
(Σ ((n Nat)) (Vec Atom n))  ; Type of pairs where first component is n:Nat
                            ; and second is a vector of length n
(Pair Nat Nat)              ; Non-dependent pair type, sugar for (Σ ((x Nat)) Nat)

; Equivalent in other systems
(n : Nat ** Vec Atom n)     ; Idris
Σ n : Nat, Vec Atom n       ; Lean
Σ[ n ∈ Nat ] Vec Atom n     ; Agda
{n : nat & Vector atom n}   ; Coq

Inductive Types

Pie has built-in inductive types rather than allowing user-defined ones:

• Natural numbers (Nat)
• Lists (List)
• Vectors (Vec)
• Equality type (=)
• Sum type (Either)
• Unit type (Trivial)
• Empty type (Absurd)
• Atoms (Atom)

Syntax and Term Construction

Type Annotations

(the Nat zero)                  ; Explicitly annotate zero with type Nat
(the (-> Nat Nat) (λ (n) n))    ; Explicitly annotate the identity function

Function Definition

(claim identity (-> Nat Nat))
(define identity (λ (n) n))

; Equivalent in other systems
def identity : Nat -> Nat := λ n => n   ; Lean
id : Nat -> Nat; id n = n               ; Idris
identity : Nat → Nat; identity n = n    ; Agda
Definition identity (n : nat) : nat := n ; Coq

Dependent Function

(claim vec-map 
  (Π ((A U) (B U) (n Nat))
     (-> (-> A B) (Vec A n)
         (Vec B n))))

(define vec-map
  (λ (A B n)
    (λ (f vs)
      (ind-Vec n vs
        (λ (k xs) (Vec B k))
        vecnil
        (λ (k x xs ih) (vec:: (f x) ih))))))

Pattern Matching/Eliminators

Pie uses explicit eliminators rather than pattern matching:

Natural numbers

; Simple recursion
(iter-Nat n base step)

; Dependent recursion (motive allows result type to depend on n)
(ind-Nat n motive base step)

Lists

; Simple recursion
(rec-List xs base step)

; Dependent recursion
(ind-List xs motive base step)

Vectors

; Vector induction
(ind-Vec n vs motive base step)

Equality

; Substitution principle (transport)
(replace eq motive base)

Proofs as Functions

Like other dependent type systems, proofs in Pie are represented as functions that construct inhabitants of proposition types:

(claim +-comm
  (Π ((n Nat) (m Nat))
     (= Nat (+ n m) (+ m n))))

(define +-comm
  (λ (n m)
    (ind-Nat n
      (λ (k) (= Nat (+ k m) (+ m k)))
      (same-type-lemma m)
      (λ (k ih) (trans-lemma k m ih)))))

Proof Methods

Equality Proofs

; Reflexivity
(same e)  ; Proves (= T e e)

; Symmetry 
(symm eq)  ; If eq : (= T a b), then (symm eq) : (= T b a)

; Transitivity
(trans eq1 eq2)  ; If eq1 : (= T a b) and eq2 : (= T b c), then (trans eq1 eq2) : (= T a c)

; Congruence
(cong eq f)  ; If eq : (= T a b) and f : (-> T S), then (cong eq f) : (= S (f a) (f b))

; Substitution
(replace eq mot base)  ; If eq : (= T a b), mot : (-> T U), base : (mot a), 
                      ; then (replace eq mot base) : (mot b)

Induction

Pie provides induction principles for its built-in inductive types:

; Natural number induction
(ind-Nat n motive base step)

; List induction
(ind-List xs motive base step)

; Vector induction
(ind-Vec n xs motive base step)

; Equality induction
(ind-= eq motive base)

Ex Falso Quodlibet

; Derive anything from a contradiction
(ind-Absurd absurd target-type)