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