module Live where data Nat : Set where z : Nat s : Nat → Nat _+_ : Nat → Nat → Nat z + n = n s m + n = s (m + n) {-# BUILTIN NATURAL Nat #-} {-# BUILTIN ZERO z #-} {-# BUILTIN SUC s #-} _*_ : Nat → Nat → Nat z * n = z s m * n = n + (m * n) data Bool : Set where tt : Bool ff : Bool _==_ : Nat → Nat → Bool z == z = tt z == s n = ff s m == z = ff s m == s n = m == n -- Pairs record _×_ (A B : Set) : Set where -- constructor _,_ field fst : A snd : B open _×_ -- if we want to define the constructor by hand _,_ : {A B : Set} → A → B → A × B a , b = record{fst = a;snd = b} curry : {A B C : Set} → (A × B → C) → A → B → C curry f a b = f (a , b) uncurry : {A B C : Set} → (A → B → C) → A × B → C uncurry f p = f (fst p) (snd p) papp : {A B C D : Set} → ((A → B) × (C → D)) → (A × C) → (B × D) papp p q = fst p (fst q) , snd p (snd q) -- Lists data List (X : Set) : Set where [] : List X _::_ : X → List X → List X -- asside on parameters and indices data List' : Set → Set1 where [] : ∀{X} → List' X _::_ : ∀{X} → X → List' X → List' X _++_ : ∀{X} → List X → List X → List X [] ++ vs' = vs' (v :: vs) ++ vs' = v :: (vs ++ vs') zip : ∀{A B} → List A → List B → List (A × B) zip [] bs = [] zip as [] = [] zip (a :: as) (b :: bs) = (a , b) :: zip as bs unzip : ∀{A B} → List (A × B) → List A × List B unzip [] = [] , [] --unzip (p :: ps) = (fst p :: fst (unzip ps)) , (snd p :: snd (unzip ps)) {- unzip (p :: ps) = let x = unzip ps in (fst p :: fst x) , (snd p :: snd x) -} unzip (p :: ps) = (fst p :: fst x) , (snd p :: snd x) where x = unzip ps -- Wednesday head : ∀{X} → List X → X head [] = {!!} head (x :: xs) = x data Maybe (A : Set) : Set where Just : A → Maybe A Nothing : Maybe A -- safe head mhead : ∀{X} → List X → Maybe X mhead [] = Nothing mhead (x :: xs) = Just x -- safe tail mtail : ∀{X} → List X → Maybe (List X) mtail [] = Nothing mtail (x :: xs) = Just xs mreturn : ∀{X} → X → Maybe X mreturn = Just mbind : ∀{X Y} → (X → Maybe Y) → Maybe X → Maybe Y mbind f (Just x) = f x mbind f Nothing = Nothing mjoin : ∀{X} → Maybe (Maybe X) → Maybe X mjoin (Just mx) = mx mjoin Nothing = Nothing -- Vectors data Vec (X : Set) : Nat → Set where [] : Vec X z _::_ : ∀{n} → X → Vec X n → Vec X (s n) vhead : ∀{X n} → Vec X (s n) → X vhead (x :: xs) = x vtail : ∀{X n} → Vec X (s n) → Vec X n vtail (x :: xs) = xs vec2List : ∀{X n} → Vec X n → List X vec2List [] = [] vec2List (x :: xs) = x :: (vec2List xs) length : ∀{X} → List X → Nat length [] = z length (x :: xs) = s (length xs) list2Vec : ∀{X}(xs : List X) → Vec X (length xs) list2Vec [] = [] list2Vec (x :: xs) = x :: list2Vec xs test1 : List Nat test1 = 1 :: (2 :: (3 :: (4 :: (5 :: [])))) lookup : ∀{X} → Nat → List X → Maybe X lookup n [] = Nothing lookup z (x :: xs) = Just x lookup (s n) (x :: xs) = lookup n xs data Fin : Nat → Set where fz : ∀ {n} → Fin (s n) fs : ∀{n} → Fin n → Fin (s n) vlookup : ∀{X n}(i : Fin n) → Vec X n → X vlookup fz (x :: xs) = x vlookup (fs i) (x :: xs) = vlookup i xs -- Thursday -- The empty type and pattern matching data False : Set where weird : {X : Set} → False → X weird ()