-- Advanced Functional Programming course 2019 -- Chalmers TDA342 / GU DIT260 -- -- 2019-03-04 Guest lecture by Andreas Abel -- -- Introduction to Agda -- -- File 1: The Curry-Howard Isomorphism -- {-# OPTIONS --allow-unsolved-metas #-} module Prelude where -- Natural numbers as our first example of -- an inductive data type. data ℕ : Set where zero : ℕ suc : (n : ℕ) → ℕ -- To use decimal notation for numerals, like -- 2 instead of (suc (suc zero)), connect it -- to the built-in natural numbers. {-# BUILTIN NATURAL ℕ #-} n : ℕ -- \ b N n = 6 -- Lists are a parameterized inductive data type. data List (A : Set) : Set where [] : List A _∷_ : (x : A) (xs : List A) → List A -- C-\ : : infixr 6 _∷_ {-# NON_TERMINATING #-} f : {A : Set} → List A → List A f [] = [] f {A} (x ∷ as) = f {A} (x ∷ as) -- C-c C-l load -- C-c C-c case split -- C-c C-. goal type and infer -- C-c C-SPC give -- C-c C-= constraints -- C-c C-s solve -- Disjoint sum type. data _⊎_ (S T : Set) : Set where -- \uplus inl : S → S ⊎ T inr : T → S ⊎ T infixr 4 _⊎_ either : ∀{A B C : Set} → A ⊎ B → (A → C) → (B → C) → C either (inl x) f g = f x either (inr x) f g = g x -- The empty sum is the type with 0 alternatives, -- which is the empty type. -- By the Curry-Howard-Isomorphism, -- which views a proposition as the set/type of its proofs, -- it is also the absurd proposition. data False : Set where ⊥-elim : False → {A : Set} → A ⊥-elim () -- C-c C-c RET split on result -- C-c C-SPC give -- C-c C-, show hypotheses and goal -- C-c C-. show hypotheses and infers type -- Tuple types -- The generic record type with two fields -- where the type of the second depends on the value of the first -- is called Sigma-type (or dependent sum), in analogy to -- -- Σ ℕ A = Σ A(n) = A(0) + A(1) + ... -- n ∈ ℕ record Σ (A : Set) (B : A → Set) : Set where -- \GS \Sigma constructor _,_ field fst : A snd : B fst open Σ infixr 5 _,_ data Σ' (A : Set) (B : A → Set) : Set where _,_ : (a : A) (b : B a) → Σ' A B record MyPair : Set where field p1 : ℕ p2 : ℕ → ℕ -- foo : MyPair -- MyPair.p1 foo = 1 -- MyPair.p2 foo zero = 4 -- MyPair.p2 foo (suc x) = x -- The non-dependent version is the ordinary Cartesian product. _×_ : (S T : Set) → Set -- \times S × T = Σ S λ _ → T infixr 5 _×_ -- The record type with no fields has exactly one inhabitant -- namely the empty tuple record{} -- By Curry-Howard, it corresponds to Truth, as -- no evidence is needed to construct this proposition. record True : Set where test : True test = record {} -- C-c C-a auto -- Example: distributivity A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) dist : ∀{A B C : Set} → A × (B ⊎ C) → (A × B) ⊎ (A × C) dist (a , inl b) = inl (a , b) dist (a , inr c) = inr (a , c) -- Vectors of length n data Vec (A : Set) : ℕ → Set where [] : Vec A zero _∷_ : {n : ℕ} (x : A) (xs : Vec A n) → Vec A (suc n) zeros : (n : ℕ) → Vec ℕ n zeros zero = [] zeros (suc n) = 0 ∷ zeros n repeat : (A : Set) → A → (n : ℕ) → Vec A n repeat A a zero = [] repeat A a (suc n) = a ∷ (repeat A a n) -- C-c C-r refine -- Relations -- Type-theoretically, the type of relations 𝓟(A×A) is -- -- A × A → Prop -- -- which is -- -- A × A → Set -- -- by the Curry-Howard-Isomorphism -- and -- -- A → A → Set -- -- by currying. Rel : (A : Set) → Set₁ Rel A = A → A → Set -- Less-or-equal on natural numbers _≤_ : Rel ℕ zero ≤ y = True suc x ≤ zero = False suc x ≤ suc y = x ≤ y -- C-c C-l load -- C-c C-c case split -- C-c C-, show goal and assumptions -- C-c C-. show goal and assumptions and current term -- C-c C-SPC give -- -} -- -} -- -} -- -}