FiniteCategories.hs

{-# LANGUAGE TemplateHaskell, QuasiQuotes       #-}
{-# LANGUAGE DataKinds, KindSignatures          #-}
{-# LANGUAGE ScopedTypeVariables, UnicodeSyntax #-}
{-# LANGUAGE TypeFamilies, GADTs                #-}
{-# LANGUAGE ConstraintKinds                    #-}

import Data.Singletons.TH  -- http://hackage.haskell.org/package/singletons-2.7/
import Data.Singletons (sing, Sing, SingI)
import Control.Category.Constrained (Category(..)) -- http://hackage.haskell.org/package/constrained-categories-0.4.1.0

$(singletons [d|
   data TcObjectKind = TcObject
  |])
$(singletons [d|
   data Trap = Free | Trapped
  |])

data TcArrowType (a₀ :: TcObjectKind) (a₁ :: TcObjectKind) where
  TcArrow :: TcArrowType 'TcObject 'TcObject

data TrapArrowType (a₀ :: Trap) (a₁ :: Trap) where
  StillFree :: TrapArrowType 'Free 'Free
  Falling :: TrapArrowType 'Free 'Trapped
  Stuck :: TrapArrowType 'Trapped 'Trapped

tcId :: ∀ a . SingI a => TcArrowType a a
tcId = case sing :: Sing a of
  STcObject -> TcArrow

trapId :: ∀ a . SingI a => TrapArrowType a a
trapId = case sing :: Sing a of
  SFree -> StillFree
  STrapped -> Stuck


instance Category TcArrowType where
  type Object TcArrowType a = SingI a
  id = tcId
  TcArrow . TcArrow = TcArrow

instance Category TrapArrowType where
  type Object TrapArrowType a = SingI a
  id = trapId
  StillFree . StillFree = StillFree
  Stuck . Stuck = Stuck
  Stuck . Falling = Falling
  Falling . StillFree = Falling

https://stackoverflow.com/questions/64743559/how-can-we-build-explicit-categories-in-haskell/