constrained-category.hs

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}

import Control.Category
import GHC.Exts (Constraint)
import Prelude hiding ((.))

data NC (c :: * -> Constraint) (t :: * -> * -> *) a b where
  Id :: NC c t a a
  NC :: (c a, c x) => t a x -> NC c t x b -> NC c t a b

instance Category (NC c t) where
  id = Id
  g . Id = g
  g . NC m k = NC m (g . k)

class (Show a, Eq a) => ShowEq a
instance (Show a, Eq a) => ShowEq a

newtype FooF a b = Fun (a -> b)

newtype Foo a b = Foo { runFoo :: NC ShowEq FooF a b } deriving Category

liftFoo :: (Eq a, Show a, Eq b, Show b) => (a -> b) -> Foo a b
liftFoo f = Foo (NC (Fun f) Id)

run :: Foo a b -> a -> b
run = go . runFoo
  where
    go :: NC ShowEq FooF a b -> a -> b
    go Id = id
    go (NC (Fun f) k) = go k . f

runShow :: Show b => Foo a b -> a -> (b, [String])
runShow = (runWriter .) . go . runFoo
  where
    go :: Show b => NC ShowEq FooF a b -> a -> Writer [String] b
    go Id x = x <$ tell [show x]
    go (NC (Fun f) k) x = tell [show x] *> go k (f x)

fooIncr :: (Eq a, Show a, Num a) => Foo a a
fooIncr = liftFoo (1+)

fooShow :: (Eq a, Show a) => Foo a String
fooShow = liftFoo show

fooRead :: (Eq a, Show a, Read a) => Foo String a
fooRead = liftFoo read

abc :: Foo Int Double
abc = fooIncr . fooRead . fooShow . fooIncr