Skip to content

Instantly share code, notes, and snippets.

@davazp
Last active February 17, 2019 12:28
Show Gist options
  • Save davazp/35638cc8f8ef9cabf8653f9e9729274f to your computer and use it in GitHub Desktop.
Save davazp/35638cc8f8ef9cabf8653f9e9729274f to your computer and use it in GitHub Desktop.
The Little Typer
;; -*- scheme-*-
#lang pie
;;
;; Boolean
;;
(claim Boolean U)
(define Boolean Atom)
;;
;; Arithmetic
;;
(claim step-+ (-> Nat Nat))
(define step-+
(λ (n) (add1 n)))
(claim + (-> Nat Nat Nat))
(define +
(λ (x y)
(iter-Nat x
y
step-+)))
(claim make-step-* (-> Nat Nat Nat))
(define make-step-*
(λ (x y) (+ x y)))
(claim * (-> Nat Nat Nat))
(define *
(λ (x y)
(iter-Nat x
0
(make-step-* y))))
(claim zerop (-> Nat Boolean))
(define zerop
(λ (n)
(which-Nat n
't
(λ (n-1) 'nil))))
;;
;; Pair accessor
;;
(claim elim-Pair
(Π ((A U)
(D U)
(R U))
(-> (Pair A D)
(-> A D R)
R)))
(define elim-Pair
(λ (A D R)
(λ (p f)
(f (car p) (cdr p)))))
(claim kar
(Π ((A U)
(D U))
(-> (Pair A D) A)))
(define kar
(λ (A D)
(λ (p)
(elim-Pair A D A p (λ (x y) x)))))
;;
;; PI Type
;;
(claim flip
(Π ((A U)
(D U))
(-> (Pair A D)
(Pair D A))))
(define flip
(λ (A D)
(λ (p)
(cons (cdr p) (car p)))))
(claim id
(Π ((A U))
(-> A A)))
(define id
(λ (_u x)
x))
;;
;; Lists
;;
(claim l (List Nat))
(define l (:: 1 (:: 2 (:: 3 nil))))
(claim length
(Π ((A U))
(-> (List A) Nat)))
(define length
(λ (A)
(λ (l)
(rec-List l
0
(λ (x ll n)
(add1 n))))))
(claim append-step
(Π ((A U))
(-> A (List A) (List A) (List A))))
(define append-step
(λ (A)
(λ (x _xs acc)
(:: x acc))))
(claim append
(Π ((A U))
(-> (List A) (List A) (List A))))
(define append
(λ (A)
(λ (lst1 lst2)
(rec-List lst1
lst2
(append-step A)))))
(claim snoc
(Π ((A U))
(-> (List A) A (List A))))
(define snoc
(λ (A)
(λ (xs x)
(rec-List xs
(:: x nil)
(append-step A)))))
;; I struggled to get the ordering of the list right,
;; but it turned out to be a mistake in the book
;; http://thelittletyper.com/errata.html
(claim concat-step
(Π ((A U))
(-> A (List A) (List A) (List A))))
(define concat-step
(λ (A)
(λ (x xs acc)
(snoc A acc x))))
(claim concat
(Π ((A U))
(-> (List A) (List A) (List A))))
(define concat
(λ (A)
(λ (l1 l2)
(rec-List l2
l1
(concat-step A)))))
(claim reverse-step
(Π ((A U))
(-> A (List A) (List A) (List A))))
(define reverse-step
(λ (A)
(λ (x xs acc)
(snoc A acc x))))
(claim reverse
(Π ((A U))
(-> (List A) (List A))))
(define reverse
(λ (A)
(λ (list)
(rec-List list
(the (List A) nil)
(reverse-step A)))))
;;
;; Danish recipes
;;
(claim rugbrød
(List Atom))
(define rugbrød
(:: 'rye-flour
(:: 'rye-kernels
(:: 'water
(:: 'sourdough
(:: 'salt nil))))))
(claim toppings
(List Atom))
(define toppings
(:: 'potato
(:: 'butter nil)))
(claim condiments
(List Atom))
(define condiments
(:: 'chives
(:: 'mayonnaise nil)))
(claim kartoffelmad
(List Atom))
(define kartoffelmad
(append Atom
(append Atom toppings condiments)
(reverse Atom (:: 'plate
(:: 'rye-bread nil)))))
;;
;; Vectors
;;
(claim v (Vec Nat 3))
(define v
(vec:: 1
(vec:: 2
(vec:: 3 vecnil))))
(claim first
(Π ((A U)
(l Nat))
(-> (Vec A (add1 l)) A)))
(define first
(λ (A l)
(λ (v)
(head v))))
(claim rest
(Π ((A U)
(l Nat))
(-> (Vec A (add1 l)) (Vec A l))))
(define rest
(λ (A l)
(λ (v) (tail v))))
;;
;; Induction
;;
(claim peas-mot
(-> Nat U))
(define peas-mot
(λ (k) (Vec Atom k)))
(claim peas-step
(Π ((k-1 Nat))
(-> (peas-mot k-1)
(peas-mot (add1 k-1)))))
(define peas-step
(λ (k-1 acc)
(vec:: 'pea acc)))
(claim peas
(Π ((k Nat))
(Vec Atom k)))
(define peas
(λ (k)
(ind-Nat k
peas-mot
vecnil
peas-step)))
;; last
(claim last-mot
(-> U Nat U))
(define last-mot
(λ (A k)
(-> (Vec A (add1 k))
A)))
(claim last-base
(Π ((A U))
(last-mot A 0)))
(define last-base
(λ (A)
(first A 0)))
(claim last-step
(Π ((A U)
(k Nat))
(-> (last-mot A k) (last-mot A (add1 k)))))
(define last-step
(λ (A k-1 almost)
(λ (v)
(almost (rest A (add1 k-1) v)))))
(claim last
(Π ((A U)
(k Nat))
(-> (Vec A (add1 k)) A)))
(define last
(λ (A k)
(ind-Nat k
(last-mot A)
(last-base A)
(last-step A))))
;; drop-last
(claim drop-last-mot
(Π ((A U))
(-> Nat U)))
(define drop-last-mot
(λ (A k)
(-> (Vec A (add1 k)) (Vec A k))))
(claim drop-last-base
(Π ((A U))
(drop-last-mot A zero)))
(define drop-last-base
(λ (_A)
(λ (v) vecnil)))
(claim drop-last-step
(Π ((A U)
(k Nat))
(-> (drop-last-mot A k)
(drop-last-mot A (add1 k)))))
(define drop-last-step
(λ (A k acc)
(λ (v)
(vec:: (first A (add1 k) v)
(acc (rest A (add1 k) v))))))
(claim drop-last
(Π ((A U)
(k Nat))
(-> (Vec A (add1 k)) (Vec A k))))
(define drop-last
(λ (A k)
(ind-Nat k
(drop-last-mot A)
(drop-last-base A)
(drop-last-step A))))
;;
;; Equality & proofs
;;
(claim add1=1+
(Π ((n Nat))
(= Nat (add1 n) (+ 1 n))))
(define add1=1+
(λ (n)
(same (add1 n))))
(claim incr
(-> Nat Nat))
(define incr
(λ (n)
(iter-Nat n
1
(+ 1))))
;; add1 = inc
(claim add1=incr-mot
(-> Nat U))
(define add1=incr-mot
(λ (n)
(= Nat (incr n) (add1 n))))
(claim add1=incr-base
(= Nat (incr 0) (add1 0)))
(define add1=incr-base
(same 1))
(claim add1=incr-step
(Π ((k-1 Nat))
(-> (= Nat (incr k-1) (add1 k-1))
(= Nat (add1 (incr k-1)) (add1 (add1 k-1))))))
(define add1=incr-step
(λ (k-1)
(λ (eq)
(cong eq (+ 1)))))
(claim add1=incr
(Π ((n Nat))
(= Nat (incr n) (add1 n))))
(define add1=incr
(λ (n)
(ind-Nat n
add1=incr-mot
add1=incr-base
add1=incr-step)))
;;
;; double === twice
;;
(claim double (-> Nat Nat))
(define double
(λ (n)
(iter-Nat n
0
(+ 2))))
(claim twice (-> Nat Nat))
(define twice
(λ (n) (+ n n)))
(claim add1+=+add1
(Π ((n Nat)
(m Nat))
(= Nat
(add1 (+ n m))
(+ n (add1 m)))))
(define add1+=+add1
(λ (n m)
(ind-Nat n
(λ (i)
(= Nat
(add1 (+ i m))
(+ i (add1 m))))
(same (add1 m))
(λ (k eq) (cong eq (+ 1))))))
(claim twice=double-mot
(-> Nat U))
(define twice=double-mot
(λ (n)
(= Nat (twice n) (double n))))
(claim twice=double-base
(= Nat (twice 0) (double 0)))
(define twice=double-base
(same 0))
(claim twice=double-step
(Π ((n Nat))
(-> (= Nat (twice n) (double n))
(= Nat (twice (add1 n)) (double (add1 n))))))
(define twice=double-step
(λ (n-1)
(λ (eq)
(replace (add1+=+add1 n-1 n-1)
(λ (k)
(= Nat
(add1 k)
(add1
(add1 (double n-1)))))
(cong eq (+ 2))))))
(claim twice=double
(Π ((n Nat))
(= Nat (twice n) (double n))))
(define twice=double
(λ (n)
(ind-Nat n
twice=double-mot
twice=double-base
twice=double-step)))
;; twice-Vec
(claim double-Vec-base
(Π ((E U))
(-> (Vec E 0) (Vec E 0))))
(define double-Vec-base
(λ (E v)
vecnil))
(claim double-Vec
(Π ((E U)
(n Nat))
(-> (Vec E n) (Vec E (double n)))))
(define double-Vec
(λ (E n)
(ind-Nat n
(λ (k) (-> (Vec E k) (Vec E (double k))))
(double-Vec-base E)
(λ (k acc)
(λ (v)
;; This would not work with twice because v, as
;; described by the type would have size `twice n`,
;; which has normal form
;; (iter-Nat k ....)
;; and Pie can't determine/prove that it
;; is not empty (it should start with add1).
(vec:: (head v)
(vec:: (head v)
(acc (tail v)))))))))
(claim twice-Vec
(Π ((E U)
(n Nat))
(-> (Vec E n) (Vec E (twice n)))))
(define twice-Vec
(λ (E n)
(λ (es)
(replace (symm (twice=double n))
(λ (k)
(Vec E k))
(double-Vec E n es)))))
;;
;; replicate
;;
(claim replicate
(Π ((E U)
(l Nat))
(-> E (Vec E l))))
(define replicate
(λ (E l)
(λ (e)
(ind-Nat l
(λ (k) (Vec E k))
vecnil
(λ (k v)
(vec:: e v))))))
;; list->vec
;;
;; This version has a type which accepts
;; buggy definitions of list->vec.
(claim list->vec-mot
(Π ((E U))
(-> (List E) U)))
(define list->vec-mot
(λ (E es)
(Vec E (length E es))))
(claim list->vec-step
(Π ((E U)
(e E)
(es (List E)))
(-> (Vec E (length E es))
(Vec E (add1 (length E es))))))
(define list->vec-step
(λ (E e es)
(λ (v)
(vec:: e v))))
(claim list->vec
(Π ((E U)
(es (List E)))
(Vec E (length E es))))
(define list->vec
(λ (E es)
(ind-List es
(list->vec-mot E)
vecnil
(list->vec-step E))))
;; vec-append
(claim vec-append-mot
(Π ((E U)
(j Nat)
(k Nat))
(-> (Vec E k) U)))
(define vec-append-mot
(λ (E j k)
(λ (v)
(Vec E (+ k j)))))
(claim vec-append-step
(Π ((E U)
(j Nat)
(k Nat)
(e E)
(es (Vec E k)))
(-> (vec-append-mot E j
k es)
(vec-append-mot E j
(add1 k) (vec:: e es)))))
(define vec-append-step
(λ (E j k e es)
(λ (almost-answer)
(vec:: e almost-answer))))
(claim vec-append
(Π ((E U)
(l Nat)
(j Nat))
(-> (Vec E l) (Vec E j)
(Vec E (+ l j)))))
(define vec-append
(λ (E l j)
(λ (v1 v2)
(ind-Vec l v1
(vec-append-mot E j)
v2
(vec-append-step E j)))))
;; define vec->list now, and we'll use it to prove
;; that converting a list to a vector and then back
;; into a list will give the same list. Ruling out
;; some foolish list->vec definitions.
(claim vec->list-mot
(Π ((E U)
(k Nat))
(-> (Vec E k) U)))
(define vec->list-mot
(λ (E k)
(λ (v) (List E))))
(claim vec->list-step
(Π ((E U)
(l-1 Nat)
(e E)
(es (Vec E l-1)))
(-> (vec->list-mot E l-1 es)
(vec->list-mot E (add1 l-1) (vec:: e es)))))
(define vec->list-step
(λ (E l-1 e es)
(λ (vec->list-es)
(:: e vec->list-es))))
(claim vec->list
(Π ((E U)
(l Nat))
(-> (Vec E l) (List E))))
(define vec->list
(λ (E l)
(λ (es)
(ind-Vec l es
(vec->list-mot E)
nil
(vec->list-step E)))))
;; ensure list->vec vec->list gives the original list back
(claim list->vec->list=-mot
(Π ((E U))
(-> (List E) U)))
(define list->vec->list=-mot
(λ (E es)
(= (List E)
es
(vec->list E
(length E es)
(list->vec E es)))))
(claim list->vec->list=-step
(Π ((E U)
(e E)
(es (List E)))
(-> (list->vec->list=-mot E es)
(list->vec->list=-mot E (:: e es)))))
;(define list->vec->list=-step
; (λ (E e es)
; (λ (eq)
; TODO)))
;
;(claim list->vec->list=
; (Π ((E U)
; (es (List E)))
; (= (List E)
; es
; (vec->list E
; (length E es)
; (list->vec E es)))))
;(define list->vec->list=
; (λ (E es)
; (ind-List es
; (list->vec->list=-mot E)
; (same nil)
; (list->vec->list=-step E))))
;;
;; 12. Even numbers can be odd
;;
(claim Even
(-> Nat U))
(define Even
(λ (n)
(Σ ((half Nat))
(= Nat n (double half)))))
(claim zero-is-even
(Even 0))
(define zero-is-even
(cons 0 (same 0)))
(claim +two-even
(Π ((n Nat))
(-> (Even n) (Even (+ 2 n)))))
(define +two-even
(λ (n eq)
(cons (add1 (car eq))
(cong (cdr eq) (+ 2)))))
(claim two-is-even
(Even 2))
(define two-is-even
(+two-even 0 zero-is-even))
(claim Odd
(-> Nat U))
(define Odd
(λ (n)
(Σ ((haf Nat))
(= Nat n (add1 (double haf))))))
(claim one-is-odd
(Odd 1))
(define one-is-odd
(cons 0 (same 1)))
(claim add1-even->odd
(Π ((n Nat))
(-> (Even n) (Odd (add1 n)))))
(define add1-even->odd
(λ (n even)
(cons (car even)
(cong (cdr even) (+ 1)))))
(claim add1-odd->even
(Π ((n Nat))
(-> (Odd n) (Even (add1 n)))))
(define add1-odd->even
(λ (n odd)
(cons (add1 (car odd))
(cong (cdr odd) (+ 1)))))
;;
;; Every number is either odd or even
;;
(claim even-or-odd
(Π ((n Nat))
(Either (Even n) (Odd n))))
(claim even-or-odd-step
(Π ((k-1 Nat))
(-> (Either (Even k-1) (Odd k-1))
(Either (Even (add1 k-1)) (Odd (add1 k-1))))))
(define even-or-odd-step
(λ (k-1)
(λ (proof-k-1)
(ind-Either proof-k-1
(λ (_) (Either (Even (add1 k-1)) (Odd (add1 k-1))))
(λ (proof-even)
(right (add1-even->odd k-1 proof-even)))
(λ (proof-odd)
(left (add1-odd->even k-1 proof-odd)))))))
(define even-or-odd
(λ (n)
(ind-Nat n
(λ (k) (Either (Even k) (Odd k)))
(left zero-is-even)
even-or-odd-step)))
;;
;; 14. There is safety in numbers
;;
(claim Maybe
(-> U U))
(define Maybe
(λ (X) (Either X Trivial)))
(claim nothing
(Π ((E U)) (Maybe E)))
(define nothing
(λ (E)
(right sole)))
(claim just
(Π ((E U)) (-> E (Maybe E))))
(define just
(λ (E x) (left x)))
(claim maybe-head
(Π ((E U))
(-> (List E) (Maybe E))))
(define maybe-head
(λ (E)
(λ (lst)
(rec-List lst
(nothing E)
(λ (hd tl acc)
(just E hd))))))
(claim maybe-tail
(Π ((E U))
(-> (List E) (Maybe (List E)))))
(define maybe-tail
(λ (E)
(λ (lst)
(rec-List lst
(nothing (List E))
(λ (hd tl acc)
(just (List E) tl))))))
(claim list-ref
(Π ((E U))
(-> Nat (List E) (Maybe E))))
(define list-ref
(λ (E)
(λ (k)
(rec-Nat k
(maybe-head E)
(λ (k-1 acc)
(λ (es)
(ind-Either (maybe-tail E es)
(λ (_) (Maybe E))
(λ (tl) (acc tl))
(λ (_) (nothing E)))))))))
;;
;; (Fin N)
;;
(claim Fin
(-> Nat U))
(define Fin
(λ (n)
(iter-Nat n
Absurd
Maybe)))
(claim fzero
(Π ((n Nat))
(Fin (add1 n))))
(define fzero
(λ (n)
(nothing (Fin n))))
(claim fadd1
(Π ((n Nat))
(-> (Fin n) (Fin (add1 n)))))
(define fadd1
(λ (n)
(λ (i-1)
(just (Fin n) i-1))))
(claim vec-ref
(Π ((E U)
(l Nat))
(-> (Fin l) (Vec E l) E)))
(claim vec-ref-base
(Π ((E U))
(-> (Fin zero) (Vec E zero)
E)))
(define vec-ref-base
(λ (E)
(λ (no-value es)
(ind-Absurd no-value
E))))
(claim vec-ref-step
(Π ((E U)
(l-1 Nat))
(-> (-> (Fin l-1)
(Vec E l-1)
E)
(-> (Fin (add1 l-1))
(Vec E (add1 l-1))
E))))
(define vec-ref-step
(λ (E l-1)
(λ (vec-ref-l-1)
(λ (i es)
(ind-Either i
(λ (i) E)
(λ (i-1) (vec-ref-l-1 i-1 (tail es)))
(λ (triv) (head es)))))))
(define vec-ref
(λ (E l)
(ind-Nat l
(λ (k)
(-> (Fin k) (Vec E k) E))
(vec-ref-base E)
(vec-ref-step E))))
;;
;;
(claim =consequence
(-> Nat Nat U))
(define =consequence
(λ (n j)
(which-Nat n
;; n=0
(which-Nat j
;; j=0
Trivial
(λ (j-1) Absurd))
;; n!=0
(λ (n-1)
(which-Nat j
;; j=0
Absurd
(λ (j-1)
(= Nat n-1 j-1)))))))
(claim =consequence-same
(Π ((n Nat))
(=consequence n n)))
(define =consequence-same
(λ (n)
(ind-Nat n
(λ (k)
(=consequence k k))
sole
(λ (n-1 almost)
(same n-1)))))
(claim use-Nat=
;; for every n and j Nats, if they are
;; equal, then consequence of they being
;; equal follows.
(Π ((n Nat)
(j Nat))
(-> (= Nat n j)
(=consequence n j))))
(define use-Nat=
(λ (n j)
(λ (n=j)
(replace n=j
(λ (k) (=consequence n k))
(=consequence-same n)))))
(claim zero-not-add1
(Π ((n Nat))
(-> (= Nat zero (add1 n))
Absurd)))
(define zero-not-add1
(λ (n)
(use-Nat= zero (add1 n))))
;;
;; pem, middle excluded...
;;
;; Every statement is either true or false
;(claim pem
; (-> X (Either X (-> X Abusrd))))
(claim pem-not-false
(Π ((X U))
(-> (-> (Either X (-> X Absurd))
Absurd)
Absurd)))
(define pem-not-false
(λ (X)
(λ (pem-false)
(pem-false
(right
(λ (x)
(pem-false (left x))))))))
(claim Dec
(-> U U))
(define Dec
(λ (X)
(Either X (-> X Absurd))))
(claim zero?
(Π ((j Nat))
(Dec (= Nat zero j))))
(define zero?
(λ (j)
(ind-Nat j
(λ (k) (Dec (= Nat zero k)))
(left (same 0))
(λ (j-1 zero?n-1)
(right (zero-not-add1 j-1))))))
(claim add1-not-zero
(Π ((n Nat))
(-> (= Nat (add1 n) zero)
Absurd)))
(define add1-not-zero
(λ (n) (use-Nat= (add1 n) zero)))
(claim mot-nat=?
(-> Nat U))
(define mot-nat=?
(λ (k)
(Π ((j Nat))
(Dec (= Nat k j)))))
(claim sub1=
(Π ((n Nat)
(j Nat))
(-> (= Nat (add1 n) (add1 j))
(= Nat n j))))
(define sub1=
(λ (n j)
(use-Nat= (add1 n) (add1 j))))
(claim dec-add1=
(Π ((n-1 Nat)
(j-1 Nat))
(-> (Dec (= Nat n-1 j-1))
(Dec (= Nat (add1 n-1) (add1 j-1))))))
(define dec-add1=
(λ (n-1 j-1 eq-or-not)
(ind-Either eq-or-not
(λ (_target)
(Dec (= Nat (add1 n-1) (add1 j-1))))
(λ (yes)
(left (cong yes (+ 1))))
(λ (no)
(right (λ (n=j)
(no (sub1= n-1 j-1 n=j))))))))
(claim nat=-step
(Π ((n-1 Nat))
(-> (mot-nat=? n-1)
(mot-nat=? (add1 n-1)))))
(define nat=-step
(λ (n-1 nat=?n-1 j)
(ind-Nat j
(λ (k) (Dec (= Nat (add1 n-1) k)))
(right (add1-not-zero n-1))
(λ (j-1 _)
(dec-add1= n-1 j-1
(nat=?n-1 j-1))))))
(claim nat=?
(Π ((n Nat)
(j Nat))
(Dec (= Nat n j))))
(define nat=?
(λ (n j)
((ind-Nat n
mot-nat=?
zero?
nat=-step)
j)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment