Skip to content

Instantly share code, notes, and snippets.

@wenkokke

wenkokke/lecture1.agda

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