Algebraic Ornaments!

reornament.agda

module reornament where

open import Data.Product
open import Data.Nat
open import Data.List

ListAlg : (A B : Set) → Set
ListAlg A B = B × (A → B → B)

data ListSpec (A : Set) {B : Set} (alg : ListAlg A B) : (b : B) → Set where
  nil  :  ListSpec A alg (proj₁ alg)
  cons : (a : A) {b : B} (as : ListSpec A alg b) → ListSpec A alg (proj₂ alg a b)

AlgLength : {A : Set} → ListAlg A ℕ
AlgLength = 0 , (λ _ → suc)

AlgSum : ListAlg ℕ ℕ
AlgSum = 0 , _+_

Alg× : {A B C : Set} (algB : ListAlg A B) (algC : ListAlg A C) →
       ListAlg A (B × C)
Alg× (b , sucB) (c , sucC) = (b , c) , (λ a → λ { (b , c) → sucB a b , sucC a c })

Vec : (A : Set) (n : ℕ) → Set
Vec A n = ListSpec A AlgLength n


allFin4 : Vec ℕ 4
allFin4 = cons 0 (cons 1 (cons 2 (cons 3 nil)))

Distribution : Set
Distribution = ListSpec ℕ AlgSum 100

uniform : Distribution
uniform = cons 25 (cons 25 (cons 25 (cons 25 nil)))

SizedDistribution : ℕ → Set
SizedDistribution n = ListSpec ℕ (Alg× AlgLength AlgSum) (n , 100)

uniform4 : SizedDistribution 4
uniform4 = cons 25 (cons 25 (cons 25 (cons 25 nil)))