{-# LANGUAGE RankNTypes, PolyKinds, DataKinds, ConstraintKinds, ScopedTypeVariables, KindSignatures, TypeFamilies, MultiParamTypeClasses, UndecidableInstances, GADTs, AllowAmbiguousTypes, FlexibleInstances #-}
module Hask.Category.Polynomial
  ( 
  -- * Product Category
    Product(..), ProductOb, Fst, Snd
  -- * Coproduct Category
  , Coproduct(..), CoproductOb(..)
  -- * Unit Category
  , Unit(..)
  -- * Empty Category
  , Empty
  , Void, absurd

  ) where

import Hask.Category
import Data.Void
import Hask.Functor.Faithful
import Prelude (error)

--------------------------------------------------------------------------------
-- * Products
--------------------------------------------------------------------------------

-- TODO: do this as a product of profunctors instead?
data Product (p :: i -> i -> *) (q :: j -> j -> *) (a :: (i, j)) (b :: (i, j)) =
  Product (p (Fst a) (Fst b)) (q (Snd a) (Snd b))

type family Fst (p :: (i,j)) :: i
type instance Fst '(a,b) = a

type family Snd (q :: (i,j)) :: j
type instance Snd '(a,b) = b

class    (Ob p (Fst a), Ob q (Snd a)) => ProductOb (p :: i -> i -> *) (q :: j -> j -> *) (a :: (i,j))
instance (Ob p (Fst a), Ob q (Snd a)) => ProductOb (p :: i -> i -> *) (q :: j -> j -> *) (a :: (i,j))

instance (Category p, Category q) => Functor (Product p q) where
  type Dom (Product p q) = Op (Product (Opd p) (Opd q))
  type Cod (Product p q) = Nat (Product (Dom2 p) (Dom2 q)) (->)
  fmap f = case observe f of
    Dict -> Nat (. unop f)

instance (Category p, Category q, ProductOb p q a) => Functor (Product p q a) where
  type Dom (Product p q a) = Product (Dom2 p) (Dom2 q)
  type Cod (Product p q a) = (->)
  fmap = (.)

instance (Category p, Category q) => Category' (Product p q) where
  type Ob (Product p q) = ProductOb p q
  id = Product id id
  Product f f' . Product g g' = Product (f . g) (f' . g')
  observe (Product f g) = case observe f of
    Dict -> case observe g of
      Dict -> Dict


--------------------------------------------------------------------------------
-- * Coproducts
--------------------------------------------------------------------------------

data Coproduct (c :: i -> i -> *) (d :: j -> j -> *) (a :: Either i j) (b :: Either i j) where
  Inl :: c x y -> Coproduct c d (Left x) (Left y)
  Inr :: d x y -> Coproduct c d (Right x) (Right y)

class CoproductOb (p :: i -> i -> *) (q :: j -> j -> *) (a :: Either i j) where
  side :: Endo (Coproduct p q) a -> (forall x. (a ~ Left x, Ob p x) => r) -> (forall y. (a ~ Right y, Ob q y) => r) -> r
  coproductId :: Endo (Coproduct p q) a

instance (Category p, Ob p x) => CoproductOb (p :: i -> i -> *) (q :: j -> j -> *) (Left x :: Either i j) where
  side _ r _ = r
  coproductId = Inl id

instance (Category q, Ob q y) => CoproductOb (p :: i -> i -> *) (q :: j -> j -> *) (Right y :: Either i j) where
  side _ _ r = r
  coproductId = Inr id

instance (Category p, Category q) => Functor (Coproduct p q) where
  type Dom (Coproduct p q) = Op (Coproduct p q)
  type Cod (Coproduct p q) = Nat (Coproduct p q) (->)
  fmap (Op f) = Nat (. f)

instance (Category p, Category q) => Functor (Coproduct p q a) where
  type Dom (Coproduct p q a) = Coproduct p q
  type Cod (Coproduct p q a) = (->)
  fmap = (.)

instance (Category p, Category q) => Category' (Coproduct p q) where
  type Ob (Coproduct p q) = CoproductOb p q
  id = coproductId
  observe (Inl f) = case observe f of
    Dict -> Dict
  observe (Inr f) = case observe f of
    Dict -> Dict
  Inl f . Inl g = Inl (f . g)
  Inr f . Inr g = Inr (f . g)
  _ . _ = error "Type error"

--------------------------------------------------------------------------------
-- * The Unit category
--------------------------------------------------------------------------------

data Unit a b = Unit

instance Functor Unit where
  type Dom Unit = Op Unit
  type Cod Unit = Nat Unit (->)
  fmap _ = Nat $ \_ -> Unit

instance Functor (Unit a) where
  type Dom (Unit a) = Unit
  type Cod (Unit a) = (->)
  fmap _ _ = Unit

instance Category' Unit where
  type Ob Unit = Vacuous Unit
  id = Unit
  Unit . Unit = Unit
  observe _ = Dict

instance FullyFaithful Unit where
  unfmap _ = Op Unit

instance FullyFaithful (Unit a) where
  unfmap _ = Unit


--------------------------------------------------------------------------------
-- * The Empty category
--------------------------------------------------------------------------------

data Empty (a :: Void) (b :: Void)

{-
instance Functor Empty where
  type Dom Empty = Op Empty
  type Cod Empty = Nat Empty (->)
  fmap f = case f of {}

instance No (:-) a => Functor (Empty a) where
  type Dom (Empty a) = Empty
  type Cod (Empty a) = (->)
  fmap f = case f of {}

data NO = No

-- | the functor from the empty category to every category
type No = (Any 'No :: (i -> i -> *) -> Void -> i)

-- | the empty category
instance Category' c => Functor (No c) where
  type Dom (No c) = Empty
  type Cod (No c) = c
  fmap f = case f of {}

instance Category' Empty where
  type Ob Empty = No (:-)
  id = undefined -- no
  f . _ = case f of {}
  observe f = case f of {}
-}