CTC

CTC.hs

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple"        @-}
{-@ LIQUID "--etabeta"    @-}

module CTC where

import Prelude hiding (id)
import Language.Haskell.Liquid.ProofCombinators

data Cat k = Cat
  { comp    :: forall b c a. k b c -> k a b -> k a c
  , id      :: forall a. k a a
  , idLeft  :: forall a b. k a b -> Proof
  , idRight :: forall a b. k a b -> Proof
  , assoc   :: forall a b c d. k a b -> k b c -> k c d -> Proof
  }

{-@ 
data Cat kd k = Cat
  { comp    :: forall b c a. k b c -> k a b -> k a c
  , id      :: forall a. k a a
  , idLeft  :: forall a b. y:k a b -> { comp id y = y }
  , idRight :: forall a b. y:k a b -> { comp y id = y }
  , assoc   :: forall a b c d. x:k a b -> y:k b c -> z:k c d -> { comp z (comp y x) = comp (comp z y) x }
  }
@-}


{-@ reflect composeHask @-}
composeHask :: (b -> c) -> (a -> b) -> (a -> c)
composeHask g f x = g (f x)

{-@ reflect idHask @-}
idHask :: a -> a
idHask x = x

hask = Cat
    { id      = idHask
    , comp    = composeHask
    , idLeft  = \x -> trivial
    , idRight = \x -> trivial
    , assoc   = \x y z -> trivial
    }

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple" @-}
{-@ LIQUID "--etabeta" @-}
{-@ LIQUID "--save" @-}

module CTC where

import Prelude hiding (id, (<>))

{-@ reflect idF @-}
idF :: a -> a
idF x = x

data Category k = Category
{ comp :: forall b c a. k b c -> k a b -> k a c
, iddd :: forall a. k a a
, idLeft :: forall a b. k a b -> ()
}

{-@ Category :: comp:(forall b c a. k b c -> k a b -> k a c)
-> iddd:(forall a. k a a)
-> idLeft : (forall a b. y:k a b -> { comp iddd y = y })
-> Category kind k @-}

{-@ idLeftHask :: f:_ -> { composeF idF f = f } @-}
idLeftHask :: (a -> b) -> ()
idLeftHask f = ()

{-@ reflect composeF @-}
composeF :: (b -> c) -> (a -> b) -> (a -> c)
composeF g f x = g (f x)

hask = Category composeF idF idLeftHask