freesemiring.idr

data Mu : (pattern : Type -> Type) -> Type where
    In : {f: Type -> Type} -> f (Mu f) -> Mu f

data TwoOps x a = Val x | Addunit | Mulunit | Add a a | Mul a a

Functor (TwoOps x) where
  map f (Val y) = Val y
  map f (Addunit) = Addunit
  map f (Mulunit) = Mulunit
  map f (Add a1 a2) = Add (f a1) (f a2)
  map f (Mul a1 a2) = Mul (f a1) (f a2)
  
Freesemiring : Type -> Type
Freesemiring x = Mu (TwoOps x)

Algebra : (Type -> Type) -> Type -> Type  
Algebra f a = f a -> a

 --universal property of the initial algebra
cata : Functor f => Algebra f a -> Mu f -> a
cata alg (In op) = alg (map (cata alg) op)


nats : Algebra (TwoOps Nat) Nat
nats (Val x) = x
nats (Addunit) = 0
nats (Mulunit) = 1
nats ((Add x y)) = x + y
nats ((Mul x y)) = x * y

cata' : Algebra (TwoOps a) a -> Algebra Freesemiring a 
cata' = cata

-- use the universal property to freely extend nats
freenats = cata' nats

--min plus semiring

trop : Algebra (TwoOps (Maybe Double)) (Maybe Double)
trop (Val x) = x
trop Addunit = Nothing
trop Mulunit = Just 0
trop (Add Nothing y) = y 
trop (Add x Nothing) = x 
trop (Add (Just x) (Just y)) = Just (min x y)
trop (Mul Nothing y) = Nothing 
trop (Mul x Nothing) = Nothing 
trop (Mul (Just x) (Just y)) = Just (x + y)

-- the free extension
freetrop = cata' trop

data Fin : Nat -> Type where
  Zero : Fin (S n)
  Suc : (i : Fin n) -> Fin (S n)

-- the 2-rig of types
Tworig : Algebra (TwoOps Type) Type
Tworig (Val a) = a
Tworig Addunit = Void
Tworig Mulunit = Fin 1
Tworig (Add a b) = Either a b
Tworig (Mul a b) = (a,b)

--and its free extension
freetypes= cata' Tworig

--example
term : Freesemiring Type
term = In $ Mul (In (Val (Fin 4))) (In Addunit)
bigtype = freetypes term

-- did i just write a types compiler?