-- 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)