--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--Module       : Data.Category
--Author       : Daniel Schüssler
--License      : BSD3
--Copyright    : Daniel Schüssler
--
--Maintainer   : Daniel Schüssler
--Stability    : Experimental
--Portability  : Uses various GHC extensions
--
--------------------------------------------------------------------------------
--Description  : 
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------



{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

-- | This module is a stub!
module Data.Category where

import Type.Set
import Type.Dummies
import Type.Function
import Type.Logic
import Data.Type.Equality
import Control.Monad
import Control.Category
import Prelude hiding(id,(.))
    

-- | Category with type-level set of objects and type-level /hom/ function, but value-level composition and value-level definition of identity functions.
data Cat ob hom =
    Cat {
      homIsFun :: ((ob :×: ob) :~>: Univ) hom
    , getid :: forall a. a :∈: ob -> ExId hom a
    -- | Composition
    , getc :: forall a b c. 
           a :∈: ob ->
           b :∈: ob ->
           c :∈: ob ->
           ExC hom a b c
    }
                
-- | Existential wrapping of the identity function on a
data ExId hom a where
    ExId :: ((a,a),aa) :∈: hom -> aa -> ExId hom a
           
-- | Existential wrapping of the composition for types a,b,c
data ExC hom a b c where
    ExC ::
           ((b,c), bc) :∈: hom ->
           ((a,b), ab) :∈: hom ->
           ((a,c), ac) :∈: hom ->
               
           (bc -> ab -> ac) ->

           ExC hom a b c

                
hask :: Cat Univ HaskFun
hask = Cat (extendCod haskFunIsFun auto)
       (\_ -> ExId HaskFun id)
       (\_ _ _ -> ExC HaskFun HaskFun HaskFun (.))
       
kleisli :: Monad m => Cat Univ (KleisliHom m)
kleisli = Cat (extendCod kleisliHomIsFun auto)
          (\_ -> ExId KleisliHom return)
          (\_ _ _ -> ExC KleisliHom KleisliHom KleisliHom (<=<))
          

fromControlCategory :: (Category hom) => Cat Univ (BiGraph hom)
fromControlCategory = Cat biGraphIsFun
                      (\_ -> ExId BiGraph id)
                      (\_ _ _ -> ExC BiGraph BiGraph BiGraph (.))

          
-- | Lemma for constructing categories; abstracts the usage of the hom function's 'total'
makeCat :: ((ob :×: ob) :~>: Univ) hom ->  
          (forall a aa. ((a,a),aa) :∈: hom -> aa) ->
              
          (forall a b c bc ab ac.
           ((b,c), bc) :∈: hom ->
           ((a,b), ab) :∈: hom ->
           ((a,c), ac) :∈: hom ->
               
           (bc -> ab -> ac)) ->


          Cat ob hom

makeCat hom k1 k2 =
    Cat hom 
     (\a -> case total hom (a :×: a) of
             ExSnd aa -> ExId aa (k1 aa))
     (\a b c -> case ( total hom (b :×: c)
                    , total hom (a :×: b)
                    , total hom (a :×: c) ) of
                      
                      ( ExSnd bc
                       ,ExSnd ab
                       ,ExSnd ac ) ->  

                           ExC bc ab ac (k2 bc ab ac) )

               
                                 
                             
-- idAuto :: forall ob hom a aa. Fact (((a, a), aa) :∈: hom) => Cat ob hom -> aa

idauto :: (Fact (a :∈: ob)) => Cat ob hom -> ExId hom a
idauto cat = getid cat auto

--      Cat ob hom -> bc -> ab -> ac


cauto :: (Fact (a :∈: ob), Fact (b :∈: ob), Fact (c :∈: ob)) =>
     Cat ob hom -> ExC hom a b c
cauto cat = getc cat auto auto auto

-- test :: a -> a
-- test = idAuto hask


-- test2 :: (b -> c) -> (a -> b) -> a -> c
-- test2 = ccAuto hask
        

-- test3 :: forall m a. Monad m => a -> m a
-- test3 = idAuto kleisli
      
-- foo :: forall a. a -> a
-- foo = idEx hask (Univ :: Univ a) go
--       where
--          go :: (((a, a), aa) :∈: HaskFun) -> aa -> (a -> a)
--          go HaskFun x = x

       
data GFunctor ob1 hom1 ob2 hom2 f = 
    GFunctor {
      omapIsFun :: (ob1 :~>: ob2) f
    , getfmap :: forall a b.
              a :∈: ob1 ->
              b :∈: ob1 ->
              
              ExFmap hom1 hom2 f a b
                  
    }

data ExFmap hom1 hom2 f a b where
    ExFmap ::
              (a,fa) :∈: f ->
              (b,fb) :∈: f ->
              ((a,b),ab) :∈: hom1 ->
              ((fa,fb),fafb) :∈: hom2 ->

              (ab -> fafb) ->

                  ExFmap hom1 hom2 f a b

fromFunctor :: (Functor f) => GFunctor Univ HaskFun Univ HaskFun (Graph f)
fromFunctor = GFunctor graphIsFun (\_ _ -> ExFmap Graph Graph HaskFun HaskFun fmap)


                                  
-- gmapCPS f afa bfb abab fafbfafb k
--         = case ( total (homIsFun cat) (b :×: c)
--                , total (homIsFun cat) (a :×: b)
--                , total (homIsFun cat) (a :×: c) ) of
                      
--                       ( ExSnd bc
--                        ,ExSnd ab
--                        ,ExSnd ac ) ->  k bc ab ac (cc cat bc ab ac)