ObjIndexedCategory.hs

#!/usr/bin/env stack
{- stack --resolver lts-12.0 runghc -}

{-# LANGUAGE TypeFamilies, FlexibleInstances #-}
{-# LANGUAGE DataKinds, PolyKinds, KindSignatures, TypeInType #-}
{-# LANGUAGE AllowAmbiguousTypes, TypeApplications, GADTs #-}

import Prelude hiding ((.), id)
import qualified Prelude
import Data.Kind


class Category o where
  type Hom o (a :: o) (b :: o) :: Type
  type ValidObject o (a :: o) :: Constraint
  type ValidObject o a = ()
  (.) :: Hom o b c -> Hom o a b -> Hom o a c
  id :: ValidObject o a => Hom o a a


instance Category Type where
  type Hom Type a b = a->b
  (.) = (Prelude..)
  id = Prelude.id

f :: Hom Type Int Int
f 0 = 0
f n = n+1

g :: Hom Type Int Int
g = succ

h :: Hom Type Int Int
h = (.) @Type g f


main :: IO ()
main = print [h 0, h 1, h 2]


data XY = X | Y

data XYMorphism :: (XY -> XY -> *) where
  X2X :: XYMorphism 'X 'X
  Y2Y :: XYMorphism 'Y 'Y
  X2Y :: XYMorphism 'X 'Y
  Y2X :: XYMorphism 'Y 'X

class XOrY (p :: XY) where
  xyId :: XYMorphism p p
instance XOrY 'X where xyId = X2X
instance XOrY 'Y where xyId = Y2Y

instance Category XY where
  type Hom XY a b = XYMorphism a b
  type ValidObject XY p = XOrY p
  X2X . f = f
  Y2Y . f = f
  f . X2X = f
  f . Y2Y = f
  X2Y . Y2X = Y2Y
  Y2X . X2Y = X2X
  id = xyId

This is a Haskell version of the Idris interface proposed in idris-lang/Idris-dev#4736