Skip to content

Instantly share code, notes, and snippets.

@josh-hs-ko

josh-hs-ko/FLOLAC18.agda

Last active July 23, 2018 03:59
Show Gist options
  • Save josh-hs-ko/3a0ea16a225ca4efbd01428c06b8fdba to your computer and use it in GitHub Desktop.
Save josh-hs-ko/3a0ea16a225ca4efbd01428c06b8fdba to your computer and use it in GitHub Desktop.
Download ZIP
Raw
FLOLAC18.agda
-- programming
data Nat : Set where
zero : Nat
suc : Nat → Nat
_+_ : Nat → Nat → Nat
zero + n = n
suc m + n = suc (m + n)
data List (A : Set) : Set where
[] : List A
_∷_ : A → List A → List A
sum : List Nat → Nat
sum [] = zero
sum (x ∷ xs) = x + sum xs
map : {A B : Set} → (A → B) → List A → List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs
-- proving
rapp : {A B : Set} → A → (A → B) → B
rapp x f = f x
data _∧_ (A B : Set) : Set where
_,_ : A → B → A ∧ B
data _∨_ (A B : Set) : Set where
left : A → A ∨ B
right : B → A ∨ B
distr : {A B C : Set} → A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C)
distr (x , left y) = left (x , y)
distr (x , right z) = right (x , z)
data ⊥ : Set where
⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()
¬_ : Set → Set
¬ A = A → ⊥
ex1 : {A : Set} → ¬ ¬ (¬ ¬ A → A)
ex1 x = x (λ y → ⊥-elim (y (λ z → x (λ _ → z))))
ex2 : {A B C : Set} → ¬ ¬ (A ∨ B) → (¬ ¬ A → ¬ ¬ C) → (¬ ¬ B → ¬ ¬ C) → ¬ ¬ C
ex2 x y z w = x (λ { (left u) → y (λ z₁ → z₁ u) w; (right v) → z (λ z₁ → z₁ v) w })
-- equality
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
pm : (suc zero + suc zero) ≡ suc (suc zero)
pm = refl
arith-contradiction : ¬ (zero ≡ suc zero)
arith-contradiction ()
sym : {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl
trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl eq = eq
cong : {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
cong f refl = refl
_∘_ : {A B C : Set} → (B → C) → (A → B) → (A → C)
(f ∘ g) x = f (g x)
map-functorial : {A B C : Set} (f : B → C) (g : A → B) → (xs : List A) → map (f ∘ g) xs ≡ map f (map g xs)
map-functorial f g [] = refl
map-functorial f g (x ∷ xs) = cong (f (g x) ∷_) (map-functorial f g xs)
-- equational reasoning
_≡[_]_ : {A : Set} (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
x ≡[ eq ] eq' = trans eq eq'
_∎ : {A : Set} (x : A) → x ≡ x
x ∎ = refl
infixr 1 _≡[_]_
infix 2 _∎
map-functorial' : {A B C : Set} (f : B → C) (g : A → B) → (xs : List A) → map (f ∘ g) xs ≡ map f (map g xs)
map-functorial' f g [] =
map (f ∘ g) []
≡[ refl ]
[]
≡[ refl ]
map f []
≡[ refl ]
map f (map g [])
∎
map-functorial' f g (x ∷ xs) =
map (f ∘ g) (x ∷ xs)
≡[ refl ]
(f ∘ g) x ∷ map (f ∘ g) xs
≡[ refl ]
f (g x) ∷ map (f ∘ g) xs
≡[ cong (f (g x) ∷_) (map-functorial' f g xs) ]
f (g x) ∷ map f (map g xs)
≡[ refl ]
map f (g x ∷ map g xs)
≡[ refl ]
map f (map g (x ∷ xs))
∎
-- indexed datatypes
{-# BUILTIN NATURAL Nat #-}
data Vec (A : Set) : Nat → Set where
[] : Vec A 0
_∷_ : A → {n : Nat} → Vec A n → Vec A (suc n)
vec3 : Vec Nat 3
vec3 = 0 ∷ (1 ∷ (2 ∷ []))
_++_ : {A : Set} {m n : Nat} → Vec A m → Vec A n → Vec A (m + n)
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
data SumList : Nat → Set where
[] : SumList 0
_∷_ : (m : Nat) {n : Nat} → SumList n → SumList (m + n)
slist15 : SumList 15
slist15 = 3 ∷ (9 ∷ (2 ∷ (1 ∷ (0 ∷ []))))
expand : {n : Nat} → SumList n → Vec Nat n
expand [] = []
expand (x ∷ xs) = aux x ++ expand xs
where
aux : (y : Nat) → Vec Nat y
aux zero = []
aux (suc y) = y ∷ aux y
-- metamorphisms (0.625₁₀ = 0.101₂)
-- coinductive lists
mutual
record CoList (B : Set) : Set where
coinductive
field
decon : CoListF B
data CoListF (B : Set) : Set where
[] : CoListF B
_∷_ : B → CoList B → CoListF B
downFrom : Nat → CoList Nat
CoList.decon (downFrom zero ) = []
CoList.decon (downFrom (suc n)) = n ∷ downFrom n
upFrom : Nat → CoList Nat
CoList.decon (upFrom n) = n ∷ upFrom (suc n)
take : {B : Set} → Nat → CoList B → List B
take zero xs = []
take (suc n) xs with CoList.decon xs
take (suc n) xs | [] = []
take (suc n) xs | b ∷ xs' = b ∷ take n xs'
data Maybe (A : Set) : Set where
nothing : Maybe A
just : A → Maybe A
unfoldr : {B S : Set} (g : S → Maybe (B ∧ S)) → S → CoList B
CoList.decon (unfoldr g s) with g s
CoList.decon (unfoldr g s) | nothing = []
CoList.decon (unfoldr g s) | just (b , s') = b ∷ unfoldr g s'
downFrom' : Nat → CoList Nat
downFrom' = unfoldr (λ { zero → nothing; (suc n) → just (n , n) })
upFrom' : Nat → CoList Nat
upFrom' = unfoldr (λ n → just (n , suc n))
-- foldl as foldr
foldr : {A S : Set} → (A → S → S) → S → List A → S
foldr f e [] = e
foldr f e (x ∷ xs) = f x (foldr f e xs)
foldl : {A S : Set} → (S → A → S) → S → List A → S
foldl f e [] = e
foldl f e (x ∷ xs) = foldl f (f e x) xs
flip : {A B C : Set} → (A → B → C) → (B → A → C)
flip f y x = f x y
fromLeftAlg : {A S : Set} → (S → A → S) → (A → (S → S) → (S → S))
fromLeftAlg f a t = t ∘ flip f a
id : {A : Set} → A → A
id x = x
foldl-as-foldr : {A S : Set} {f : S → A → S} {e : S} (xs : List A) → foldl f e xs ≡ foldr (fromLeftAlg f) id xs e
foldl-as-foldr [] = refl
foldl-as-foldr (x ∷ xs) = foldl-as-foldr xs
-- algebraic and coalgebraic lists
data AlgList (A : Set) {S : Set} (f : A → S → S) (e : S) : S → Set where
[] : AlgList A f e e
_∷_ : (a : A) → {s : S} → AlgList A f e s → AlgList A f e (f a s)
vec3' : AlgList Nat (λ _ n → suc n) 0 3
vec3' = 0 ∷ (1 ∷ (2 ∷ []))
slist15' : AlgList Nat _+_ 0 15
slist15' = 3 ∷ (9 ∷ (2 ∷ (1 ∷ (0 ∷ []))))
mutual
record CoalgList (B : Set) {S : Set} (g : S → Maybe (B ∧ S)) (s : S) : Set where
coinductive
field
decon : CoalgListF B g s
data CoalgListF (B : Set) {S : Set} (g : S → Maybe (B ∧ S)) : S → Set where
⟨_⟩ : {s : S} → g s ≡ nothing → CoalgListF B g s
_∷⟨_⟩_ : (b : B) → {s s' : S} → g s ≡ just (b , s') → CoalgList B g s' → CoalgListF B g s
open CoalgList
single : CoalgList Nat (λ { zero → nothing; (suc n) → just (n , n) }) 1
CoalgList.decon single = 0 ∷⟨ refl ⟩ none
where
none : CoalgList Nat _ 0
CoalgList.decon none = ⟨ refl ⟩
-- metamorphic algorithms
data Inspect {A B : Set} (f : A → B) (x : A) (y : B) : Set where
[[_]] : f x ≡ y → Inspect f x y
inspect : {A B : Set} (f : A → B) (x : A) → Inspect f x (f x)
inspect f x = [[ refl ]]
module _ {A B S : Set} (f : S → A → S) (g : S → Maybe (B ∧ S)) where
meta : {h : S → S} → AlgList A (fromLeftAlg f) id h → (s : S) → CoalgList B g (h s)
decon (meta [] s) with g s | inspect g s
decon (meta [] s) | nothing | [[ eq ]] = ⟨ eq ⟩
decon (meta [] s) | just (b , s') | [[ eq ]] = b ∷⟨ eq ⟩ meta [] s'
decon (meta (a ∷ as) s) = decon (meta as (f s a))
module _ {A B S : Set} (f : S → A → S) (g : S → Maybe (B ∧ S))
(streaming-condition : {a : A} {b : B} {s s' : S} → g s ≡ just (b , s') → g (f s a) ≡ just (b , f s' a)) where
lemma : {s : S} {b : B} {s' : S} {h : S → S} →
AlgList A (fromLeftAlg f) id h →
g s ≡ just (b , s') → g (h s) ≡ just (b , h s')
lemma [] eq = eq
lemma (a ∷ as) eq = lemma as (streaming-condition eq)
stream : {h : S → S} → AlgList A (fromLeftAlg f) id h → (s : S) → CoalgList B g (h s)
decon (stream as s) with g s | inspect g s
decon (stream [] s) | nothing | [[ eq ]] = ⟨ eq ⟩
decon (stream (a ∷ as) s) | nothing | [[ eq ]] = decon (stream as (f s a))
decon (stream as s) | just (b , s') | [[ eq ]] = b ∷⟨ lemma as eq ⟩ stream as s'
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment