Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Kind-polymorphic Category
{-# LANGUAGE PolyKinds, KindSignatures, TypeOperators, TypeFamilies #-}
{-# LANGUAGE ConstraintKinds, GADTs, RankNTypes #-}
module Categories where
import qualified Prelude
import GHC.Prim (Constraint)
--------------------------------------------------------------------------------
-- Kind-polymorphic Category
class Category cat where
-- inferred: 'cat :: k -> k -> *'
id :: cat a a
(.) :: cat b c -> cat a b -> cat a c
instance Category (->) where
id = Prelude.id
(.) = (Prelude..)
--------------------------------------------------------------------------------
-- Logical entailment
data Dict :: Constraint -> * where
Dict :: ctx => Dict ctx
newtype (|-) a b = Sub (a => Dict b)
(\\) :: a => (b => r) -> (a |- b) -> r
r \\ Sub Dict = r
reflexive :: a |- a
reflexive = Sub Dict
transitive :: (b |- c) -> (a |- b) -> (a |- c)
transitive f g = Sub (Dict \\ f \\ g)
instance Category (|-) where
id = reflexive
(.) = transitive
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment