id x = x
first f (x,y) = (f x, y)
map f [] = []
map f (x:xs) = f x : map f xs
flip f x y = f y x
fst (x,y) = x
snd (x,y) = y

kind List a = Nil | Cons a (List a)


data Id x = Id x

{- (built-in)
data Equal a b where
  Eq :: Equal a a -}

data IndId :: *0 ~> *0 ~> *0 ~> *0 where
  IndId :: x -> IndId s s x
-- equivalently data IndId s s' x = IndId (Equal s s') x

data CoIndId s s' x = CoIndId (Equal s s' -> x)


data NatT f g = NatT (forall x. f x -> g x)
data GraT c d = GraT (forall x y. c x y -> d x y)
data IndT m n = IndT (forall s1 s2 a. m s1 s2 a -> n s1 s2 a)

data Compose f g x = Compose (f (g x))
data GCompose g h x z = forall y. GCompose (g x y) (h y z)
data ICompose m n s1 s3 x = forall s2. ICompose (m s1 s2 (n s2 s3 x))
data CoICompose m n s1 s3 x = CoICompose (forall s2. (m s1 s2 (n s2 s3 x)))

data Dual c a b = Dual (c b a)




kind MCategory k = MCat (k ~> k ~> *0) k (k ~> k ~> k)

type Hask      = MCat (->) () (,)          -- :: MCategory (*0)
type EndHask   = MCat NatT Id Compose      -- :: MCategory (*0 ~> *0)
type Graph     = MCat GraT Equal GCompose  -- :: MCategory (*0 ~> *0 ~> *0)
type Indexed   = MCat IndT IndId ICompose  -- :: MCategory (*0 ~> *0 ~> *0 ~> *0)
type CoEndHask = MCat (Dual NatT) Id Compose
type CoIndexed = MCat (Dual IndT) CoIndId CoICompose


data Monoid :: forall (k :: *1). MCategory k ~> k ~> *0 where
  M :: forall (k :: *1) (m :: k) (mor :: k ~> k ~> *0) (unit :: k) (prod :: k ~> k ~> k).
          mor unit m -> mor (prod m m) m ->
          Monoid (MCat mor unit prod) m


-- Monoid
sumMonoid :: Monoid Hask Int
sumMonoid = M (\() -> 0) (\(x,y) -> x+y)

-- Monad
maybeMonad :: Monoid EndHask Maybe
maybeMonad = M (NatT (\(Id x) -> Just x)) (NatT join)
  where join (Compose (Just (Just x))) = Just x
        join _ = Nothing

-- Category
haskCat :: Monoid Graph (->)                  -- instance Category (->)
haskCat = M (GraT ident) (GraT compose)
  where ident :: Equal a b -> a -> b     -- Type signature needed (else Equal a b -> c -> c)
        ident Eq x = x
        compose (GCompose g h) = h . g

discCat :: Monoid Graph Equal
discCat = M (GraT id) (GraT compose)
  where compose :: GCompose Equal Equal a b -> Equal a b
        compose (GCompose Eq Eq) = Eq

-- Comonad
data Env s a = Env s a

envComonad :: Monoid CoEndHask (Env s)  -- instance Comonad (Env s)
envComonad = M extract duplicate
  where extract :: Dual NatT Id (Env s)
        extract = Dual (NatT (\(Env s a) -> Id a))

        duplicate :: Dual NatT (Compose (Env s) (Env s)) (Env s)
        duplicate = Dual (NatT (\(Env s a) -> Compose (Env s (Env s a))))

data Store s a = Store (s -> a) s

storeComonad :: Monoid CoEndHask (Store s)  -- instance Comonad (Store s)
storeComonad = M extract duplicate
  where extract :: Dual NatT Id (Store s)
        extract = Dual (NatT (\(Store f x) -> Id (f x)))

        duplicate :: Dual NatT (Compose (Store s) (Store s)) (Store s)
        duplicate = Dual (NatT (\(Store f x) -> Compose (Store (Store f) x)))

-- Indexed monad
data IxState s1 s2 a = IxState (s1 -> (a, s2))
runIxState (IxState x) = x

ixstate :: Monoid Indexed IxState
ixstate = M (IndT ret) (IndT join)
  where ret :: IndId s s' x -> IxState s s' x
        ret (IndId x) = IxState (\s -> (x,s))
        join :: ICompose IxState IxState s s' x -> IxState s s' x
        join (ICompose x) = IxState (\s -> let (y, s') = runIxState x s
                                           in runIxState y s')

-- Indexed comonad
data IxStore s t a = IxStore (t -> a) s

ixstore :: Monoid CoIndexed IxStore
ixstore = M extract duplicate
  where extract :: Dual IndT CoIndId IxStore
        extract = Dual (IndT (\x -> CoIndId (k x)))

        duplicate :: Dual IndT (CoICompose IxStore IxStore) IxStore
        duplicate = Dual (IndT (\(IxStore f x) ->
          CoICompose (IxStore (IxStore f) x)))

        k :: IxStore s t a -> Equal s t -> a    -- Needs type signature.
        k (IxStore f a) Eq = f a

-- Auxiliary

getNatT (NatT x) = x
getDual (Dual x) = x
getIndT (IndT x) = x
fromId (Id x) = x
fromCompose (Compose x) = x
fromCoIndId (CoIndId x) = x Eq
fromCoICompose (CoICompose x) = x

------
-- Some functions operating on monoids
------

-- Dual monoid
dualmon :: Monoid Hask c -> Monoid Hask c
dualmon (M unit prod) = M unit (\(x,y) -> prod (y,x))

-- Dual category
dualcat :: Monoid Graph c -> Monoid Graph (Dual c)
dualcat (M (GraT ident) (GraT compose)) = M (GraT (dualid ident)) (GraT (dualcmp compose))
  where 
    dualid :: (forall x1 y1. Equal x1 y1 -> c x1 y1) ->
                Equal x y -> Dual c x y
    dualid ident Eq = Dual (ident Eq)

    dualcmp :: (forall x1 y1. GCompose c c x1 y1 -> c x1 y1) ->
                GCompose (Dual c) (Dual c) x y -> Dual c x y
    dualcmp compose (GCompose (Dual f) (Dual g)) = Dual (compose (GCompose g f))

-- Product monoid
prodmon :: Monoid Hask m -> Monoid Hask n -> Monoid Hask (m,n)
prodmon (M unit1 mult1) (M unit2 mult2) =
  M (\() -> (unit1 (), unit2 ()))
    (\((a,b),(a',b')) -> (mult1 (a,a'), mult2 (b,b')))

-- Product category
data CatProd c d x y = CatProd (c x y) (d x y)
prodcat :: Monoid Graph c -> Monoid Graph d -> Monoid Graph (CatProd c d)
prodcat (M id1 comp1) 
        (M id2 comp2) = M (GraT (u id1 id2)) (GraT (v comp1 comp2))
  where u :: GraT Equal c -> GraT Equal d -> Equal a b -> CatProd c d a b
        u (GraT i1) (GraT i2) Eq = CatProd (i1 Eq) (i2 Eq)

        v :: GraT (GCompose c c) c -> GraT (GCompose d d) d ->
              GCompose (CatProd c d) (CatProd c d) a b -> CatProd c d a b
        v (GraT comp1) (GraT comp2) (GCompose (CatProd c1 d1) (CatProd c2 d2)) =
           CatProd (comp1 (GCompose c1 c2)) (comp2 (GCompose d1 d2))

-- Writer
data Writer m a = Writer m a

writer :: Monoid Hask m -> Monoid EndHask (Writer m)
writer (M unit mult) = M (NatT ret) (NatT join)
  where ret (Id a) = Writer (unit ()) a
        join (Compose (Writer x (Writer y z))) = Writer (mult (x,y)) z

-- Indexed writer
data IxWriter c x y a = IxWriter (c x y) a

ixwriter :: Monoid Graph c -> Monoid Indexed (IxWriter c)
ixwriter (M id comp) = M (IndT (ret id)) (IndT (join comp))
  where ret :: GraT Equal c -> IndId u v a -> IxWriter c u v a
        ret (GraT i) (IndId a) = IxWriter (i Eq) a

        join :: GraT (GCompose c c) c -> ICompose (IxWriter c) (IxWriter c) x y a -> IxWriter c x y a
        join (GraT c) (ICompose (IxWriter f (IxWriter g x))) = IxWriter (c (GCompose f g)) x



-------------------------------------------------------------------------------
-- Endomorphisms
-------------------------------------------------------------------------------

-- Endomorphisms of a category form a monoid
end :: Monoid Graph m -> Monoid Hask (m x x)
end (M (GraT ident) (GraT compose)) =
   M (\() -> ident Eq)
     (\(x,y) -> compose (GCompose x y))

-- Endomorphisms of an indexed monad form a monad
end' :: Monoid Indexed m -> Monoid EndHask (m x x)
end' (M (IndT ident) (IndT compose)) =
   M (NatT (ident . IndId . fromId))
     (NatT (compose . ICompose . fromCompose))

-- Endomorphisms of an indexed comonad form a comonad
end'' :: Monoid CoIndexed m -> Monoid CoEndHask (m x x)
end'' (M (Dual (IndT extract)) (Dual (IndT duplicate))) =
  M (Dual (NatT (Id . fromCoIndId . extract)))
    (Dual (NatT (Compose . fromCoICompose . duplicate)))



data Category :: forall (k :: *1). MCategory k ~> (*0 ~> *0 ~> k) ~> *0 where
  C :: forall (k :: *1) (c :: *0 ~> *0 ~> k) mor unit prod.
        (forall x. mor unit (c x x)) ->
        (forall x y z. mor (prod (c x y) (c y z)) (c x z)) ->
            Category (MCat mor unit prod) c

iso1 :: Monoid Graph c -> Category Hask c
iso1 (M (GraT i) (GraT c)) = C (\() -> i Eq) (\(f,g) -> c (GCompose f g))

iso1' :: Category Hask c -> Monoid Graph c
iso1' (C i c) = M (GraT (v i)) (GraT (\(GCompose u v) -> c (u,v)))
  where v :: (() -> c a a) -> Equal a b -> c a b
        v f Eq = f ()

iso2 :: Monoid Indexed c -> Category EndHask c
iso2 (M (IndT i) c) = C (NatT (\(Id x) -> i (IndId x))) (NatT (k c))
  where k :: IndT (ICompose c c) c -> Compose (c x y) (c y z) a -> c x z a
        k (IndT f) (Compose x) = f (ICompose x)

iso2' :: Category EndHask c -> Monoid Indexed c
iso2' (C i c) = M (IndT (u i)) (IndT (v c))
  where u :: NatT Id (c x x) -> IndId x y a -> c x y a 
        u (NatT f) (IndId x) = f (Id x)

        v :: (forall y. NatT (Compose (c x y) (c y z)) (c x z)) -> ICompose c c x z a -> c x z a
        v f (ICompose x) = w f x

        w :: NatT (Compose (c x y) (c y z)) (c x z) -> c x y (c y z a) -> c x z a
        w (NatT f) x = f (Compose x)


iso3 :: Monoid CoIndexed m -> Category CoEndHask m
iso3 (M (Dual (IndT i)) (Dual (IndT c))) =
  C (Dual (NatT (Id . fromCoIndId . i))) (Dual (NatT (Compose . fromCoICompose . c)))

iso3' :: Category CoEndHask m -> Monoid CoIndexed m
iso3' (C i c) = M (f4 i) (fun c)

  where fun :: (forall x y z. Dual NatT (Compose (m x y) (m y z)) (m x z)) -> Dual IndT (CoICompose m m) m
        fun c = Dual (IndT (\x -> CoICompose (fromCompose (getNatT (getDual c) x))))

        f1 :: (forall x a. (m x x a -> Id a)) -> m u v b -> Equal u v -> b
        f1 m x Eq = fromId (m x)

        f2 :: (forall x a. (m x x a -> Id a)) -> m u v b -> CoIndId u v b
        f2 m x = CoIndId (f1 m x)
        
        f3 :: (forall x. NatT (m x x) Id) -> m u v b -> CoIndId u v b
        f3 m = f2 (getNatT m)
        
        f4 :: (forall x. Dual NatT Id (m x x)) -> Dual IndT CoIndId m
        f4 x = Dual (IndT (f3 (getDual x)))

endGen :: Category k c -> Monoid k (c x x)
endGen (C x y) = M x y


graph :: MCategory k ~> MCategory (*0 ~> *0 ~> k)
{graph Hask} = Graph
{graph EndHask} = Indexed
{graph CoEndHask} = CoIndexed

-- Isomorphisms between Monoid {graph k} c and Category k c

data Token :: k ~> *0 where
  Token :: forall (k :: *1) (a :: k). Token a

endiso :: Token k -> (Monoid {graph k} c -> Category k c, Category k c -> Monoid {graph k} c)
endiso (Token :: Token Hask) = (iso1, iso1')
endiso (Token :: Token EndHask) = (iso2, iso2')
endiso (Token :: Token CoEndHask) = (iso3, iso3')

-------------------------------------------------------------------------------
-- Inherent data
-------------------------------------------------------------------------------
data MonoidHom m n = MonoidHom (m -> n)
type Monoids = MCat MonoidHom () (,)


data Functor f = Functor (forall x y. (x -> y) -> f x -> f y)

composeFunctor :: Functor f -> Functor g -> Functor (Compose f g)
composeFunctor (Functor f) (Functor g) = Functor (lift . f . g)
  where lift k (Compose x) = Compose (k x)

data IxFunctor f = IxFunctor (forall a b x y. (x -> y) -> f a b x -> f a b y)

composeIxFunctor :: IxFunctor f -> IxFunctor g -> IxFunctor (ICompose f g)
composeIxFunctor (IxFunctor f) (IxFunctor g) = IxFunctor (lift . f . g)
  where lift k (ICompose x) = ICompose (k x)

composeCIxFunctor :: IxFunctor f -> IxFunctor g -> IxFunctor (CoICompose f g)
composeCIxFunctor (IxFunctor f) (IxFunctor g) = IxFunctor (\k (CoICompose x) -> CoICompose (f (g k) x))

deFunctor (Functor x) = x
deIxFunctor (IxFunctor w) = w

inh :: forall (k :: *1). MCategory k ~> k ~> *0
{inh Hask m} = ()
{inh EndHask f} = Functor f
{inh CoEndHask f} = Functor f
{inh Graph g} = ()
{inh Indexed f} = IxFunctor f
{inh CoIndexed f} = IxFunctor f
{inh Ab g} = Group g
{inh Monoids m} = Monoid Hask m
{inh (VSpaces k) v} = VSpace k v

emptyProd :: () -> () -> ()
emptyProd _ _ = ()

getprod :: forall (k :: *1). MCategory k ~> k ~> k ~> k
{getprod (MCat mor un pro) a b} = pro a b

getunit :: forall (k :: *1). MCategory k ~> k
{getunit (MCat mor un pro)} = un

getmor :: forall (k :: *1). MCategory k ~> k ~> k ~> *0
{getmor (MCat mor un pro) a b} = mor a b




data Monoid2 :: forall (k :: *1). MCategory k ~> k ~> *0 where
  M2 :: forall (k :: *1) (m :: k) mor unit prod.
          {inh (MCat mor unit prod) m} ->
          mor unit m -> mor (prod m m) m ->
          Monoid2 (MCat mor unit prod) m

intRing2 :: Monoid2 Ab Int
intRing2 = M2 intGroup (powr intGroup 1) (bilin intGroup (*))

maybeMonad2 :: Monoid2 EndHask Maybe
maybeMonad2 = M2 (Functor fmap) (NatT (\(Id x) -> Just x)) (NatT join)
  where fmap f (Just x) = Just (f x)
        fmap _ _ = Nothing

        join (Compose (Just (Just x))) = Just x
        join _ = Nothing

ixstate2 :: Monoid2 Indexed IxState
ixstate2 = M2 (IxFunctor map) (IndT ret) (IndT join)
  where ret :: IndId s s' x -> IxState s s' x
        ret (IndId x) = IxState (\s -> (x,s))
        join (ICompose x) = IxState (\s -> let (y, s') = runIxState x s
                                           in runIxState y s')

        map f x = IxState (\s -> let (y, s') = runIxState x s in (f y, s'))

data IxCont s1 s2 a = IxCont ((a -> s2) -> s1)
runIxCont (IxCont x) = x

ixcont2 :: Monoid2 Indexed IxCont
ixcont2 = M2 (IxFunctor map) (IndT ret) (IndT join)
  where ret :: IndId s s' x -> IxCont s s' x
        ret (IndId x) = IxCont (\f -> f x)
        join (ICompose x) = IxCont (\c -> runIxCont x (\a -> runIxCont a c))
        map f x = IxCont $ (flip (.) . flip (.)) f $ runIxCont x

sumCMonoid :: Monoid2 Monoids Int
sumCMonoid = M2 intM (MonoidHom zero) (MonoidHom mult)
  where intM :: Monoid Hask Int
        intM = M zero mult

        mult (x,y) = x + y
        zero () = 0

-------------------------------------------------------------------------------
-- Utility functions for Monoid2
-------------------------------------------------------------------------------
writer2 :: Monoid2 Hask m -> Monoid2 EndHask (Writer m)
writer2 (M2 () unit mult) = M2 (Functor map) (NatT ret) (NatT join)
  where ret (Id a) = Writer (unit ()) a
        join (Compose (Writer x (Writer y z))) = Writer (mult (x,y)) z
        map f (Writer m x) = Writer m (f x)

ixwriter2 :: Monoid2 Graph c -> Monoid2 Indexed (IxWriter c)
ixwriter2 (M2 () id comp) = M2 (IxFunctor map) (IndT (ret id)) (IndT (join comp))
  where ret :: GraT Equal c -> IndId u v a -> IxWriter c u v a
        ret (GraT i) (IndId a) = IxWriter (i Eq) a

        join :: GraT (GCompose c c) c -> ICompose (IxWriter c) (IxWriter c) x y a -> IxWriter c x y a
        join (GraT c) (ICompose (IxWriter f (IxWriter g x))) = IxWriter (c (GCompose f g)) x

        map f (IxWriter m x) = IxWriter m (f x)

data Kleisli m a b = Kleisli (a -> m b)

kleisli :: Monoid2 EndHask m -> Monoid2 Graph (Kleisli m)
kleisli (M2 fmap (NatT r) (NatT j)) =
  M2 () (GraT (kleiid r)) (GraT (kleicmp fmap j))

  where kleiid :: (forall x. Id x -> m x) -> Equal a b -> Kleisli m a b
        kleiid r Eq = Kleisli (r . Id)

        kleicmp ::
           Functor m ->
           (forall x. Compose m m x -> m x) ->
           GCompose (Kleisli m) (Kleisli m) x y -> Kleisli m x y
        kleicmp (Functor fmap) j (GCompose (Kleisli f) (Kleisli g)) = Kleisli (j . Compose . fmap g . f)


data Cont r a = Cont ((a -> r) -> r)

univ_monad :: Monoid2 EndHask m -> m a -> Cont (m b) a
univ_monad (M2 fmap _ join) x =
  Cont (\f -> getNatT join (Compose (deFunctor fmap f x)))

univ_imonad :: Monoid2 Indexed m -> m u v a -> IxCont (m u w b) (m v w b) a
univ_imonad (M2 fmap _ join) x =
  IxCont (\f -> getIndT join (ICompose (deIxFunctor fmap f x)))

univ_comonad :: Monoid2 CoEndHask w -> Store (w a) b -> w b
univ_comonad (M2 fmap _ duplicate) (Store f x) =
  deFunctor fmap f (fromCompose (getNatT (getDual duplicate) x))

-- univ_monad   :: NatT m (Cont (m b))
-- univ_comonad :: NatT (Store (w a)) w
-- univ_imonad :: m s1 s2 a -> IxCont (m s1) (m s2) a?

data Fix f = Fix (f (Fix f))

fold :: Functor f -> (f a -> a) -> Fix f -> a
fold (Functor fmap) f (Fix x) = f (fmap (fold (Functor fmap) f) x)

fold' :: Functor f -> Fix f -> Cont a (f a)
fold' fun x = Cont (\c -> fold fun c x)

unfold :: Functor f -> (a -> f a) -> a -> Fix f
unfold (Functor fmap) f x = Fix (fmap (unfold (Functor fmap) f) (f x))

unfold' :: Functor f -> Store a (f a) -> Fix f
unfold' fun (Store u v) = unfold fun u v

data IFix f x z = forall y. IFix (f x z (IFix f z y))

ifold :: IxFunctor f -> (forall x y. f x y a -> a) -> IFix f u v -> a
ifold _ = undefined -- ??

-------------------------------------------------------------------------------
-- Rings
-------------------------------------------------------------------------------

data Group g = Group (g -> g -> g) g (g -> g)
data GroupHom g h = GroupHom (g -> h)

intGroup :: Group Int
intGroup = Group (+) 0 negate

powr :: Group g -> g -> GroupHom Int g
powr (Group m u i) g = GroupHom pow
  where pow 0 = u
        pow n | n < 0 = i (pow (-n))
        pow n = m g (pow (n-1))


data Tensor g h = Tensor [(g,h)]

tensor :: Group g -> Group h -> Group (Tensor g h)
tensor (Group _ _ i) _ = Group (\(Tensor a) (Tensor b) -> Tensor (a ++ b))
                               (Tensor [])
                               (\(Tensor a) -> Tensor (map (first i) a))

gsum :: Group g -> [g] -> g
gsum (Group m u i) (x:xs) = m x (gsum (Group m u i) xs)
gsum (Group _ u _) [] = u

bilin :: Group r -> (g -> h -> r) -> GroupHom (Tensor g h) r
bilin g f = GroupHom (\(Tensor xs) -> gsum g (map (\(a,b) -> f a b) xs))

type Ab = MCat GroupHom Int Tensor

-- The Z2 ring
boolRing :: Monoid Ab Bool
boolRing = M (powr boolG True) (bilin boolG (&&))
  where boolG :: Group Bool
        boolG = Group xor False not

        xor False False = False
        xor True True = False
        xor _ _ = True

intRing :: Monoid Ab Int
intRing = M (powr intGroup 1) (bilin intGroup (*))

ringadd :: Monoid Ab v -> v -> v -> v
ringadd (M (GroupHom unit) (GroupHom mult)) x y =
  mult (Tensor [(x, unit 1), (y, unit 1)])

-------------------------------------------------------------------------------
-- Vector spaces and algebras
-------------------------------------------------------------------------------

data Linear v w = Linear (v -> w)
type VSpaces k = MCat Linear k Tensor

data VSpace k v = VSpace (Group v) (k -> v -> v)

tensorSpace :: VSpace k v -> VSpace k w -> VSpace k (Tensor v w)
tensorSpace (VSpace g1 m1) (VSpace g2 m2) = VSpace (tensor g1 g2)
  (\x (Tensor a) -> Tensor (map (first (m1 x)) a))


data Complex = Complex Float Float

complGroup :: Group Complex
complGroup = Group cadd czero cneg
  where cadd (Complex r1 i1) (Complex r2 i2) = Complex (r1 #+ r2) (i1 #+ i2)
        cneg (Complex r i) = Complex (negateFloat r) (negateFloat i)
        czero = Complex 0.0 0.0

complexVS :: VSpace Float Complex
complexVS = VSpace complGroup vmult
  where vmult a (Complex r i) = Complex (a #* r) (a #* i)

complexAlgebra :: Monoid2 (VSpaces Float) Complex
complexAlgebra = M2 complexVS (Linear un) (Linear mult)
  where un x = Complex x 0.0

        mult :: Tensor Complex Complex -> Complex
        mult (Tensor xs) = gsum complGroup (map cmult xs)
        cmult (Complex r1 i1, Complex r2 i2) =
          Complex (r1#*r2#-i1#*i2) (r1#*i2#+r2#*i1)


-------------------------------------------------------------------------------
-- Testing laws
-------------------------------------------------------------------------------

isomor :: forall (k :: *1). MCategory k ~> k ~> k ~> *0
{isomor (MCat mor un pro) a b} = (mor a b, mor b a)

inhsq :: forall (a :: *1) (b :: MCategory a) (c :: a).
       Token b -> {inh b c} -> {inh b {getprod b c c}}

inhsq c a = inhprod c a a

--inhprod' :: forall (a :: *1) (b :: MCategory a) (c :: a).  Token b -> {inh b c} -> {inh b {getprod b c c}}
inhprod' :: Token (MCat mor unit prod) -> {inh (MCat mor unit prod) m} -> {inh (MCat mor unit prod) (prod m m)}
inhprod' (Token :: Token Hask) x = inhprod (Token :: Token Hask) x x
--inhprod' _ = undefined --inhsq
--ll c a = inhprod c a a

inhunit' :: forall (k :: *1) mor unit prod. Token (MCat mor unit prod) -> {inh (MCat mor unit prod) unit}
inhunit' = inhunit


--laws :: Monoid2 c m -> {getmor c {getprod c {getprod c m m} m} {getprod c m m}}
morid :: forall (k :: *1) (c :: MCategory k) (x :: k). Token c ->
  {getmor c x x}
morid (Token :: Token Hask)        = id
morid (Token :: Token EndHask)     = NatT id
morid (Token :: Token CoEndHask)   = Dual (NatT id)
morid (Token :: Token Graph)       = GraT id
morid (Token :: Token Indexed)     = IndT id
morid (Token :: Token CoIndexed)   = Dual (IndT id)
morid (Token :: Token Ab)          = GroupHom id
morid (Token :: Token Monoids)     = MonoidHom id
morid (Token :: Token (VSpaces k)) = Linear id


morcomp :: forall (k :: *1) (c :: MCategory k) (x :: k) (y :: k) (z :: k).
  Token c -> {getmor c y z} -> {getmor c x y} -> {getmor c x z}
morcomp (Token :: Token Hask)      = (.)
morcomp (Token :: Token EndHask)   = comp
  where comp (NatT f) (NatT g) = NatT (f . g) -- Somehow this has to be
                                              -- separated
morcomp (Token :: Token CoEndHask) = comp
  where comp (Dual (NatT f)) (Dual (NatT g)) = Dual (NatT (g . f))
        -- Notice inversion

morcomp (Token :: Token Graph)     = comp
  where comp (GraT f) (GraT g) = GraT (f . g)

morcomp (Token :: Token Indexed)   = comp
  where comp (IndT f) (IndT g) = IndT (f . g)

morcomp (Token :: Token CoIndexed) = comp
  where comp (Dual (IndT f)) (Dual (IndT g)) = Dual (IndT (g . f))

morcomp (Token :: Token Ab)        = comp
  where comp (GroupHom f) (GroupHom g) = GroupHom (f . g)

morcomp (Token :: Token Monoids)   = comp
  where comp (MonoidHom f) (MonoidHom g) = MonoidHom (f . g)

morcomp (Token :: Token (VSpaces k)) = comp
  where comp (Linear f) (Linear g) = Linear (f . g)

inhprod :: forall (k :: *1) (c :: MCategory k) (x :: k) (y :: k).
  Token c -> {inh c x} -> {inh c y} -> {inh c {getprod c x y}}
inhprod (Token :: Token Hask)        = emptyProd
inhprod (Token :: Token EndHask)     = composeFunctor
inhprod (Token :: Token CoEndHask)   = composeFunctor
inhprod (Token :: Token Graph)       = emptyProd
inhprod (Token :: Token Indexed)     = composeIxFunctor
inhprod (Token :: Token CoIndexed)   = composeCIxFunctor
inhprod (Token :: Token Ab)          = tensor
inhprod (Token :: Token Monoids)     = prodmon
inhprod (Token :: Token (VSpaces k)) = tensorSpace

idFunctor :: Functor Id
idFunctor = Functor (\f (Id x) -> Id (f x))

idIxFunctor :: IxFunctor IndId
idIxFunctor = IxFunctor k
  where k :: (a -> b) -> IndId s s' a -> IndId s s' b -- Needed
        k f (IndId x) = IndId (f x)

idCIxFunctor :: IxFunctor CoIndId
idCIxFunctor = IxFunctor k
  where -- k :: (a -> b) -> CoIndId s s' a -> CoIndId s s' b -- Not needed
        k f (CoIndId x) = CoIndId (f . x)

inhunit :: forall (k :: *1) (c :: MCategory k). Token c -> {inh c {getunit c}}
inhunit (Token :: Token Hask)        = ()
inhunit (Token :: Token EndHask)     = idFunctor
inhunit (Token :: Token CoEndHask)   = idFunctor
inhunit (Token :: Token Graph)       = ()
inhunit (Token :: Token Indexed)     = idIxFunctor
inhunit (Token :: Token CoIndexed)   = idCIxFunctor
inhunit (Token :: Token Ab)          = intGroup
inhunit (Token :: Token Monoids)     = M (\() -> ()) (\((),()) -> ())
inhunit (Token :: Token (VSpaces k)) = fieldVS (Token :: Token k)

fieldVS :: Token k -> VSpace k k
fieldVS (Token :: Token Float) = VSpace (Group (#+) 0.0 negateFloat) (#*)


assoc :: forall (k :: *1) (c :: MCategory k) (x :: k) (y :: k) (z :: k).
  Token c -> {inh c x} -> {inh c y} -> {inh c z} ->
  {isomor c {getprod c x {getprod c y z}} {getprod c {getprod c x y} z}}
 
assoc (Token :: Token Hask) () () ()  = (\(a,(b,c)) -> ((a,b),c), 
                                           \((a,b),c) -> (a,(b,c)))
assoc (Token :: Token EndHask) m n o = (NatT (f1 m), NatT (f2 m))
  where f1 :: Functor a -> Compose a (Compose b c) x -> Compose (Compose a b) c x
        f1 (Functor fmapA) (Compose x) = Compose (Compose (fmapA fromCompose x))

        f2 :: Functor a -> Compose (Compose a b) c x -> Compose a (Compose b c) x
        f2 (Functor fmapA) (Compose (Compose x)) = Compose (fmapA Compose x)



-- No operators.
star :: (a -> c) -> (b -> d) -> (a,b) -> (c,d) 
star f g (x,y) = (f x, g y)

morprod :: forall (k :: *1) (c :: MCategory k) (x :: k) (y :: k) (z :: k) (t :: k).
  Token c -> {inh c x} -> {inh c y} -> {inh c z} -> {inh c t} ->
    {getmor c x y} -> {getmor c z t} -> {getmor c {getprod c x z} {getprod c y t}}
morprod (Token :: Token Hask) = \() () () () -> star
morprod (Token :: Token EndHask) = comp
  where comp = \_ (Functor f) _ _ (NatT u) (NatT v) -> NatT (\(Compose k) -> Compose (f v (u k))) 
morprod (Token :: Token Ab) = comp
  where comp = \_ _ _ _ (GroupHom f) (GroupHom g) -> GroupHom (\(Tensor xs) -> Tensor (map (f `star` g) xs))
morprod (Token :: Token Monoids) = comp
  where comp = \_ _ _ _ (MonoidHom f) (MonoidHom g) -> MonoidHom (star f g)
morprod (Token :: Token (VSpaces k)) = comp
  where comp = \_ _ _ _ (Linear f) (Linear g) -> Linear (\(Tensor xs) -> Tensor (map (f `star` g) xs))



-- More properly, natural isomorphism between A * and identity functor.
lambda :: forall (k :: *1) (c :: MCategory k) (x :: k).
  Token c -> {inh c x} -> ({getmor c {getprod c {getunit c} x} x}, {getmor c x {getprod c {getunit c} x}})
lambda (Token :: Token Hask)    _ = (\((),a) -> a, \a -> ((), a))
lambda (Token :: Token EndHask) _ = (NatT (\(Compose (Id x)) -> x), NatT (\x -> Compose (Id x)))
lambda (Token :: Token Graph)   _ = (GraT x, GraT (GCompose Eq))
  where x :: GCompose Equal c x y -> c x y
        x (GCompose Eq a) = a
lambda (Token :: Token Indexed) _ = (IndT x, IndT (ICompose . IndId))
  where x :: ICompose IndId m x y a -> m x y a
        x (ICompose (IndId a)) = a

fromIndId2 :: IndId u v a -> (Equal u v, a)
fromIndId2 (IndId x) = (Eq, x)

-- Todo: This "r" seems wrong
tran :: IxFunctor m -> ICompose m IndId x y a -> m x y a
tran n (ICompose a) = p n a
  where p :: forall x y z m a. IxFunctor m -> m x z (IndId z y a) -> m x y a
        p w a = r w (deeq w a)

        deeq :: forall x y z m a. IxFunctor m -> m x z (IndId z y a) -> m x z (Equal z y, a)
        deeq m k = deIxFunctor m fromIndId2 k

        r :: forall x y z m a. IxFunctor m -> m x z (Equal z y, a) -> m x y a
        r (IxFunctor w) a = undefined

tran2 :: IxFunctor m -> m x y a -> ICompose m IndId x y a
tran2 (IxFunctor x) k = ICompose (x IndId k)

rho :: forall (k :: *1) (c :: MCategory k) (x :: k).
  Token c -> {inh c x} -> ({getmor c {getprod c x {getunit c}} x}, {getmor c x {getprod c x {getunit c}}})
rho (Token :: Token Hask) () = (\(a,()) -> a, \a -> (a, ()))
rho (Token :: Token EndHask) f = (l f, r f)
  where l (Functor map) = NatT (map fromId . fromCompose)
        r (Functor map) = NatT (Compose . map Id)
rho (Token :: Token Graph) _ = (GraT x, GraT (\x -> GCompose x Eq))
  where x :: GCompose c Equal x y -> c x y
        x (GCompose a Eq) = a
rho (Token :: Token Indexed) m = (IndT (tran m), IndT (tran2 m))


assoclaw :: Monoid2 (MCat mor unit prod) m -> (mor (prod (prod m m) m) m, mor (prod (prod m m) m) m)--mor (prod (prod m m) m) (prod m (prod m m)))
assoclaw (M2 a _ mul) = (comp mul (prod (inhprod' t a) a a a mul ident),
                   comp (comp mul (prod a a (inhprod' t a) a ident mul)) (snd (assoc t a a a)))
  where t = Token :: Token (MCat mor unit prod)
        comp = morcomp t
        prod = morprod t
        ident = morid t

lunitlaw :: Monoid2 (MCat mor unit prod) m -> (mor m m, mor m m)
lunitlaw (M2 a un mul) = (ident, comp (comp mul (prod (inhunit' t) a a a un ident)) (snd (lambda t a)))
  where t = Token :: Token (MCat mor unit prod)
        comp = morcomp t
        prod = morprod t
        ident = morid t

runitlaw :: Monoid2 (MCat mor unit prod) m -> (mor m m, mor m m)
runitlaw (M2 a un mul) = (ident, comp (comp mul (prod a a (inhunit' t) a ident un)) (snd (rho t a)))
  where t = Token :: Token (MCat mor unit prod)
        comp = morcomp t
        prod = morprod t
        ident = morid t


nonmonoid :: Monoid2 Hask Int
nonmonoid = M2 () (\() -> 0) (\(x,y) -> x-y)


assoctest m a b c = let (x,y) = assoclaw m
                        u = ((a,b),c)
                    in (x u, y u)

lunittest m a = let (x,y) = lunitlaw m
                in (x a, y a)

runittest m a = let (x,y) = runitlaw m
                in (x a, y a)


{-
test:

assoctest nonmonoid 2 3 4
lunittest nonmonoid 3
runittest nonmonoid 3
-}

-------------------------------------------------------------------------------
-- Level polymorphism
-------------------------------------------------------------------------------

data MCategory' :: level n. *n ~> *n ~> *n where
  MCat' :: forall (k :: *n) (m :: *n). (k ~> k ~> m) ~>
                   k ~> (k ~> k ~> k) ~> MCategory' m k

data Monoid' :: level n. forall (k :: *(n+1)) (mo :: *(n+1)).
                 MCategory' mo k ~> k ~> *n where
  M' :: forall (k :: *(n+1)) (mo :: *(n+1)) (m :: k) (mor :: k ~> k ~> mo)
          (unit :: k) (prod :: k ~> k ~> k).
          mor unit m ~> mor (prod m m) m ~>
          Monoid' (MCat' mor unit prod) m

type Hask' = MCat' (->) () (,)
type EndHask' = MCat' NatT Id Compose

sumMonoid' :: Monoid' Hask' Int
sumMonoid' = M' (\() -> 1) (\(x,y) -> x*y)

maybeMonad' :: Monoid' EndHask' Maybe
maybeMonad' = M' (NatT (\(Id x) -> Just x)) (NatT join)
  where join (Compose (Just (Just x))) = Just x
        join _ = Nothing

kind Unit = Unt
kind Morp x y = Mrp (x ~> y)
kind Prod x y = Prd x y

type Cat = MCat' Morp Unit Prod

data UnitHsk :: Unit ~> *0 where
  UnitHskV :: UnitHsk Unt

data ProdHsk :: Prod *0 *0 ~> *0 where
  ProdHskV :: (x, y) -> ProdHsk (Prd x y)

type Hask'' = M' (Mrp UnitHsk) (Mrp ProdHsk)  -- :: Monoid' Cat *


data IdEHsk :: Unit ~> *0 ~> *0 where
  IdEHskV :: x -> IdEHsk Unt x

data CompEHsk :: Prod (*0 ~> *0) (*0 ~> *0) ~> *0 ~> *0 where
  CompEHskV :: Compose f g x -> CompEHsk (Prd f g) x

type EndHask'' = M' (Mrp IdEHsk) (Mrp CompEHsk) -- :: Monoid' Cat (* ~> *)



data Curry f x y = Curry (f (Prd x y))

crea :: Monoid' Cat *0 ~> (*0 ~> *0 ~> *0) ~> MCategory *0
{crea (M' (Mrp u) (Mrp p)) mor} = MCat mor (u Unt) (Curry p)

intmul :: Monoid {crea Hask'' (->)} Int
intmul = M (\UnitHskV -> 1) (\(Curry (ProdHskV (x,y))) -> x * y)


crea' :: Monoid' Cat *0 ~> (*0 ~> *0 ~> m) ~> MCategory' m *0
{crea' (M' (Mrp u) (Mrp p)) mor} = MCat' mor (u Unt) (Curry p)

intmul' :: Monoid' {crea' Hask'' (->)} Int
intmul' = M' (\UnitHskV -> 1) (\(Curry (ProdHskV (x,y))) -> x * y)

data Curry2 f x y z = Curry2 (f (Prd x y) z)

crea'' :: Monoid' Cat (*0 ~> *0) ~> ((*0 ~> *0) ~> (*0 ~> *0) ~> m) ~>
           MCategory' m (*0 ~> *0)
{crea'' (M' (Mrp u) (Mrp p)) mor} = MCat' mor (u Unt) (Curry2 p)

may :: Monoid' {crea'' EndHask'' NatT} Maybe
may = M' (NatT (\(IdEHskV a) -> Just a)) (NatT (\(Curry2 (CompEHskV (Compose x))) -> j x))
  where j (Just (Just x)) = Just x
        j _ = Nothing




--- Lax monoidal
data GFunctor mor1 mor2 f = GFunctor (forall x y. mor1 x y -> mor2 (f x) (f y))
conv :: Functor f -> GFunctor (->) (->) f
conv (Functor k) = GFunctor k


data LaxMonoidal :: MCategory k ~> MCategory l ~> (k ~> l) ~> *0 where
  LaxM :: forall (k :: *1) (l :: *1)
                 (mor1 :: k ~> k ~> *0) (un1 :: k) (prod1 :: k ~> k ~> k)
                 (mor2 :: l ~> l ~> *0) (un2 :: l) (prod2 :: l ~> l ~> l)
                 (f :: k ~> l).
            GFunctor mor1 mor2 f -> mor2 un1 (f un2) ->
            (forall a b. mor2 (prod2 (f a) (f b)) (f (prod1 a b))) ->
            LaxMonoidal (MCat mor1 un1 prod1) (MCat mor2 un2 prod2) f

-- Monad to applicative
monToApp :: Monoid2 EndHask m -> LaxMonoidal Hask Hask m
monToApp (M2 fmap (NatT r) (NatT j)) = LaxM (conv fmap) return zip
  where zip (u,v) =  u `bind` (\u' ->
                     v `bind` (\v' ->
                     return (u',v')))
        bind x f = j (Compose (deFunctor fmap f x))
        return = r . Id