{-# OPTIONS --copatterns #-} module AdvancedFunctionalProgramming where data ⊤ : Set where it : ⊤ data _⊎_ (A B : Set) : Set where inl : A → A ⊎ B inr : B → A ⊎ B ⊎-elim : (A B C : Set) → A ⊎ B → (A → C) → (B → C) → C ⊎-elim A B C (inl x) f g = f x ⊎-elim A B C (inr x) f g = g x data Σ_,_ (A : Set) (P : A → Set) : Set where _,_ : (x : A) → P x → Σ A , P _×_ : Set → Set → Set A × B = Σ A , (λ x → B) proj₁ : (A : Set) → (P : A → Set) → Σ A , P → A proj₁ A P (fst , snd) = fst proj₂ : (A : Set) → (P : A → Set) → (σ : Σ A , P) → P (proj₁ A P σ) proj₂ A P (fst , snd) = snd data ⊥ : Set where ⊥-elim : (A : Set) → ⊥ → A ⊥-elim A () oops : {A : Set} → A oops {A} = {!!} proof-of-false : ⊥ proof-of-false = oops data _≡_ {A : Set} (x : A) : A → Set where refl : x ≡ x 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 prf₂ = prf₂ subst : {A : Set} {x y : A} {P : A → Set} → x ≡ y → P x → P y subst refl px = px cong : {A B : Set} {x y : A} (f : A → B) → x ≡ y → f x ≡ f y cong f refl = refl data ℕ : Set where zero : ℕ succ : ℕ → ℕ _+_ : ℕ → ℕ → ℕ zero + n = n succ m + n = succ (m + n) zero-+-identity₁ : (m : ℕ) → (zero + m) ≡ m zero-+-identity₁ m = refl zero-+-identity₂ : (m : ℕ) → (m + zero) ≡ m zero-+-identity₂ zero = refl zero-+-identity₂ (succ m) = cong succ (zero-+-identity₂ m) succ-+ : (m n : ℕ) → (m + succ n) ≡ succ (m + n) succ-+ zero n = refl succ-+ (succ m) n = cong succ (succ-+ m n) Commutative : (A : Set) → (A → A → A) → Set Commutative A op = (x y : A) → op x y ≡ op y x +-symm : Commutative ℕ _+_ +-symm zero n = sym (zero-+-identity₂ n) +-symm (succ m) n = trans (cong succ (+-symm m n)) (sym (succ-+ n m)) -- trans (cong succ (+-symm m n)) (sym (succ-+ n m)) -- Proof by transitivity: -- -- succ (m + n) -- ≡ -- succ (n + m) -- ≡ -- n + succ m QED data List (A : Set) : Set where ε : List A _▹_ : A → List A → List A length : ∀ {A} → List A → ℕ length ε = zero length (x ▹ xs) = succ (length xs) hd : ∀ {A} → List A → A hd ε = {!!} -- ??? hd (x ▹ xs) = x data Vec (A : Set) : ℕ → Set where [] : Vec A zero _∷_ : ∀ {m} → A → Vec A m → Vec A (succ m) head : ∀ {A m} → Vec A (succ m) → A head (x ∷ xs) = x tail : ∀ {A m} → Vec A (succ m) → Vec A m tail (x ∷ xs) = xs map : ∀ {A B m} → (A → B) → Vec A m → Vec B m map f [] = [] map f (x ∷ xs) = (f x) ∷ (map f xs) zip : ∀ {A B m} → Vec A m → Vec B m → Vec (A × B) m zip [] ys = [] zip (x ∷ xs) (y ∷ ys) = (x , y) ∷ zip xs ys record PartialOrder : Set₁ where field Carrier : Set _≼_ : Carrier → Carrier → Set reflexive : ∀ x → x ≼ x antisymmetric : ∀ x y → x ≼ y → y ≼ x → x ≡ y transitive : ∀ x y z → x ≼ y → y ≼ z → x ≼ z data _≤_ : ℕ → ℕ → Set where ≤-zero : (m : ℕ) → zero ≤ m ≤-succ : (m n : ℕ) → m ≤ n → succ m ≤ succ n ℕ-partialOrder : PartialOrder ℕ-partialOrder = record { Carrier = ℕ ; _≼_ = _≤_ ; reflexive = ≤-reflexive ; antisymmetric = ≤-antisymmetric ; transitive = ≤-transitive } where ≤-reflexive : ∀ m → m ≤ m ≤-reflexive zero = ≤-zero zero ≤-reflexive (succ m) = ≤-succ m m (≤-reflexive m) ≤-antisymmetric : (m n : ℕ) → m ≤ n → n ≤ m → m ≡ n ≤-antisymmetric .zero .zero (≤-zero .zero) (≤-zero .zero) = refl ≤-antisymmetric .(succ m) .(succ n) (≤-succ m n prf₁) (≤-succ .n .m prf₂) = cong succ (≤-antisymmetric m n prf₁ prf₂) ≤-transitive : (m n o : ℕ) → m ≤ n → n ≤ o → m ≤ o ≤-transitive .zero .zero o (≤-zero .zero) (≤-zero .o) = ≤-zero o ≤-transitive .zero .(succ m) .(succ n) (≤-zero .(succ m)) (≤-succ m n prf₂) = ≤-zero (succ n) ≤-transitive .(succ m) .(succ n) .(succ n₁) (≤-succ m n prf₁) (≤-succ .n n₁ prf₂) = ≤-succ m n₁ (≤-transitive m n n₁ prf₁ prf₂) _⁻¹ : PartialOrder → PartialOrder p ⁻¹ = record { Carrier = PartialOrder.Carrier p ; _≼_ = λ x y → PartialOrder._≼_ p y x ; reflexive = PartialOrder.reflexive p ; antisymmetric = λ x y z z₁ → PartialOrder.antisymmetric p x y z₁ z ; transitive = λ x y z z₁ z₂ → PartialOrder.transitive p z y x z₂ z₁ } record Monad : Set₁ where field M : Set → Set return : ∀ {A} → A → M A _>>=_ : ∀ {A B} → M A → (A → M B) → M B return-bind₁ : ∀ {A B} {f : A → M B} {x : A} → ((return x) >>= f) ≡ (f x) return-bind₂ : ∀ {A} {x : M A} → (x >>= return) ≡ x bind-associative : ∀ {A B C} {x : M A} {f : A → M B} {g : B → M C} → (x >>= (λ y → (f y >>= g))) ≡ ((x >>= f) >>= g) module AssumingMonad (MD : Monad) where open Monad MD public mapM : ∀ {A B} → (A → M B) → List A → M (List B) mapM f ε = return ε mapM f (x ▹ xs) = f x >>= (λ h → mapM f xs >>= (λ t → return (h ▹ t))) data Maybe (A : Set) : Set where none : Maybe A some : A → Maybe A maybeMonad : Monad maybeMonad = record { M = Maybe ; return = some ; _>>=_ = bind ; return-bind₁ = λ {A} {B} {f} {x} → refl ; return-bind₂ = λ {A} {x} → lemma₀ x ; bind-associative = λ {A} {B} {C} {x} → lemma₁ x } where bind : ∀ {A B} → Maybe A → (A → Maybe B) → Maybe B bind none f = none bind (some x) f = f x lemma₀ : ∀ {A} (m : Maybe A) → bind m some ≡ m lemma₀ none = refl lemma₀ (some x) = refl lemma₁ : {A B C : Set} (m : Maybe A) {f : A → Maybe B} {g : B → Maybe C} → bind m (λ y → bind (f y) g) ≡ bind (bind m f) g lemma₁ none = λ {f} {g} → refl lemma₁ (some x) = λ {f} {g} → refl module X = AssumingMonad maybeMonad test₀ : _ test₀ = X.mapM some (succ zero ▹ (succ (succ (succ zero)) ▹ (zero ▹ (succ zero ▹ ε)))) -- Mega advanced material record Stream (A : Set) : Set where coinductive field first : A rest : Stream A open Stream public zeros : Stream ℕ first zeros = zero rest zeros = zeros ones : Stream ℕ first ones = succ zero rest ones = ones combine : ∀ {A B} → Stream A → Stream B → Stream (A × B) first (combine xs ys) = first xs , first ys rest (combine xs ys) = combine (rest xs) (rest ys) take : ∀ {A} → (m : ℕ) → Stream A → Vec A m take zero ss = [] take (succ m) ss = first ss ∷ take m (rest ss) record _≅_ {A : Set} (xs ys : Stream A) : Set where coinductive field ≡-first : first xs ≡ first ys ≅-rest : rest xs ≅ rest ys open _≅_ public mutual interleave : ∀ {A} → Stream A → Stream A → Stream A first (interleave xs ys) = first xs rest (interleave xs ys) = interleave′ (rest xs) (rest ys) interleave′ : ∀ {A} → Stream A → Stream A → Stream A first (interleave′ xs ys) = first ys rest (interleave′ xs ys) = interleave (rest xs) (rest ys) mutual interleave-ones : interleave ones ones ≅ ones ≡-first interleave-ones = refl ≅-rest interleave-ones = interleave′-ones interleave′-ones : interleave′ ones ones ≅ ones ≡-first interleave′-ones = refl ≅-rest interleave′-ones = interleave-ones -- Giga advanced material record DecidablePartialOrder : Set₁ where field partialOrder : PartialOrder open PartialOrder partialOrder public field decidable : ∀ x y → (x ≼ y) ⊎ (y ≼ x) module AssumingPartialOrder (P : DecidablePartialOrder) where open DecidablePartialOrder P mutual data SortedVec : ℕ → Set where ⟨⟩ : SortedVec zero _∷_⟨_⟩ : ∀ {m} → (x : Carrier) → (xs : SortedVec m) → xs is-dominated-by x → SortedVec (succ m) _is-dominated-by_ : ∀ {m} → SortedVec m → Carrier → Set ⟨⟩ is-dominated-by x = ⊤ (y ∷ ys ⟨ prf ⟩) is-dominated-by x with DecidablePartialOrder.decidable P x y ... | inl q = ⊥ ... | inr q = ys is-dominated-by x ℕ-decidablePartialOrder : DecidablePartialOrder ℕ-decidablePartialOrder = record { partialOrder = ℕ-partialOrder ; decidable = ≤-decidable } where ≤-decidable : ∀ m n → (m ≤ n) ⊎ (n ≤ m) ≤-decidable m n = {!!} open AssumingPartialOrder ℕ-decidablePartialOrder test₁ : SortedVec (succ (succ zero)) test₁ = succ (succ (succ (succ zero))) ∷ succ zero ∷ ⟨⟩ ⟨ {!!} ⟩ ⟨ {!!} ⟩ test₂ : SortedVec (succ (succ zero)) test₂ = zero ∷ succ (succ (succ (succ zero))) ∷ ⟨⟩ ⟨ {!!} ⟩ ⟨ {!!} ⟩ -- Impossible, unless Agda is inconsistent...