Slides and tutorial for my guest lectures on Agda at the University of Edinburgh in 2017.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-(- 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 = ? | |
{+-} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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