Cat.hs

{-# LANGUAGE
    PolyKinds,
    InstanceSigs,
    DataKinds,
    GADTs #-}

module Cat where

import Control.Category
import Prelude hiding ((.))
import Data.Kind

-- 0 --> 1

data C = Z | O

data Arr (a :: C) (b :: C) where
  Id :: Arr a a
  X :: Arr 'Z 'O

instance Category Arr where
  id = Id

  Id . g = g
  f . Id = f

data FreeCat (g :: k -> k -> Type) (a :: k) (b :: k) where
  FreeId :: FreeCat g a a
  FreeDot :: g a b -> FreeCat g b c -> FreeCat g a c

instance Category (FreeCat g) where
   id = FreeId

   a . FreeId = a
   a . FreeDot h b = FreeDot h (a . b)

data List a = Nil | Sing a | App (List a) (List a)

{-
-- | A Cartesian-closed category is a Category k, together with...
class Category k => CCC k where
  -- | a terminal object,
  data Unit k :: *
  -- | products
  data Tensor k :: * -> * -> *
  -- | exponentials,
  data Hom k :: * -> * -> *

  -- | currying and uncurring operations,
  curry :: forall a b c. k (Tensor k a b) c -> k a (Hom k b c)
  uncurry :: forall a b c. k a (Hom k b c) -> k (Tensor k a b) c

  -- | product introduction and elimination terms
  fork :: forall a c d. k a c -> k a d -> k a (Tensor k c d)
  exl :: forall a b. k (Tensor k a b) a
  exr :: forall a b. k (Tensor k a b) b
-}

-- https://blog.functorial.com/posts/2017-10-08-HOAS-CCCs.html