-- Agda tutorial at FLOPS 2016
-- Andreas Abel (partially plagiarized from Ulf Norell's ICFP 2013 talk)
-- 2016-03-06

-- Prelude

-- Basic types

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

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

-- Basic propositions

-- Absurdity

data ⊥ : Set where

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

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

-- Decidable propositions

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

-- Equality

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

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

-- Simply-typed lambda-calculus

-- Types

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

-- Type equality is propositional equality

-- Injectivity properties

⇒≠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

-- Deciding type equality

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

-- Raw de Bruijn terms

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

data Inferable : Exp → Set where
  var : ∀{x} → Inferable (var x)
  app : ∀{f e} → Inferable (app f e)

data NfView : Exp → Set where
  abs : {e : Exp} → NfView (abs e)
  inf : ∀{e} (i : Inferable e) → NfView e

nfView : (e : Exp) → NfView e
nfView (abs e) = abs
nfView (var x) = inf var
nfView (app f e) = inf app

-- Well typed well-scoped variables

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 b} (x : Var Γ n b) → Ne Γ (var n) b
    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 LookupError : ∀ (Γ : Cxt) (n : ℕ) → Set where
  vz : ∀{n} → LookupError [] n
  vs : ∀{Γ a n} (err : LookupError Γ n) → LookupError (a ∷ Γ) (suc n)

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

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

-- Sound type checking

-- Type errors

mutual

  data InferError (Γ : Cxt) : (e : Exp) → Set where
    var  : ∀{x} (err : LookupError Γ x) → InferError Γ (var x)
    abs  : ∀ e → InferError Γ (abs e)
    appl : ∀{f e} (err : InferError Γ f) → InferError Γ (app f e)
    ¬fun : ∀{f e} (t : Ne Γ f base) → InferError Γ (app f e)
    ¬arg : ∀{f e a b} (t : Ne Γ f (a ⇒ b)) (err : CheckError Γ e a) → InferError Γ (app f e)

  data CheckError (Γ : Cxt) : (e : Exp) (a : Ty) → Set where
    absBase : ∀ e → CheckError Γ (abs e) base
    conv    : ∀{e a b} (t : Ne Γ e a) (q : a ≢ b) → CheckError Γ e b
    abs     : ∀{e a b} (err : CheckError (a ∷ Γ) e b) → CheckError Γ (abs e) (a ⇒ b)
    ne      : ∀{e a} (inf : Inferable e) (err : InferError Γ e) → CheckError Γ e a

-- Result of type checking

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

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

-- Rules

-- Variable

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

-- Application

inferApp : ∀ {Γ}{f e : Exp} →
           Infer Γ f → (∀ a → Check Γ e a) → Infer Γ (app f e)
inferApp (yes base t) k = no (¬fun t )
inferApp (yes (a ⇒ b) t) k with k a
inferApp (yes (a ⇒ b) t) k | yes u = yes b (app t u)
inferApp (yes (a ⇒ b) t) k | no q = no (¬arg t q)
inferApp (no q) k = no (appl q)

-- Neutrals

checkNe : ∀{Γ}{e : Exp} (i : Inferable e) a → Infer Γ e → Check Γ e a
checkNe i a (yes b t) with eqTy b a
checkNe i a (yes .a t) | yes refl = yes (ne t)
checkNe i a (yes b t)  | no ¬p = no (conv t ¬p)
checkNe i a (no err) = no (ne i err)

-- Abstraction

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

-- Sound type-checker

mutual
  check : ∀ Γ e a → Check Γ e a
  check Γ e a with nfView e
  check Γ (abs e) base    | abs   = no (absBase e)
  check Γ (abs e) (a ⇒ b) | abs   = checkAbs (check (a ∷ Γ) e b)
  check Γ e a             | inf i = checkNe i a (infer Γ e)

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

-- Completeness
-- We show that the presence of a type error implies untypability

-- Completeness of context lookup

soundLookupError : ∀{Γ n} (err : LookupError Γ n) → ∀ {a} (x : Var Γ n a) → ⊥
soundLookupError vz ()
soundLookupError (vs err) (vs x) = soundLookupError err x

-- Uniqueness of inferred types

uniqueVar : ∀ {Γ a b} {n : ℕ} (x : Var Γ n a) (y : Var Γ n b) → a ≡ b
uniqueVar vz vz = refl
uniqueVar (vs x) (vs y) with uniqueVar x y
uniqueVar (vs x) (vs y) | refl = refl

unique : ∀ {Γ a b} {e : Exp} (t : Ne Γ e a) (u : Ne Γ e b) → a ≡ b
unique (var x) (var y) = uniqueVar x y
unique (app t₁ u₁) (app t u) with unique t₁ t
unique (app t₁ u₁) (app t u) | refl = refl

-- Completeness of type-checking

mutual

  soundInferError : ∀{Γ e} (err : InferError Γ e) → ∀ {a} (t : Ne Γ e a) → ⊥
  soundInferError (var err) (var x)              = soundLookupError err x
  soundInferError (abs e) ()
  soundInferError (appl err) (app t u)           = soundInferError err t
  soundInferError (¬fun t) (app t₁ u) with unique t t₁
  ... | ()
  soundInferError (¬arg t err) (app t₁ u) with unique t t₁
  soundInferError (¬arg t err) (app t₁ u) | refl = soundCheckError err u

  soundCheckError : ∀{Γ e a} (err : CheckError Γ e a) (t : Nf Γ e a) → ⊥
  soundCheckError (absBase e) (ne ())
  soundCheckError (conv t q) (ne t₁)             = q (unique t t₁)
  soundCheckError (conv () q) (abs t₁)
  soundCheckError (abs err) (ne ())
  soundCheckError (abs err) (abs t)              = soundCheckError err t
  soundCheckError (ne i err) (ne t)              = soundInferError err t
  soundCheckError (ne () (abs e)) (abs t)