open import Level open import Relation.Binary.PropositionalEquality open ≡-Reasoning open import list open import basic open import nat open import laws module delta where data Delta {l : Level} (A : Set l) : (Nat -> (Set l)) where mono : A -> Delta A (S O) delta : {n : Nat} -> A -> Delta A (S n) -> Delta A (S (S n)) deltaAppend : {l : Level} {A : Set l} {n m : Nat} -> Delta A (S n) -> Delta A (S m) -> Delta A ((S n) + (S m)) deltaAppend (mono x) d = delta x d deltaAppend (delta x d) ds = delta x (deltaAppend d ds) headDelta : {l : Level} {A : Set l} {n : Nat} -> Delta A (S n) -> A headDelta (mono x) = x headDelta (delta x _) = x tailDelta : {l : Level} {A : Set l} {n : Nat} -> Delta A (S (S n)) -> Delta A (S n) tailDelta (delta _ d) = d -- Functor delta-fmap : {l : Level} {A B : Set l} {n : Nat} -> (A -> B) -> (Delta A (S n)) -> (Delta B (S n)) delta-fmap f (mono x) = mono (f x) delta-fmap f (delta x d) = delta (f x) (delta-fmap f d) -- Monad (Category) delta-eta : {l : Level} {A : Set l} {n : Nat} -> A -> Delta A (S n) delta-eta {n = O} x = mono x delta-eta {n = (S n)} x = delta x (delta-eta {n = n} x) delta-mu : {l : Level} {A : Set l} {n : Nat} -> (Delta (Delta A (S n)) (S n)) -> Delta A (S n) delta-mu (mono x) = x delta-mu (delta x d) = delta (headDelta x) (delta-mu (delta-fmap tailDelta d)) delta-bind : {l : Level} {A B : Set l} {n : Nat} -> (Delta A (S n)) -> (A -> Delta B (S n)) -> Delta B (S n) delta-bind d f = delta-mu (delta-fmap f d) {- -- Monad (Haskell) delta-return : {l : Level} {A : Set l} -> A -> Delta A (S O) delta-return = delta-eta _>>=_ : {l : Level} {A B : Set l} {n : Nat} -> (x : Delta A n) -> (f : A -> (Delta B n)) -> (Delta B n) d >>= f = delta-bind d f -}