Skip to content

Instantly share code, notes, and snippets.

@Lysxia Lysxia/CatMonad.hs
Last active Jul 16, 2019

Embed
What would you like to do?
{-# LANGUAGE GADTs, FunctionalDependencies, FlexibleInstances, MultiParamTypeClasses, RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}
module CatMonad where
import Control.Category as C
import Data.Kind
class CatMonad (c :: k -> k -> Type) (m :: forall (x :: k) (y :: k). c x y -> Type -> Type) | c -> m where
type Id c :: c x x
type Cat c (f :: c x y) (g :: c y z) :: c x z
xpure :: a -> m (Id c) a
xbind :: m f a -> (a -> m g b) -> m (Cat c f g) b
data Edge (cat :: k -> k -> Type) (x :: k) (y :: k) = E
-- newtype IWriter (cat :: k -> k -> Type) (i :: k) (j :: k) (q :: Edge cat i j) (a :: Type)
-- = IWriter { runWriter :: (a, cat i j) }
newtype IWriter (cat :: k -> k -> Type) :: forall (i :: k) (j :: k). Edge cat i j -> Type -> Type where
IWriter :: { runWriter :: (a, cat i j) } -> IWriter cat (e :: Edge cat i j) a
instance Category cat => CatMonad (Edge cat) (IWriter cat) where
type Id (Edge cat) = E
type Cat (Edge cat) _ _ = E
xpure a = IWriter (a, C.id)
xbind (IWriter (a, f)) k =
let IWriter (b, g) = k a in
IWriter (b, f C.>>> g)
hello :: IWriter (->) (E :: Edge (->) Bool Bool) String
hello = xpure "hello"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.