Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
ImplicationConstraints

To allow hask

type Cat k = k -> k -> Type

type Fun i j = i -> j

data Nat :: Cat i -> Cat j -> Cat (Fun i j) where
  Nat :: (FunctorOf cat cat' f, FunctorOf cat cat' f') => (forall a. Ob cat a => cat' (f a) (f' a)) -> Cat cat cat' f f'

type (~>) = Nat (->) (->)
data (~>) :: Cat (Type -> Type) where
  N :: (FunctorOf (->) (->) f, FunctorOf (->) (->) f') 
    => (forall a. f a -> f' a) 
    -> f ~> f'

to be used as liftCoT0M :: (Comonad w, Monad m) => (forall a. w a -> m s) -> CoT w m s

data (~??>) :: Cat (Type -> Type) where
  CM :: (Comonad w, Monad m) 
     => (forall a. w a -> m a) 
     -> w ~??> m

where every ~??> implies ~> since both Comonad, Monad have Funtors as superclasses..

to :: w ~??> m 
   -> w  ~>  m
to (CM nat) = Nat nat

from :: (Comonad w, Monad m) 
     => w  ~>  m
     -> w ~??> m 
from (Nat nat) = CM nat

hell could be defined

data (~??>) :: Cat (Type -> Type) where
  CM :: (Comonad w, Monad m) 
     => w  ~> m 
     -> w ~??> m
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Jun 19, 2017

Making the implementation wrapping and unwrapping ~??>

to :: w ~??> m 
   -> w  ~>  m
to (CM nat) = nat

from :: (Comonad w, Monad m) 
     => w  ~>  m
     -> w ~??> m 
from = CM 
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Jun 19, 2017

So now the tricky part is, I want subsumption between them. This requires ImplicationConstraints, I believe this monstrosity could be it

type Constr i j = (i -> j) -> Constraint

data Nat :: Cat i -> Cat j -> Constr i j -> Constr i j -> Cat (Fun i j) where
  Nat :: (ctx f, ctx' f') => (forall a. Ob cat a => cat' (f a) (f' a)) -> Nat cat cat' ctx ctx' f f'

-- ?
instance (Category cat, Category cat') => Category (Nat_ cat cat' ctx ctx') where
  type Ob (Nat_ cat cat' ctx ctx') = ctx & ctx

Okay so, now we can specify, “is at least a” for both of the constraints

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Jun 19, 2017

sigh, think about it later..

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Jun 19, 2017

Yuck what am I thinking

type family Ctx  (b::Bool) (cat :: Cat i) (cat' :: Cat j) :: Fun i j -> Constraint
type family Ctx' (b::Bool) (cat :: Cat i) (cat' :: Cat j) :: Fun i j -> Constraint

data Nat_ :: Bool -> Cat i -> Cat j -> Cat (Fun i j) where
  Nat_ :: (Ctx b cat cat' f, Ctx' b cat cat' f') 
       => (forall a. Ob cat a => cat' (f a) (f' a)) 
       -> Nat_ b cat cat' f f'
 
type instance Ctx  False (->) (->) = Comonad
type instance Ctx' False (->) (->) = Monad

type instance Ctx  True (->) (->) = Functor
type instance Ctx' True (->) (->) = Functor
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment