Skip to content

Instantly share code, notes, and snippets.

@wenkokke

wenkokke/lecture1.agda

Last active May 25, 2019
Embed
What would you like to do?
Slides and tutorial for my guest lectures on Agda at the University of Edinburgh in 2017.
{-(- 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 = ?
{+-}
{-# 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
-- -}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment