Example of Andromeda ML-programming

example.m31

(* In Andromeda everything the user writes is "meta-level programming. *)

(* ML-level natural numbers *)
mltype rec mlnat =
  | zero
  | succ of mlnat
  end

(* We can use the meta-level numbers to define a program which computes n-fold iterations
  of f. Here we give an explicit type of iterate because the ML-type inference cannot tell
  whether f is an ML-function or an object-level term. *)
let rec iterate f x n : judgment → judgment → mlnat → judgment =
  match n with
  | zero ⇒ x
  | succ ?n ⇒ f (iterate f x n)
  end

constant A : Type
constant a : A
constant g : A → A

do iterate g a (succ (succ (succ zero)))
(* output: ⊢ g (g (g a)) : A *)

(* Defining iteration of functions at object-level is a different business. We first
   axiomatize the natural numbers. *)
constant nat : Type
constant O : nat
constant S : nat → nat
constant nat_rect : Π (P : nat → Type) (s0 : P O) (s : Π (n : nat), P n → P (S n)) (m : nat), P m

constant nat_iota_O :
  Π (P : nat → Type) (s0 : P O) (s : Π (n : nat), P n → P (S n)),
  nat_rect P s0 s O ≡ s0

constant nat_iota_S :
  Π (P : nat → Type) (s0 : P O) (s : Π (n : nat), P n → P (S n)) (m : nat),
  nat_rect P s0 s (S m) ≡ s m (nat_rect P s0 s m)

(* We use the standard library to get correct normalization of nat_rect *)
now reducing = add_reducing nat_rect [lazy, lazy, lazy, eager]
now betas = add_betas [nat_iota_O, nat_iota_S]

(* Iterataion at object-level is defined using nat_rect, as it is
   just the non-dependent version of induction. *)
constant iter : ∏ (X : Type), (X → X) → X → nat → X
constant iter_def :
  ∏ (X : Type) (f : X → X) (x : X) (n : nat),
    iter X f x n ≡ nat_rect (λ _, X) x (λ _ y, f y) n

(* We tell the standard library about the definition of iter *)
now betas = add_beta iter_def

(* An object-level iteration of g can be done as follows. *)
do iter A g a (S (S (S O)))
(* output: ⊢ iter A g a (S (S (S O))) : A *)

(* We can use the whnf function from the standard library to normalize a term. By default
   it performs weak head-normalization. But here we *locally* tell it to aggresively
   normalize arguments of g. *)
do
  now reducing = add_reducing g [eager] in
  whnf (iter A g a (S (S (S O))))
(* output: ⊢ refl (g (g (g a))) : iter A g a (S (S (S O))) ≡ g (g (g a)) *)

(* We can also pattern-match on terms at ML-level. *)
do
  match g (g (g a)) with
  | ⊢ (?h (?h ?x)) ⇒ h x
  end
(* output ⊢ g (g a) : A *)

(* We can match anywhere, also under a λ-expression. Because match is ML-level it computes
   immediately, i.e, it actually matches against the bound variable x. *)
do
  (λ x : A,
    match x with
    | ⊢ ?f ?y ⇒ y
    | ⊢ ?z ⇒ g z
    end) (g a)
(* output ⊢ (λ (x : A), g x) (g a) : A *)

(* Now suppose we want to construct λ h, h (h (h a)) using iteration. Since λ-expressions
   are still just ML-level programs which compute judgments, we can do it as follows using
   the ML-level iteration. *)
do λ h : A → A, iterate h a (succ (succ (succ zero)))
(* output: ⊢ λ (h : A → A), h (h (h a)) : (A → A) → A *)

(* If we use object-level iteration we get a different term which
   is still equal to the one we wanted. *)
do λ h : A → A, iter A h a (S (S (S O)))
(* output: ⊢ λ (h : A → A), iter A h a (S (S (S O))) : (A → A) → A *)

(* The standard library is smart enough to see that the two terms
   are equal. (It has funext built in.) *)
do 
  let u = λ (h : A → A), iterate h a (succ (succ (succ zero)))
  and v = λ (h : A → A), iter A h a (S (S (S O))) in
  refl u : u ≡ v
(* output: 
   ⊢ refl (λ (h : A → A), h (h (h a)))
     : (λ (h : A → A), h (h (h a))) ≡
       (λ (h : A → A), iter A h a (S (S (S O))))
*)

(* We could use object-level iteration and normalization to compute
   the desired term as follows. *)
do 
  λ h : A → A,
    now reducing = add_reducing h [eager] in
    match whnf (iter A h a (S (S (S O)))) with
    | ⊢ _ : _ ≡ ?e ⇒ e
    end
(* output: ⊢ λ (h : A → A), h (h (h a)) : (A → A) → A *)