[[
wikihub
]]
Search
⌘K
Explore
People
For Agents
Sign in
Explore
People
For Agents
Sign in
@jemoka / Jemoka Knowledge Base / raw/course/cs242/kbhsu_cs242_nov192024.md
Suggest edit
Cancel
Submit suggestion
Title
Name
Note
--- 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 -> Set isTrue true = True isTrue false = False we have now created True/False AS TYPES. We just mapped values to types. less than _<_ : Nat -> Nat -> Bool and now consider: _ < zero = false zero < succ n = true succ m < succ n = m < n length of list length : { A : Set } -> List A -> Nat length [] = zero length (x :: xs) = succ (length xs) safe! list lookup we leverage the fact that False -> A has no candidates. lookup : {A : Set}(xs : List A)(n : Nat) -> isTrue (n < length xs) -> A lookup [] n () lookup (x :: xs) zero p = x lookup (x :: xs) (succ n) p = lookup xs n p where () is a the “absurd pattern”, and this can’t execute. and p is a proof that we show to Agda that (n < 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 -> Bool not false = true not true = false numbers data Nat : Set where zero : Nat succ : Nat -> Nat plus : Nat -> Nat -> 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…. patterns must be exaustive (every case must be covered) patterns must be disjoint — 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 -> Nat -> 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 -> List A -> List A indexed type data Eq {A : Set} (x : A) : A -> 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 “if m = n, then f m = f n” cong : {A : set} {B : set} {m : A} {n : A} (f: A -> B) -> Eq m n -> 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 -> Nat trip n = let double = n + n triple = n + double in triple lambda addZero : Nat -> Nat addZero n = (\x -> x + zero) n polymorphic types identity : (A : Set) -> A -> A identity A x = x and now you can make identity things such as: zero' : Nat zero' = 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} -> A -> A identity x = x and then you can write: zero '' : Nat zero'' = 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…) defined for you: myxc : Position -> Nat myxc p = Position.xc p myyc : Position -> 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) }