-- 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 -- Truth record ⊤ : Set where -- Absurdity data ⊥ : Set where ⊥-elim : {A : Set} → ⊥ → A ⊥-elim = {!!} ¬ : (A : Set) → Set ¬ A = A → ⊥ -- Decidable propositions data Dec (P : Set) : Set where -- 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 = {!!} ⇒injr : ∀{a b c d} → (a ⇒ c) ≡ (b ⇒ d) → c ≡ d ⇒injr = {!!} -- Deciding type equality eqTy : (a b : Ty) → Dec (a ≡ b) eqTy = {!!} -- Raw de Bruijn terms data Exp : Set where -- Well typed well-scoped variables Cxt = List Ty data Var : ∀(Γ : Cxt) (x : ℕ) (a : Ty) → Set where -- Bidirectional calculus mutual data Ne (Γ : Cxt) : (e : Exp) (b : Ty) → Set where data Nf (Γ : Cxt) : (e : Exp) (a : Ty) → Set where -- Sound context lookup data Lookup (Γ : Cxt) (n : ℕ) : Set where lookupVar : ∀ Γ (x : ℕ) → Lookup Γ x lookupVar = {!!} -- Sound type checking -- Result of type checking data Infer (Γ : Cxt) (e : Exp) : Set where data Check (Γ : Cxt) (e : Exp) (a : Ty) : Set where -- Inference rules -- Variable inferVar : {!!} inferVar = {!!} -- Application inferApp : {!!} inferApp = {!!} -- nfView data Inferable : Exp → Set where data NfView : Exp → Set where nfView : (e : Exp) → NfView e nfView e = {!!} -- Checking rules -- Neutrals checkNe : {!!} checkNe = {!!} -- Abstraction checkAbs : {!!} checkAbs = {!!} -- Sound type-checker mutual check : ∀ Γ e a → Check Γ e a check Γ e a = {!!} infer : ∀ Γ e → Infer Γ e infer Γ e = {!!}