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