NamedFunctors.hs

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE InstanceSigs #-}
module NamedFunctors where

import Prelude ()
import qualified Prelude hiding ((.), id)
import Data.Kind (Type)
import GHC.TypeLits (Nat, KnownNat, natVal)
import Data.Proxy (Proxy(..))
import qualified Control.Category as Prelude

type family Obj cat :: k
-- type family Arr cat (src :: Obj cat) (dst :: Obj cat) :: Type
type family Arr cat (src :: k) (dst :: k) :: Type

class Category cat where
  id  ::  forall (a :: Obj cat).
          Arr cat a a
  (.) ::  forall (a :: Obj cat) (b :: Obj cat) (c :: Obj cat).
          Arr cat b c -> Arr cat a b -> Arr cat a c

data Hask
type instance Obj Hask = Type
type instance Arr Hask a b = a -> b
instance Category Hask where
  id = Prelude.id
  (.) = (Prelude..)

data Plus n
type instance Obj (Plus n) = ()
type instance Arr (Plus n) a b = n
instance Prelude.Num n => Category (Plus n) where
  id = 0
  (.) = (Prelude.+) 

data Multiply n
type instance Obj (Multiply n) = ()
type instance Arr (Multiply n) a b = n
instance Prelude.Num n => Category (Multiply n) where
  id = 1
  (.) = (Prelude.*)

type family Dual cat where
  Dual (DualCat cat) = cat
  Dual cat = DualCat cat

data DualCat cat
newtype DualArr cat a b = DualArr (Arr cat b a)

type instance Obj (DualCat cat) = Obj cat
type instance Arr (DualCat cat) a b = DualArr cat a b
instance Category cat => Category (DualCat cat) where
  id :: forall a. Arr (DualCat cat) a a
  id = DualArr (id @cat @a)

  (.) :: forall a b c. Arr (DualCat cat) b c -> Arr (DualCat cat) a b -> Arr (DualCat cat) a c
  DualArr f . DualArr g = DualArr ((.) @cat @c @b @a g f)

data LiftCategory (arr :: k -> k -> *)
type instance Obj (LiftCategory (arr :: k -> k -> *)) = k
type instance Arr (LiftCategory (arr :: k -> k -> *)) a b = arr a b
instance Prelude.Category arr => Category (LiftCategory arr) where
  id = Prelude.id
  (.) = (Prelude..)

type family Src f 
type family Dst f

class (Category (Src f), Category (Dst f)) => Functor f where
  -- type Map f (a :: Obj (Src f)) :: Obj (Dst f)
  type Map f a
  map :: Arr (Src f) a b -> Arr (Dst f) (Map f a) (Map f b)

data Identity cat
type instance Src (Identity cat) = cat
type instance Dst (Identity cat) = cat
instance Category cat => Functor (Identity cat) where
  type Map (Identity cat) obj = obj
  map arr = arr

data Pow (base :: Nat) (exp :: Type)
type instance Src (Pow base exp) = Plus exp
type instance Dst (Pow base exp) = Multiply exp
instance (KnownNat base, Prelude.Num exp) => Functor (Pow base exp) where
  type Map (Pow base exp) n = n
  map n = n Prelude.^ natVal (Proxy @base)

data First (b :: Type)
type instance Src (First b) = Hask
type instance Dst (First b) = Hask
instance Functor (First b) where
  type Map (First b) a = (a, b)
  map f (a, b) = (f a, b)

data Second (a :: Type)
type instance Src (Second a) = Hask
type instance Dst (Second a) = Hask
instance Functor (Second a) where
  type Map (Second a) b = (a, b)
  map f (a, b) = (a, f b)

data LiftFunctor (f :: Type -> Type)
type instance Src (LiftFunctor f) = Hask
type instance Dst (LiftFunctor f) = Hask
instance Prelude.Functor f => Functor (LiftFunctor f) where
  type Map (LiftFunctor f) a = f a
  map = Prelude.fmap
  
data Input (b :: Type)
type instance Src (Input b) = Dual Hask
type instance Dst (Input b) = Hask
instance Functor (Input b) where
  type Map (Input b) a = a -> b
  map (DualArr f) g x = g (f x)