Slides and tutorial for my guest lectures on Agda at the University of Edinburgh in 2017.

lecture1.agda

{-(- by Wen Kokke, borrowing heavily from CS410-17 lecture 1 by Conor McBride -)-}

module lecture1 where

module sum-and-product-types where

{--------------------------------------------------------------------------------}
-- so Coq and Agda are kinda the same, yet very different

-- * it's said Coq looks like ML and Agda looks like Haskell
--   (I don't really know ML, but I know Haskell, so for me...)

  data Bool : Set where
    true  : Bool
    false : Bool

{-+}
  not : Bool → Bool
  not b = ?
{+-}

-- * bad news? Agda doesn't really have tactics...
--   (it forces you wrote write programs by hand)
--   (but it doesn't force you to learn magic, i.e. Ltac)

-- * good news? Agda has a lot fewer quirks than Coq...
--   (overall, I'd say it is a lot easier to get what is going on in Agda)

-- * this is as good a time as any to bring up Unicode



{--------------------------------------------------------------------------------}
-- so how about we write some Agda?

  data 𝟎 : Set where -- we input 𝟎 as \B0
    -- we can _only_ construct values of a datatype using its constructors.
    -- there are _no_ constructors for the empty type, so there are no values.

{-+}
  nope : {A : Set} → 𝟎 → A -- should probably talk about those braces {_}
  nope e = ?
{+-}

  record 𝟏 : Set where -- we input 𝟏 as \B1
    -- we can construct instances of record types by giving values for all their
    -- fields. I'd put an empty "field" section here but Agda's parser doesn't
    -- like those. anyway, there aren't any fields, so:

  unit : 𝟏
  unit = record {}

  you-figure-it-out : 𝟏 -- honestly, this is a pretty easy request
  you-figure-it-out = _



{--------------------------------------------------------------------------------}
-- so we've got 𝟎 and 𝟏, what about + and ×?

  data _+_ (A B : Set) : Set where
    inl : A → A + B
    inr : B → A + B

-- you should tell them what do those underscores mean

  Π : (A : Set) (B : A → Set) → Set
  Π A B = (x : A) → B x

  record Σ (A : Set) (B : A → Set) : Set where
    constructor _,_
    field
      fst : A
      snd : B fst
  open Σ public -- bring `_,_`, `fst`, and `snd` into scope and export them

-- what does that have to do with _×_?

  _×_ : (A B : Set) → Set -- we input × as \x
  A × B = Σ A λ _ → B -- this lambda looks funky, maybe talk about it



{--------------------------------------------------------------------------------}
-- why do you insist on calling these 𝟎, 𝟏, _+_, and _×_?!

  infix 10 _↔_ -- we input ↔ as \<->

  _↔_ : (A B : Set) → Set
  A ↔ B = (A → B) × (B → A)

{-+} -- maybe talk about that ∀ and those {_}?
  ×-comm : ∀ {A B} → A × B → B × A -- we input ∀ as \all
  ×-comm = ?
{+-}

{-+}
  ×-assLR : ∀ {A B C} → A × (B × C) → (A × B) × C
  ×-assLR = ?
{+-}

{-+}
  ×-idR : ∀ {A} → A ↔ A × 𝟏
  ×-idR = ?
{+-}



{--------------------------------------------------------------------------------}
-- why do you insist on calling these 𝟎, 𝟏, _+_, and _×_?!

{-+}
  +-comm : ∀ {A B} → A + B → B + A
  +-comm = {!!}
{+-}

{-+}
  +-assLR : ∀ {A B C} → (A + B) + C → A + (B + C)
  +-assLR = {!!}
{+-}

{-+}
  +-idR : ∀ {A} → A + 𝟎 → A
  +-idR = {!!}
{+-}

{-+}
  ×+-dist : ∀ {A B C} → A × (B + C) → (A × B) + (A × C)
  ×+-dist = ?
{+-}



{-+----------------------------------------------------------------------------+-}

module naturals where

  open sum-and-product-types using (_↔_; _,_; 𝟎; 𝟏; unit)

{--------------------------------------------------------------------------------}
-- OK, we're convinced, but can't we just have normal + and × instead?
-- (no, not really, because I've used those identifiers already)

  data ℕ : Set where -- we input ℕ as \bN
    zero : ℕ
    suc  : ℕ → ℕ

  {-# BUILTIN NATURAL ℕ #-} -- means we can write 0, 1, 2, etc.

  _+_ : ℕ → ℕ → ℕ
  zero  + y = y
  suc x + y = suc (x + y)

  ex1 : ℕ
  ex1 = 4 + 5

-- but how do we write equalities? _↔_ won't really cut it for ℕ...

  ex2 : ℕ ↔ ℕ
  ex2 = (λ x → x) , (λ _ → 4)



-- here be lies that I've hidden from you:
-- we can tell Agda about _+_ so that it can optimize it better

  {-# BUILTIN NATPLUS _+_ #-}

{--------------------------------------------------------------------------------}
-- right, so how do we build equalities?
-- (Coq kinda hides this definition from you, but it's there as well)

  infix 10 _≡_

  data _≡_ {A : Set} : A → A → Set where
    refl : ∀ {x} → x ≡ x

{-+} -- make sure you write this using a dot pattern
  sym : ∀ {A} {x y : A} → x ≡ y → y ≡ x
  sym p = ?
{+-}

{-+}
  trans : ∀ {A} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
  trans p q = ?
{+-}

{-+}
  cong : ∀ {A B} {x y} (f : A → B) → x ≡ y → f x ≡ f y
  cong f p = ?
{+-}



{-+----------------------------------------------------------------------------+-}

-- here be lies that I've hidden from you:
-- we can tell Agda about our equality so we can use it with 'rewrite'

  {-# BUILTIN EQUALITY _≡_ #-}

{--------------------------------------------------------------------------------}
-- right, so how do we build equalities? let's do some proofs!

{-+}
  +-idR : ∀ x → x ≡ x + 0
  +-idR x = ?
{+-}

{-+}
  +-suc : ∀ x y → 1 + (x + y) ≡ x + (1 + y)
  +-suc x y = ?
{+-}

{-+}
  +-comm : ∀ x y → x + y ≡ y + x
  +-comm x y = ?
{+-}

{-+}
  +-assLR : ∀ x y z → x + (y + z) ≡ (x + y) + z
  +-assLR x y z = ?
{+-}



{--------------------------------------------------------------------------------}
-- if you want to do this, you're free to -- but I'm not gonna

  _*_ : ℕ → ℕ → ℕ
  zero  * y = 0
  suc x * y = y + (x * y)

{-+}
  *-idR : ∀ x → x ≡ x * 0
  *-idR x = ?
{+-}

{-+}
  *-suc : ∀ x y → 1 * (x * y) ≡ x * (1 * y)
  *-suc x y = ?
{+-}

{-+}
  *-comm : ∀ x y → x * y ≡ y * x
  *-comm x y = ?
{+-}

{-+}
  *-assLR : ∀ x y z → x * (y * z) ≡ (x * y) * z
  *-assLR x y z = ?
{+-}

{-+}
  *+-dist : ∀ x y z → x * (y + z) → (x * y) + (x * z)
  *+-dist x y z = ?
{+-}



{-+----------------------------------------------------------------------------+-}

-- here be lies that I've hidden from you:
-- we can tell Agda about _+_ so that it can optimize it better

  {-# BUILTIN NATTIMES _*_ #-}

{--------------------------------------------------------------------------------}
-- but what if the proofs get really large? I don't wanna work that hard!

  data _≤_ : ℕ → ℕ → Set where -- we input ≤ as \<= or \le
    refl : ∀ {x} → 0 ≤ x
    step : ∀ {x y} → x ≤ y → suc x ≤ suc y

  ex3 : 4 ≤ 5
  ex3 = step (step (step (step refl)))

  -- this looks like it's going to be a problem...

  _≤?_ : ℕ → ℕ → Set
  zero  ≤? y     = 𝟏 -- that's the unit type
  suc x ≤? zero  = 𝟎 -- that's the empty type
  suc x ≤? suc y = x ≤? y

{-+}
  prove : ∀ x y → x ≤? y → x ≤ y
  prove x y p = ?
{+-}

{-+}
  ex4 : 112 ≤ 482
  ex4 = ?
{+-}

lecture2.agda

{-# OPTIONS --type-in-type #-} -- minor cheats follow
module lecture2 where

open import Agda.Builtin.FromNat using (Number)
open import Data.Bool using (Bool; true; false; _∧_; if_then_else_)
open import Data.Empty using () renaming (⊥ to 𝟎)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Nat using (ℕ; suc; zero; _≤?_)
open import Data.Product using (_×_; _,_) renaming (proj₁ to fst; proj₂ to snd)
open import Data.Unit using (tt) renaming (⊤ to 𝟏)
open import Function as F using (case_of_)
open import Relation.Nullary.Decidable using (True; toWitness)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong₂)

-- here be cheats: in order to overload natural number notation,
-- we need to specify how it works for naturals... which is easy

instance
  NatNumber : Number ℕ
  NatNumber = record
    { Constraint = F.const 𝟏
    ; fromNat    = λ n → n
    }

∧-split : ∀ {b₁ b₂} → b₁ ∧ b₂ ≡ true → b₁ ≡ true × b₂ ≡ true
∧-split {false} {_}     ()
∧-split {true}  {false} ()
∧-split {true}  {true}  _ = (refl , refl)

module coq-style-1 where

{-------------------------------------------------------------------------}
  -- we're gonna talk about the simply-typed lambda calculus
  -- let's have some types, and a function to compare types, ok?

  data Type : Set where
    ⋆   : Type {- *mumble* we don't really care what our atomic type is -}
    _⇒_ : Type → Type → Type

  -- and something to check when types are equal

  _==_ : Type → Type → Bool
  ⋆       == ⋆       = true
  ⋆       == (C ⇒ D) = false
  (A ⇒ B) == ⋆       = false
  (A ⇒ B) == (C ⇒ D) = A == C ∧ B == D

  -- in coq, you'd use this function and then prove

  ==⟶≡ : ∀ A B → A == B ≡ true → A ≡ B
  ==⟶≡ ⋆         ⋆         p = refl
  ==⟶≡ ⋆         (B₁ ⇒ B₂) ()
  ==⟶≡ (A₁ ⇒ A₂) ⋆         ()
  ==⟶≡ (A₁ ⇒ A₂) (B₁ ⇒ B₂) p =
    -- ∧-split : ∀{b₁ b₂} → b₁ ∧ b₂ ≡ true → b₁ ≡ true × b₂ ≡ true
    case ∧-split p of λ{
      (p₁ , p₂) → cong₂ _⇒_ (==⟶≡ A₁ B₁ p₁) (==⟶≡ A₂ B₂ p₂) }

  -- and that way, you'd know your boolean function wasn't doing
  -- something incredibly stupid...
  -- like mine was, just now when I wrote these slides...

  -- anyway, anyone notice anything similar between _==_ and ==⟶≡?



module agda-style-1 where

  open coq-style-1 public using (Type; ⋆; _⇒_)


{-------------------------------------------------------------------------}
  -- hah, I tricked all of you!
  -- this lecture is about cultural differences between agda and coq...

  -- this is how you encode negation, "if you give me something of
  -- that type, I'll give you something which lives in the empty type"

  ¬_ : Set → Set
  ¬ P = P → 𝟎

  data Dec (P : Set) : Set where
    yes : ( p :   P) → Dec P
    no  : (¬p : ¬ P) → Dec P

  -- watch out, when we start writing this function, some scary things
  -- will start appearing -- keep in mind what it's all about:
  --
  --   a pattern match reveals information,
  --   and we don't want to just callously throw that away

  {-+}
  _≟_ : (A B : Type) → Dec (A ≡ B)
  A ≟ B = ?
  {+-}

  -- right, so we can _actually_ compare types now








module coq-style-2 where

  open coq-style-1 public using (Type; ⋆; _⇒_)
  open import Agda.Builtin.Nat using (_==_)


{-------------------------------------------------------------------------}
  -- I didn't lie, we're going to talk about the lambda calculus

  Id : Set
  Id = ℕ

  infixr 10 λ[_∶_]_
  infixl 20 _∙_

  data Term : Set where
    # : Id → Term
    λ[_∶_]_ : Id → Type → Term → Term
    _∙_ : Term → Term → Term

  -- let's look at some sample programs

  I = λ[ 0 ∶ ⋆ ] # 0
  K = λ[ 0 ∶ ⋆ ] λ[ 1 ∶ ⋆ ] # 0
  W = λ[ 0 ∶ ⋆ ] # 5

  -- right, we also need junk like substitution, reductions, etc...
  -- let's ignore that -- we don't have forever -- let's look at typing












{-------------------------------------------------------------------------}
  -- if we wanna look at typing, though, we have to basically redo
  -- the Maps stuff from the homework

  Ctxt : Set
  Ctxt = Id → Maybe Type

  ∅ : Ctxt
  ∅ = λ _ → nothing

  _,_∶_ : Ctxt → Id → Type → Ctxt
  (Γ , x ∶ A) y =
    -- warning, cheats: that _==_ has type ℕ → ℕ → Bool
    if x == y then just A else Γ y

  _∶_∈_ : Id → Type → Ctxt → Set
  x ∶ A ∈ Γ = Γ x ≡ just A

  -- fine, that looks about right, we can worry about theorems later

  -- by which I mean not at all
















  infix 15 _,_∶_ _∶_∈_
  infix 5 _⊢_∶_ _⊢_

{-------------------------------------------------------------------------}
  -- now, TYPING!

  data _⊢_∶_ (Γ : Ctxt) : Term → Type → Set where

    Ax  : ∀ {x A} →

      x ∶ A ∈ Γ →
      ----------- (Ax)
      Γ ⊢ # x ∶ A

    ⇒I : ∀ {x N A B} →

      Γ , x ∶ A ⊢ N ∶ B →
      ------------------------ (⇒I)
      Γ ⊢ λ[ x ∶ A ] N ∶ A ⇒ B

    ⇒E : ∀ {L M A B} →

      Γ ⊢ L ∶ A ⇒ B → Γ ⊢ M ∶ A →
      -------------------------- (⇒E)
      Γ ⊢ L ∙ M ∶ B

  -- this predicate is actually doing two things at the same time
  -- let's make that a little bit clearer









{-------------------------------------------------------------------------}
  -- this predicate is actually doing two things at the same time
  -- let's make that a little bit clearer

  -- let's remove as much of the type clutter as we can... easily

  _∈_ : Id → Ctxt → Set
  x ∈ Γ = Γ x ≢ nothing

  data _⊢_ (Γ : Ctxt) : Term → Set where

    Ax? : ∀ {x} →

      x ∈ Γ →
      ------- (Ax?)
      Γ ⊢ # x

    ⇒I? : ∀ {x N A} →

      Γ , x ∶ A ⊢ N →
      ---------------- (⇒I?)
      Γ ⊢ λ[ x ∶ A ] N

    ⇒E? : ∀ {L M} →

      Γ ⊢ L → Γ ⊢ M →
      --------------- (⇒E?)
      Γ ⊢ L ∙ M

  -- what predicate did we just encode? (albeit clumsily)







module agda-style-2 where

  open agda-style-1

{-------------------------------------------------------------------------}
  -- how can we clean up this predicate? what if we could prove that the
  -- type for variables had exactly n elements, and Γ provided a type for
  -- each of them?

  -- what does the type with exactly n elements look like?
  --
  --   * 0 lives in all types with at least 1 element
  --
  --   * if n lives in the type with m elements,
  --     then n + 1 lives in the type with m + 1 elements
  --

  data Fin : ℕ → Set where
    zero : {n : ℕ} → Fin (suc n)
    suc  : {n : ℕ} → Fin n → Fin (suc n)

  f3of6 : Fin 6
  f3of6 = suc (suc (suc (zero {n = 2})))

  f3of7 : Fin 7
  f3of7 = suc (suc (suc (zero {n = 3})))

  -- and now?












-- here be cheats: if we want to be able to use natural number
-- notation for finite types, then we better have some constraints
open import Data.Fin using (Fin; suc; zero; fromℕ≤)

instance
  FinNumber : ∀ {n} → Number (Fin n)
  FinNumber {n} = record
    { Constraint = λ{m → True (suc m ≤? n)}
    ; fromNat    = λ{m {{p}} → fromℕ≤ (toWitness p)}
    }

module agda-style-3 where

  open agda-style-1

{-------------------------------------------------------------------------}
  -- and now?
  -- we encode terms, with only a finite number of possibilities for vars

  data Term (n : ℕ) : Set where
    #     : Fin n → Term n
    λ[_]_ : Type → Term (suc n) → Term n
    _∙_   : Term n → Term n → Term n

  -- oh, I forgot to tell you, we can write 0, 1, 2... for Fin too,
  -- as long as agda can figure out the upper bound
  f5in7 : Fin 7
  f5in7 = 5 {- there is some secret magic involved, though -}

  -- anyway, this is the identity function
  I : Term 0
  I = λ[ ⋆ ] # 0
  --  ^        |
  --  \________/
  --
  --  ^^^^^^^^^^
  -- this is how binding works in de Bruijn notation

  -- once more
  K : Term 0
  K = λ[ ⋆ ] λ[ ⋆ ] # 1
  --  ^               |
  --  \_______________/

  -- this term still exists, but now mentions that it exists _in context_
  W : Term 1
  W = {- some stuff is expected here -} λ[ ⋆ ] # 1
  --                 ^                           |
  --                 \___________________________/
  --
  -- we wrote # 5 last time, but those were names, these are indices
  -- so the index # 1 is just as good as the name # 5 or # 1203
  -- the only point is that it should move out of scope











module agda-style-4 where

  open agda-style-1

{-------------------------------------------------------------------------}
  -- right, so now we have well-scoped terms...
  -- why not restrict it to well-scoped, well-typed terms?

  data Vec (A : Set) : ℕ → Set where
    []  : Vec A 0
    _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

  _‼_ : ∀ {n} {A} → Vec A n → Fin n → A
  (x ∷ _ ) ‼ zero  = x
  (_ ∷ xs) ‼ suc i = xs ‼ i

  Ctxt : ℕ → Set
  Ctxt n = Vec Type n

  data _⊢_ {n : ℕ} : Ctxt n → Type → Set where

    # : {Γ : Ctxt n} (x : Fin n) →

      ----------- (Ax)
      Γ ⊢ (Γ ‼ x)

    λ[_]_ : {Γ : Ctxt n} (A : Type) {B : Type} →

      A ∷ Γ ⊢ B →
      ----------- (⇒I)
      Γ ⊢ A ⇒ B

    _∙_ : {Γ : Ctxt n} {A B : Type} →

      Γ ⊢ A ⇒ B → Γ ⊢ A →
      ------------------- (⇒E)
      Γ ⊢ B

  -- now we cannot ever write ill-typed terms

  I : {A : Type} → [] ⊢ A ⇒ A
  I {A} = λ[ A ] # 0

  K : {A B : Type} → [] ⊢ A ⇒ (B ⇒ A)
  K {A} {B} = λ[ A ] λ[ B ] # 1








  infix 5 _⊢_

{-------------------------------------------------------------------------}
  -- is this fun? I don't know

  -- anyway, we (probably) don't have time to talk about reduction
  -- but what's the moral of the story?

  -- we have been systematically been pushing effort that we'd have
  -- to expend proving things into things that agda knows, simply
  -- because of the representation that we're using

  -- in that vein, one last trick, mock reduction:

  ⟦_⟧ : Type → Set
  ⟦ ⋆     ⟧ = ℕ -- why not?
  ⟦ A ⇒ B ⟧ = ⟦ A ⟧ → ⟦ B ⟧

  data Env⟦_⟧ : {n : ℕ} → Vec Type n → Set where
    []  : Env⟦ [] ⟧
    _∷_ : ∀ {n} {A : Type} {Γ : Vec Type n} →
          ⟦ A ⟧ → Env⟦ Γ ⟧ → Env⟦ A ∷ Γ ⟧

  lookup : ∀ {n} {Γ : Ctxt n} (x : Fin n) → Env⟦ Γ ⟧ → ⟦ Γ ‼ x ⟧
  lookup zero    (x ∷ _) = x
  lookup (suc i) (_ ∷ e) = lookup i e

  ⟪_⟫ : ∀ {n} {Γ : Ctxt n} {A : Type} →
        Γ ⊢ A → Env⟦ Γ ⟧ → ⟦ A ⟧
  ⟪ # x      ⟫ e = lookup x e
  ⟪ λ[ A ] M ⟫ e = λ x → ⟪ M ⟫ (x ∷ e)
  ⟪ M ∙ N    ⟫ e = ⟪ M ⟫ e (⟪ N ⟫ e)

  id : ℕ → ℕ
  id = ⟪ I ⟫ []

  test-id : id ≡ λ x → x
  test-id = refl

  const : ℕ → ℕ → ℕ
  const = ⟪ K ⟫ []

  test-const : const ≡ λ x y → x
  test-const = refl






-- -}