module TCQuestions where {- There are no goals to fill in in this buffer. Instead you must extend the language given below in three different ways. Make each extension in a seperate file named TCQuestions[A-C].agda. For each extension: 1. Extend the untyped and typed languages. 2. Extend the type inferer 3. Extend the type checker 4. Extend the evaluator 5. Give simple test expressions for the extended functionality which can be first typechecked and then evaluated. Note: Do not just paste the syntactic extensions from the last coursework. This time you your syntactic constructors can take other syntactic expressions as arguments. -} data Base : Set where data Nat : Set where z : Nat s : Nat → Nat data Fin : Nat → Set where z : ∀{n} → Fin (s n) s : ∀{n} → Fin n → Fin (s n) data Ty : Set where ι : Ty _⇒_ : Ty → Ty → Ty data RawTm : Nat → Set where var : ∀{n} → Fin n → RawTm n _\$_ : ∀{n} → RawTm n → RawTm n → RawTm n lam : ∀{n} → Ty → RawTm (s n) → RawTm n data Con : Set where ε : Con _<_ : Con → Ty → Con len : Con → Nat len ε = z len (Γ < σ) = s (len Γ) data Var : Con → Ty → Set where z : ∀{Γ σ} → Var (Γ < σ) σ s : ∀{Γ σ τ} → Var Γ τ → Var (Γ < σ) τ data Tm : Con → Ty → Set where var : ∀{Γ σ} → Var Γ σ → Tm Γ σ _\$_ : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ lam : ∀{Γ σ τ} → Tm (Γ < σ) τ → Tm Γ (σ ⇒ τ) data Maybe (A : Set) : Set where Just : A → Maybe A Nothing : Maybe A data Σ (A : Set)(B : A → Set) : Set where _,_ : (a : A) → B a → Σ A B fstΣ : ∀{A B} → Σ A B → A fstΣ (a , b) = a sndΣ : ∀{A B}(p : Σ A B) → B (fstΣ p) sndΣ (a , b) = b lookup : ∀ Γ → Fin (len Γ) → Σ Ty (Var Γ) lookup ε () lookup (Γ < σ) z = σ , z lookup (Γ < σ) (s i) = let x = lookup Γ i in fstΣ x , s (sndΣ x) data eqTy : Ty → Ty → Set where eq : ∀{σ} → eqTy σ σ uneq : ∀{σ τ} → eqTy σ τ isEq : (σ τ : Ty) → eqTy σ τ isEq ι ι = eq isEq ι (σ ⇒ τ) = uneq isEq (σ ⇒ τ) ι = uneq isEq (σ ⇒ τ) (σ' ⇒ τ') with isEq σ σ' | isEq τ τ' isEq (.σ ⇒ .τ) (σ ⇒ τ) | eq | eq = eq isEq (.σ ⇒ τ) (σ ⇒ τ') | eq | uneq = uneq isEq (σ ⇒ τ) (σ' ⇒ τ') | uneq | q = uneq infer : ∀ Γ → RawTm (len Γ) → Maybe (Σ Ty (Tm Γ)) infer Γ (var i) = let x = lookup Γ i in Just (fstΣ x , var (sndΣ x)) infer Γ (t \$ u) with infer Γ t infer Γ (t \$ u) | Nothing = Nothing infer Γ (t \$ u) | Just (ι , f) = Nothing infer Γ (t \$ u) | Just ((σ ⇒ τ) , f) with infer Γ u infer Γ (t \$ u) | Just ((σ ⇒ τ) , f) | Nothing = Nothing infer Γ (t \$ u) | Just ((σ ⇒ τ) , f) | Just (σ' , a) with isEq σ σ' infer Γ (t \$ u) | Just ((.σ ⇒ τ) , f) | Just (σ , a) | eq = Just (τ , (f \$ a)) infer Γ (t \$ u) | Just ((σ ⇒ τ) , f) | Just (σ' , a) | uneq = Nothing infer Γ (lam σ t) with infer (Γ < σ) t infer Γ (lam σ t) | Just p = Just ((σ ⇒ (fstΣ p)) , lam (sndΣ p)) infer Γ (lam σ t) | Nothing = Nothing check : ∀ Γ (σ : Ty) → RawTm (len Γ) → Maybe (Tm Γ σ) check Γ σ (var i) with lookup Γ i check Γ σ (var i) | σ' , x with isEq σ σ' check Γ σ (var i) | .σ , x | eq = Just (var x) check Γ σ (var i) | σ' , x | uneq = Nothing check Γ τ (t \$ u) with infer Γ u check Γ τ (t \$ u) | Nothing = Nothing check Γ τ (t \$ u) | Just (σ , a) with check Γ (σ ⇒ τ) t check Γ τ (t \$ u) | Just (σ , a) | Just f = Just (f \$ a) check Γ τ (t \$ u) | Just (σ , a) | Nothing = Nothing check Γ ι (lam σ t) = Nothing check Γ (σ ⇒ τ) (lam σ' t) with isEq σ σ' check Γ (σ ⇒ τ) (lam σ' t) | uneq = Nothing check Γ (σ ⇒ τ) (lam .σ t) | eq with check (Γ < σ) τ t check Γ (σ ⇒ τ) (lam .σ t) | eq | Just t' = Just (lam t') check Γ (σ ⇒ τ) (lam .σ t) | eq | Nothing = Nothing -- We only run the evaluator on well-typed expressions. Val : Ty → Set Val ι = Base Val (σ ⇒ τ) = Val σ → Val τ data Env : Con → Set where ε : Env ε _<_ : ∀{Γ σ} → Env Γ → Val σ → Env (Γ < σ) vlookup : ∀{Γ σ} → Var Γ σ → Env Γ → Val σ vlookup z (_ < v) = v vlookup (s i) (γ < _) = vlookup i γ eval : ∀{Γ σ} → Tm Γ σ → Env Γ → Val σ eval (var i) γ = vlookup i γ eval (t \$ u) γ = eval t γ (eval u γ) eval (lam t) γ = λ v → eval t (γ < v) {- Question A ========== Extend your language to support booleans with the following functionality: -} data Bool : Set where tt : Bool ff : Bool if_then_else_ : {S : Set} → Bool → S → S → S if tt then x else _ = x if ff then _ else y = y {- Question B ========== Extend your language to support finite products (a.k.a True and And, cartesian product and singleton, pairs and unit type) with the following functionality: -} data Unit : Set where void : Unit data _×_ (A B : Set) : Set where _,_ : A → B → A × B fst× : ∀{A B} → A × B → A fst× (a , b) = a snd× : ∀{A B} → A × B → B snd× (a , b) = b {- Question C ========== Extend your language to support natural numbers with the following functionality: -} -- (natural numbers defined above) -- Primitive recursion (induction on natural numbers) prim : {S : Set} → S → (Nat → S → S) → Nat → S prim zz ss z = zz prim zz ss (s n) = ss n (prim zz ss n) {- There are no explicit starred exercises but here are two suggestions: 1. Make some further language extensions. Failed extensions are also interesting. E.g. explain why some feature cannot be added easily added to this setup. 2. Experiment with the design of the typechecker. E.g. Can it be simplified/made more readible whilst still supporting the same functionality? Can it be nicely extended to provide more functionality? One example of the latter is McBride and McKinna's typechecker in the paper "the view from the left". Our typechecker returns a typed term as evidence of success; their typechecker also returns evidence of failure. -}