---
title: "SU-CS242 NOV192024"
source: https://www.jemoka.com/posts/kbhsu_cs242_nov192024/
date: 2024-11-19
---

Agda A whirlwind tour through Agda
Agda whitespace rules Agda allows UNICODE! IN! VARIABLES! so:
i:Int is! not! i : Int
the first thing is an indentifier of type i:Int the second thing is an i of type Int Dependent Type Theories with Agda booleans Consider two empty declarations:
data False : Set where this is a type with nothing in it!
record True : Set where this is a type with exactly one thing in it!
False has no elements in it, and True has exactly one element in it.
trivial : True trivial = _ since True only takes on one type, Agda can figure out the wild-card value is unique
isTrue : Bool -&gt; Set isTrue true = True isTrue false = False we have now created True/False AS TYPES. We just mapped values to types.
less than _&lt;_ : Nat -&gt; Nat -&gt; Bool and now consider:
_ &lt; zero = false zero &lt; succ n = true succ m &lt; succ n = m &lt; n length of list length : { A : Set } -&gt; List A -&gt; Nat length [] = zero length (x :: xs) = succ (length xs) safe! list lookup we leverage the fact that False -&gt; A has no candidates.
lookup : {A : Set}(xs : List A)(n : Nat) -&gt; isTrue (n &lt; length xs) -&gt; A lookup [] n () lookup (x :: xs) zero p = x lookup (x :: xs) (succ n) p = lookup xs n p where () is a the &ldquo;absurd pattern&rdquo;, and this can&rsquo;t execute.
and p is a proof that we show to Agda that (n &lt; length xs).
standard datatypes Set is the type of all small types (level 0 types in).
bool data Bool : Set where false : Bool true : Bool not: Bool -&gt; Bool not false = true not true = false numbers data Nat : Set where zero : Nat succ : Nat -&gt; Nat plus : Nat -&gt; Nat -&gt; Nat plus zero m = m plus (succ n) m = succ (plus n m) notice that succ in this case is a function because in a Dependent Type Theories our data type can return other stuff.
Some rules about pattern matching&hellip;.
patterns must be exaustive (every case must be covered) patterns must be disjoint &mdash; they cannot overlap in what they match (i.e. other languages have some matching order) infix operators _op_ is the way that infix operators are defined, so:
_+_ : Nat -&gt; Nat -&gt; Nat zero + m = m succ n + m = succ (n + m) also that underscores represents where arguments can go, so if, then, else can be written as if_then_else_
List data List (A : Set) : Set where [] : List A _::_ : A -&gt; List A -&gt; List A indexed type data Eq {A : Set} (x : A) : A -&gt; Set where refl : Eq x x this is an indexed type, meaning the type of the data type is a function from A to a type in Set.
This means that there is a different type for every value of x.
example proof
we want to prove &ldquo;if m = n, then f m = f n&rdquo;
cong : {A : set} {B : set} {m : A} {n : A} (f: A -&gt; B) -&gt; Eq m n -&gt; Eq (f m) (f n) cong f refl = refl the key note that the left refl has a type Eq m n, the right refl is implicitly defined through considering Eq
let + where trip : Nat -&gt; Nat trip n = let double = n + n triple = n + double in triple lambda addZero : Nat -&gt; Nat addZero n = (\x -&gt; x + zero) n polymorphic types identity : (A : Set) -&gt; A -&gt; A identity A x = x and now you can make identity things such as:
zero&#39; : Nat zero&#39; = identity Nat zero you will note that the polymorphism is explicitly instantiated (type inference is not figured out for you, you said A is of a particular argument explicitly).
polymorphic types, implicitly obviously Agda can guess what the types of things are. So:
identity : {A : Set} -&gt; A -&gt; A identity x = x and then you can write:
zero &#39;&#39; : Nat zero&#39;&#39; = identity Zero you will note that subsequent type instantiation is now implicit.
records record Position : Set where field xc : Nat yc : Nat you can create instances of this record
pos : Position pos = record { xc = zero; yc = succ(zero) } along with the record constructor, you get selectors for each field (Position.xc etc&hellip;) defined for you:
myxc : Position -&gt; Nat myxc p = Position.xc p myyc : Position -&gt; Nat myyc p = Position.yc p our record constructors could have parameters, so:
record Position : Set (A : Set) (B : Set) where field xc : A yc : B and then you can create constructors with annotated types
pos : Position Nat Nat pos = record { xc = zero; yc = succ(zero) }
