A wispy syntax for Pie, from the excellent The Little Typer.

conversion.wpi

#lang wispie

;; 'encompassing' forms: claim, define, →, λ, Π - basically all the binding forms -
;; and a couple others that gain utility, such as ::
;; These implicitly encompass the remaining lines in the form as their sole remaining
;; parameter, unless explicitly indented to show boundaries (especially useful for
;; multiple lambda arguments, or to make clear that a lambda body is nested, e.g. a
;; lambda at the end of a line of other arguments)

claim Pear
U

define Pear
Pair ℕ ℕ

claim Pear-maker
U

define Pear-maker
→ ℕ ℕ
Pear

claim elim-Pear
→ Pear Pear-maker
Pear

define elim-Pear
λ : pear maker
maker
  car pear
  cdr pear

claim step-+
→ ℕ
ℕ

define step-+
λ : +_n-1
add1 +_n-1

claim +
→ ℕ ℕ
ℕ

define +
λ : a b
iter-ℕ a
  b
  step-+

claim pearwise+
→ Pear Pear
Pear

define pearwise+
λ : pa pb
elim-Pear pa
  λ : paa pad
  elim-Pear pb
    λ : pba pbd
    cons
      + paa pba
      + pad pbd

claim step-gauss
→ ℕ ℕ
ℕ

define step-gauss
λ : n-1 gauss_n-1
+ (add1 n-1) gauss_n-1

claim gauss
→ ℕ
ℕ

define gauss
λ : n
rec-ℕ n
  0
  step-gauss

claim zerop
→ ℕ
Atom

define zerop
λ : n
rec-ℕ n
  't
  λ : n-1 zerop_n-1
    'nil

claim *
→ ℕ ℕ
ℕ

define *
λ : n j
rec-ℕ n
  0
  λ : n-1 *_n-1
    + *_n-1 j

;; 3-98 (p. 98)

claim flip
Π : (A U) (D U)
→ : Pair A D
Pair D A

define flip
λ : A D p
cons
  cdr p
  car p

claim elim-Pair
Π : (A U) (D U) (X U)
→
  Pair A D
  (→ A D X)  ;; Explicit bound
  X

define elim-Pair
λ : A D X p elim
elim
  car p
  cdr p

claim kar
→ : Pair ℕ ℕ
ℕ

define kar
λ : p
elim-Pair
  ℕ . ℕ
  ℕ
  p
  λ : a d
    a

claim kdr
→ : Pair ℕ ℕ
ℕ

define kdr
λ : p
elim-Pair
  ℕ . ℕ
  ℕ
  p
  λ : a d
    d

claim swap
→ : Pair ℕ Atom
Pair Atom ℕ

define swap
λ : p
elim-Pair
  ℕ . Atom
  Pair Atom ℕ
  p
  λ : a d
    cons d a

claim twin
Π : (Y U)
→ Y
Pair Y Y

define twin
λ : Y y
cons y y

claim expectations
List Atom

define expectations
:: 'cooked
:: 'eaten
:: 'tried-cleaning
:: 'understood
:: 'slept
∅

claim rugbrØd : List Atom

define rugbrØd
:: 'rye-flour
:: 'rye-kernels
:: 'water
:: 'sourdough
:: 'salt
∅

claim toppings : List Atom

define toppings
:: 'potato
:: 'butter
∅

claim condiments : List Atom

define condiments
:: 'chives
:: 'mayonnaise
∅

claim length
Π : (E U)
→ : List E
ℕ

define length
λ : E es
rec-List es
  0
  λ : e es-rest length_es-rest
    add1 length_es-rest

claim append
Π : (E U)
→
  List E
  List E
  List E

define append
λ : E es-1 es-2
rec-List es-1
  es-2
  λ : e es-rest append_es-rest
    :: e append_es-rest

claim snoc
Π : (E U)
→
  List E
  E
  List E

define snoc
λ : E es e
rec-List es
  :: e ∅
  λ : e-next es-rest snoc_es-rest
    :: e-next snoc_es-rest

claim reverse
Π : (E U)
→ : List E
List E

define reverse
λ : E es
rec-List es
  the (List E) ∅
  λ : e es-rest reverse_es-rest
    snoc E reverse_es-rest e

claim first-of-one
Π : (E U)
→ : Vec E 1
E

define first-of-one
λ : E v
head v

claim first
Π : (E U) (l ℕ)
→ : Vec E (add1 l)
E

define first
λ : E l-1 es
head es

claim rest
Π : (E U) (l ℕ)
→ : Vec E (add1 l)
Vec E l

define rest
λ : E l-1 es
tail es

claim peas
Π : (how-many-peas ℕ)
Vec Atom how-many-peas

define peas
λ : how-many-peas
ind-ℕ how-many-peas
  λ : n
    Vec Atom n
  the (Vec Atom 0) vec∅
  λ : l-1 peas_l-1
    vec:: 'pea peas_l-1

claim also-rec-ℕ
Π : (X U)
→ ℕ X (→ ℕ X X)
X

define also-rec-ℕ
λ : X n base step
ind-ℕ n
  λ : k
    X
  base
  step

claim base-last
Π : (E U)
→ : Vec E 1
E

define base-last
λ : E es-1
head es-1

claim mot-last
→ U ℕ
U

define mot-last
λ : E k
→ : Vec E (add1 k)
E

claim step-last
Π : (E U) (l ℕ)
→ : mot-last E l
mot-last E (add1 l)

define step-last
λ : E l-1 last_l-1 es
last_l-1
  tail es

claim last
Π : (E U) (l ℕ)
→ : Vec E (add1 l)
E

define last
λ : E l
ind-ℕ l
  mot-last E
  base-last E
  step-last E

claim base-drop-last
Π : (E U)
→ : Vec E 1
Vec E 0

define base-drop-last
λ : E es
vec∅

claim mot-drop-last
→ U ℕ
U

define mot-drop-last
λ : E l
→ : Vec E (add1 l)
Vec E l

claim step-drop-last
Π : (E U) (l-1 ℕ)
→ : mot-drop-last E l-1
mot-drop-last E (add1 l-1)

define step-drop-last
λ : E l-1 drop-last_es-1 es
vec::
  head es
  drop-last_es-1
    tail es

claim drop-last
Π : (E U) (l ℕ)
→ : Vec E (add1 l)
Vec E l

define drop-last
λ : E l
ind-ℕ l
  mot-drop-last E
  base-drop-last E
  step-drop-last E

claim incr
→ ℕ
ℕ

define incr
λ : n
iter-ℕ n
  1
  + 1

claim +1=add1
Π : (n ℕ)
= ℕ
  + 1 n
  add1 n

define +1=add1
λ : n
same : add1 n

claim mot-incr=add1
→ ℕ
U

define mot-incr=add1
λ : n
= ℕ
  incr n
  add1 n

claim base-incr=add1
= ℕ
  incr 0
  add1 0

define base-incr=add1
same 1

claim mot-step-incr=add1
→ ℕ ℕ
U

define mot-step-incr=add1
λ : n-1 k
= ℕ
  add1 : incr n-1
  add1 k

claim step-incr=add1
Π : (n-1 ℕ)
→
  = ℕ
    incr n-1
    add1 n-1
  = ℕ
    add1 : incr n-1
    add1 : add1 n-1

define step-incr=add1
λ : n-1 incr=add1_n-1
replace incr=add1_n-1
  mot-step-incr=add1 n-1
  same : add1 (incr n-1)

claim incr=add1
Π : (n ℕ)
= ℕ
  incr n
  add1 n

define incr=add1
λ : n
ind-ℕ n
  mot-incr=add1
  base-incr=add1
  step-incr=add1