Algebraic Ornaments!

reornament.idr

module reornament

-- Idris translation of Agda code:
-- https://gist.github.com/gallais/e507832abc6c91ac7cb9

-- Which follows Conor McBride's Ornaments paper:
-- https://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/Ornament.pdf

ListAlg : Type -> Type -> Type
ListAlg A B = (B, A -> B -> B)

data ListSpec : (A : Type) -> {B : Type} -> ListAlg A B -> B -> Type where
  Nil : {A, B : Type} -> {alg : ListAlg A B} -> ListSpec A alg (fst alg)
  (::) : {A, B : Type} -> (a : A) -> {b : B} -> (as : ListSpec A alg b) -> ListSpec A alg (snd alg a b)

AlgLength : {A : Type} -> ListAlg A Nat
AlgLength = (0, (\_ => succ))

AlgSum : ListAlg Nat Nat
AlgSum = (0, (+))

Algx : {A, B, C : Type} -> (algB : ListAlg A B) -> (algC : ListAlg A C) ->
       ListAlg A (B, C)
Algx (b, sucB) (c, sucC) = ((b, c), (\a => \(b, c) => (sucB a b, sucC a c)))

Vec : (A : Type) -> (n : Nat) -> Type
Vec A n = ListSpec A AlgLength n


allFin4 : Vec Nat 4
allFin4 = [0, 1, 2, 3]

Distribution : Type
Distribution = ListSpec Nat AlgSum 100

uniform : Distribution
uniform = [25, 25, 25, 25]

SizedDistribution : Nat -> Type
SizedDistribution n = ListSpec Nat (Algx AlgLength AlgSum) (n, 100)

uniform4 : SizedDistribution 4
uniform4 = [25, 25, 25, 25]