FLOPS 2016 Agda Tutorial, Andreas Abel

FLOPS2016.agda

-- FLOPS 2016 Agda Tutorial
module FLOPS2016 where

-- 歴史の話
-- ALF Half Agda1 ALFA AgdaLight Agda2

-- Simply Typed Lambda Calculus
--   Checking Inference Lookup Rules

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

data List (A : Set) : Set where
  [] : List A
  _∷_ : (x : A) (xs : List A) → List A

record ⊤ : Set where
  constructor tt

data ⊥ : Set where

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

¬ : (A : Set) → Set
¬ A = A → ⊥

data Dec (P : Set) : Set where
  yes : (p : P) → Dec P
  no : (p : ¬ P) → Dec P

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

_≢_ : {A : Set} (x y : A) → Set
x ≢ y = ¬ (x ≡ y)

pred : ℕ → ℕ
pred (suc n) = n
pred zero = zero

test : pred (suc zero) ≡ zero
test = refl

data Ty : Set where
  base : Ty
  _⇒_ : (a b : Ty) → Ty

⇒≠base : ∀ {a b} → (a ⇒ b) ≡ base → ⊥
⇒≠base ()

⇒injl : ∀ {a b c d} → (a ⇒ c) ≡ (b ⇒ d) → a ≡ b
⇒injl refl = refl

⇒injr : ∀ {a b c d} → (a ⇒ c) ≡ (b ⇒ d) → c ≡ d
⇒injr refl = refl

eqTy : (a b : Ty) → Dec (a ≡ b)
eqTy base base = yes refl
eqTy base (b ⇒ b₁) = no (λ ())
eqTy (a ⇒ a₁) base = no (λ ())
eqTy (a ⇒ a₁) (b ⇒ b₁) with eqTy a b | eqTy a₁ b₁
eqTy (a ⇒ a₁) (.a ⇒ .a₁) | yes refl | yes refl = yes refl
eqTy (a ⇒ a₁) (.a ⇒ b₁) | yes refl | no ¬p = no (λ x → ¬p (⇒injr x))
eqTy (a ⇒ a₁) (b ⇒ .a₁) | no ¬p | yes refl = no (λ x → ¬p (⇒injl x))
eqTy (a ⇒ a₁) (b ⇒ b₁) | no ¬p | no ¬p₁ = no (λ x → ¬p (⇒injl x))

-- Raw de Brujin terms

data Exp : Set where
  var : (x : ℕ) → Exp
  abs : (e : Exp) → Exp
  app : (f e : Exp) → Exp

Cxt = List Ty

data Var : (Γ : Cxt) (x : ℕ) (a : Ty) → Set where
  vz : ∀ {Γ a} → Var (a ∷ Γ) zero a
  vs : ∀ {Γ a b n} → (x : Var Γ n a) → Var (b ∷ Γ) (suc n) a

-- Bidirectional Calculus

mutual
 data Ne (Γ : Cxt) : (e : Exp) (b : Ty) → Set where
   var : ∀ {n a} → (x : Var Γ n a) → Ne Γ (var n) a
   app : ∀ {f e a b} → (t : Ne Γ f (a ⇒ b)) → (u : Nf Γ e a) → Ne Γ (app f e) b

 data Nf (Γ : Cxt) : (e : Exp) (a : Ty) → Set where
   ne : ∀ {e a} → (t : Ne Γ e a) → Nf Γ e a
   abs : ∀ {e a b} → (t : Nf (a ∷ Γ) e b) → Nf Γ (abs e) (a ⇒ b)

-- Sound context lookup

data Lookup (Γ : Cxt) (n : ℕ) : Set where
  yes : (a : Ty) (x : Var Γ n a) → Lookup Γ n
  no : Lookup Γ n

lookupVar : ∀ Γ (x : ℕ) → Lookup Γ x
lookupVar [] x = no
lookupVar (a ∷ Γ) zero = yes a vz
lookupVar (a ∷ Γ) (suc n) with lookupVar Γ n
lookupVar (a ∷ Γ) (suc n) | yes b x = yes b (vs x)
lookupVar (a ∷ Γ) (suc n) | no = no

-- Sound type checking

-- Result of type checking

data Infer (Γ : Cxt) (e : Exp) : Set where
  yes : (a : Ty) (t : Ne Γ e a) → Infer Γ e
  no : Infer Γ e

data Check (Γ : Cxt) (e : Exp) (a : Ty) : Set where
  yes : (t : Nf Γ e a) → Check Γ e a
  no : Check Γ e a

-- Variables

inferVar : ∀ Γ x → Infer Γ (var x)
inferVar Γ x with lookupVar Γ x
inferVar Γ x | yes a p = yes a (var p)
inferVar Γ x | no = no

-- Application

inferApp : ∀ {Γ f e} → Infer Γ f → (∀ a → Check Γ e a) → Infer Γ (app f e)
inferApp (yes base t) k = no
inferApp (yes (a ⇒ b) t) k with k a
inferApp (yes (a ⇒ b) t₁) k | yes t = yes b (app t₁ t)
inferApp (yes (a ⇒ b) t) k | no = no
inferApp no u = no

-- Neautrals

checkNe : ∀ {Γ e} → (a : Ty) → (t : Infer Γ e) → Check Γ e a
checkNe a (yes a₁ t) with eqTy a a₁
checkNe a (yes .a t) | yes refl = yes (ne t)
checkNe a (yes a₁ t) | no ¬p = no
checkNe a no = no

-- Abstraction

checkAbs : ∀ {Γ e a b} → Check (a ∷ Γ) e b → Check Γ (abs e) (a ⇒ b)
checkAbs (yes t) = yes (abs t)
checkAbs no = no

-- Sound type-checker

mutual
  check : ∀ Γ e a → Check Γ e a
  check Γ (var x) a = checkNe a (infer Γ (var x))
  check Γ (abs e) base = no
  check Γ (abs e) (a ⇒ a₁) = checkAbs (check (a ∷ Γ) e a₁)
  check Γ (app f e) a = checkNe a (infer Γ (app f e))

  infer : ∀ Γ e → Infer Γ e
  infer Γ (var x) = inferVar Γ x
  infer Γ (abs e) = no
  infer Γ (app f e) = inferApp (infer Γ f) (check Γ e)