gistfile1.hs

{-#LANGUAGE PolyKinds, TypeFamilies, TypeOperators, ConstraintKinds, UndecidableInstances, FlexibleInstances, FunctionalDependencies, MultiParamTypeClasses, TypeOperators, KindSignatures #-}
import qualified Prelude ((.), id, String)
import Data.Proxy
import GHC.Exts
import GHC.TypeLits

class SmallCategory cat where
    name :: Proxy cat -> Prelude.String
    id ::(Objects cat a, CategoryMorphism cat morph) => morph a a
    type Objects cat :: a ->  Constraint 
--    type Morph cat :: a -> a -> b 
class CategoryMorphism cat morph | cat -> morph, morph -> cat where
    (.) :: (Objects cat a, Objects cat b, Objects cat c) => b `morph` c -> a `morph` b -> a `morph` c

instance SmallCategory "Hask" where
    id = Prelude.id
    name Proxy = "Hask"
    type Objects "Hask" = Vacuous "Hask"
--    type Morph "Hask" = (->)
instance CategoryMorphism "Hask" (->) where
    (.) = (Prelude..)

--what I wish, using monoids and vector spaces as examples:
-- data Monoid = forall a. Monoid  {identity :: a, op :: a -> a -> a}
-- instance SmallCategory "Monoids"  FOR SOME MONOID m where
--     id = ((op m) (identity m))
--     (.) = op m
--     type Objects "Monoids" a = (a ~ Monoid)
-- type Vector = [Double]
-- type Matrix = [[Double]]
-- instance SmallCategory "FinVect_k" where
--     id = fgsfds -- k-dimensional identity matrix
--     (.) = matrixMultiply
--     type Objects "FinVect_k" a = (a ~ forall m. [m])
-- let m = Monoid 0 (+) using "Monoids" in 1 . 2 . 3
-- let k = 3 using "FinVect_k" in a . b . c . d . id . e . a --rotation matrices for example