Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Kind-indexed Category instance for Kleisli
-- https://www.reddit.com/r/haskell/comments/abxem5/experimenting_with_kleisli_instance_of/
{-# Language TypeApplications #-}
{-# Language RankNTypes #-}
{-# Language DataKinds #-}
{-# Language KindSignatures #-}
{-# Language PolyKinds #-}
{-# Language TypeOperators #-}
{-# Language GADTs #-}
{-# Language TypeFamilies #-}
{-# Language TypeSynonymInstances #-}
{-# Language FlexibleInstances #-}
{-# Language InstanceSigs #-}
import Data.Kind
import Prelude hiding (id, (<), (>))
import Control.Monad
type Obj = Type
-- Kleisli
newtype KleisliKind :: (Type -> Type) -> Obj where
Kl :: Type -> KleisliKind m
type family
UnKl (kl :: KleisliKind m) :: Type where
UnKl (Kl a) = a
class kl ~ Kl (UnKl kl) => UnKl_ (kl :: KleisliKind m)
instance kl ~ Kl (UnKl kl) => UnKl_ (kl :: KleisliKind m)
-- Kleisli :: forall m -> Cat (KleisliKind m)
data Kleisli m :: Cat (KleisliKind m) where
MkKleisli :: (a -> m b) -> Kleisli m (Kl a) (Kl b)
-- Category
type Cat (ob :: Obj) = ob -> ob -> Obj
class Empty a
instance Empty a
class Category (ob :: Obj) where
type (-->) :: Cat ob
type Object :: ob -> Constraint
type Object = Empty
id :: Object (a :: ob)
=> (a --> a)
(>) :: (a --> b)
-> (b --> c)
-> (a --> (c :: ob))
instance Category (Type :: Obj) where
type (-->) = (->)
id :: a -> a
id a = a
(>) :: (a -> b) -> (b -> c) -> (a -> c)
(one > two) a = two (one a)
instance Monad m => Category (KleisliKind m :: Obj) where
-- type (-->) @(KleisliKind m) = Kleisli m
type (-->) = (Kleisli m :: Cat (KleisliKind m))
type Object = UnKl_
id :: forall a. Kleisli m (Kl a) (Kl a)
id = MkKleisli pure
(>) :: Kleisli m kl_a kl_b
-> Kleisli m kl_b kl_c
-> Kleisli m kl_a kl_c
MkKleisli one > MkKleisli two = MkKleisli (one >=> two)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment