Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Nat as a type-level category, to be used as the index of a category-indexed monad
-- https://stackoverflow.com/a/57046042/477476
-- https://gist.github.com/Lysxia/04039e4ca6f7a3740281e4e3583ae971
{-# LANGUAGE RankNTypes, TypeFamilies, PolyKinds, DataKinds #-}
{-# LANGUAGE TypeApplications, TypeOperators, GADTs #-}
import Prelude hiding (id, (.))
import Control.Category
import Data.Kind
import GHC.TypeLits
class CatMonad (m :: forall (x :: k) (y :: k). c x y -> Type -> Type) where
type Id m :: c x x
type Cat m (f :: c x y) (g :: c y z) :: c x z
xpure :: a -> m (Id m) a
xbind :: m f a -> (a -> m g b) -> m (Cat m f g) b
data Edge (x :: ()) (y :: ()) where
E :: Nat -> Edge '() '()
type family EPlus (n :: Edge x y) (m :: Edge y z) :: Edge x z where
EPlus (E n) (E m) = E (n + m)
newtype Counter (i :: ()) (j :: ()) (q :: Edge i j) a = Counter { runCounter :: a }
instance CatMonad Counter where
type Id Counter = E 0
type Cat Counter f g = EPlus f g
xpure = Counter
xbind act k = Counter $ runCounter $ k $ runCounter act
tick :: Counter '() '() (E 1) ()
tick = Counter ()
-- > :t hello
-- hello :: Counter '() '() ('E 3) Integer
hello = do
tick
tick
x <- pure 4
tick
y <- pure 5
pure $ x + y
where
pure = xpure @_ @_ @Counter
(>>=) = xbind @_ @_ @Counter
return = pure
m >> n = m >>= \_ -> n
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.