Skip to content

Instantly share code, notes, and snippets.

@Icelandjack
Last active Nov 13, 2020
Embed
What would you like to do?
Right Kan extensions and Indexed Monads

reddit discussion

IxMonad implies Monad for (EDIT: Exists as LowerIx with newtype LiftIx m i j a = LiftIx (m a))

and `

newtype Same :: (k -> k -> k' -> Type) -> (k -> k' -> Type) where
  Same :: p f f a -> Same p f a

(EDIT: Same fits the same kind pattern as Join :: (k -> k -> Type) -> (k -> Type), we can unify when #12369 lands)

where we can coerce the instances (TODO: I want to be able to derive this)

instance IxFunctor p => Functor (Same p f) where
  fmap :: forall a b. (a -> b) -> (Same p f a -> Same p f b)
  fmap = coerce (imap @p @a @b @f @f)

instance IxApplicative p => Applicative (Same p f) where
  pure :: forall a. a -> Same p f a
  pure = coerce (ireturn @p @a @f)

  (<*>) :: forall a b. Same p f (a -> b) -> Same p f a -> Same p f b
  (<*>) = coerce (iap @p @f @f @a @b @f)

instance IxMonad p => Monad (Same p f) where
  (>>=) :: forall a b. Same p f a -> (a -> Same p f b) -> Same p f b
  (>>=) = coerce ((>>>=) @p @f @f @a @f @b)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Aug 24, 2017

I was playing around with right Kan extensions

newtype Ran g h a = Ran (forall xx. (a -> g xx) -> h xx)

which is the same as Codensity when the functors are the same, Codensity m a = Ran m m a

newtype Codensity m a = Codensity (forall xx. (a -> m xx) -> m xx)

only Codensity m has many more instances than Ran g h so I was experimenting, what happens when you take Codensity methods

(<*>) :: Codensity m (a -> b) -> Codensity m a -> Codensity m b
Codensity f <*> Codensity g = Codensity (\bfr -> f (\ab -> g (bfr . ab)))

and replace with Ran constructors; this is the inferred type

app :: Ran j i (a -> b) -> Ran k j a -> Ran k i b
Ran f `app` Ran g = Ran (\bfr -> f (\ab -> g (bfr . ab)))

Note that this is a more general version of the Codensity version, which was effectively Ran m m (a -> b) -> Ran m m a -> Ran m m b.

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Aug 24, 2017

Now I had a wee think, this looks an awful lot like an indexed applicative

iap :: m i j (a -> b) -> m j k a -> m i k b

with swapped indexes

class IxPointed m => IxApplicativeSwap m where
  iapSwap :: m j i (a -> b) -> m k j a -> m k i b

so while we can make Ran an instance of

instance IxFunctor Ran where
  imap :: forall a b j k. (a -> b) -> (Ran j k a -> Ran j k b)
  imap = fmap @(Ran j k) @a @b

instance IxPointed Ran where
  ireturn :: forall a i. a -> Ran i i a
  ireturn = coerce (return @(Codensity i) @a)

we cannot make it an instance of IxApplicative, we must make it an instance of IxApplicativeSwap

instance IxApplicativeSwap Ran where
  iapSwap :: Ran j i (a -> b) -> Ran k j a -> Ran k i b
  Ran f `iapSwap` Ran g = Ran (\bfr -> f (\ab -> g (bfr . ab)))
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Aug 24, 2017

So we can implement a Swapping newtype

newtype Swap :: (k -> k' -> k'' -> Type) -> (k' -> k -> k'' -> Type) where
  Swap :: p g f a -> Swap p f g a
instance IxFunctor f => IxFunctor (Swap f) where
  imap :: forall a b j k. (a -> b) -> (Swap f j k a -> Swap f j k b)
  imap = coerce (imap @f @a @b @k @j)

instance IxPointed f => IxPointed (Swap f) where
  ireturn :: forall a i. a -> Swap f i i a
  ireturn = coerce (ireturn @f @a @i)

instance IxApplicative m => IxApplicativeSwap (Swap m) where
  iapSwap :: forall j i a b k. Swap m j i (a -> b) -> Swap m k j a -> Swap m k i b
  iapSwap = coerce (iap @m @i @j @a @b @k)

instance IxApplicativeSwap m => IxApplicative (Swap m) where
  iap :: forall i j k a b. Swap m i j (a -> b) -> Swap m j k a -> Swap m i k b
  iap = coerce (iapSwap @m @j @i @a @b @k)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Aug 24, 2017

Can we do the same with (>>=) @(Codensity _)? Let's find out

f >>-> k = runCodensity f k

bindCod :: (a -> Codensity m b) -> (Codensity m a -> Codensity m b)
bindCod k ma = Codensity $ \return -> 
  ma  >>-> \a -> 
  k a >>-> \b ->
  return b

Inferred type:

f >>-- k = runRan f k

bindRan :: (a -> Ran k j b) -> (Ran j i a -> Ran k i b)
bindRan k ma = Ran $ \return -> 
  ma  >>-- \a -> 
  k a >>-- \b ->
  return b

This calls for the same thing

class IxApplicativeSwap m => IxMonadSwap m where
  ibindSwap :: (a -> m k j b) -> (m j i a -> m k i b)

instance IxMonadSwap Ran where
  ibindSwap :: (a -> Ran k j b) -> (Ran j i a -> Ran k i b)
  ibindSwap = bindRan

instance IxMonad m => IxMonadSwap (Swap m) where
  ibindSwap :: forall a k j b i. (a -> Swap m k j b) -> (Swap m j i a -> Swap m k i b)
  ibindSwap = coerce (ibind @m @a @j @k @b @i)

instance IxMonadSwap m => IxMonad (Swap m) where
  ibind :: forall a j k b i. (a -> Swap m j k b) -> (Swap m i j a -> Swap m i k b)
  ibind = coerce (ibindSwap @m @a @k @j @b @i)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Aug 24, 2017

What does this give us?

Now we can derive Applicative and Monad for Codensity

newtype Cod m a = Cod (Same (Swap Ran) m a)
  deriving newtype
    (Functor, Applicative, Monad)

so it feels right

@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Aug 24, 2017

Now for the dual version we have left kan extensions

data Lan :: (k -> Type) -> (k -> Type) -> (Type -> Type) where
  Lan :: (g xx -> a) -> h xx -> Lan g h a

which is an indexed Functor the same way as before, using the regular Functor (because forall i j. Functor (Lan i j))

instance IxFunctor Lan where
  imap :: (a -> a') -> (LAN j k a -> LAN j k a')
  imap = fmap

moving on to Copointed, Density f has a lovely terse instance, so what does the type of extractLam look like?

instance Copointed (Density f) where
  extract :: Density f a -> f a
  extract (Density f a) = f a

extractLan :: Lan i i a -> a
extractLan (Lan f a) = f a

which fits the type of IxCopointed

class IxFunctor w => IxCopointed w where
  iextract :: w i i a -> a

instance IxCopointed Lan where
  iextract :: Lan i i a -> a
  iextract = extractLan
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Aug 24, 2017

Now for Comonad

instance Comonad (Density f) where
  duplicate :: Density f a -> Density f (Density f a)
  duplicate (Density f ws) = Density (Density f) ws

duplicateLan :: Lan k i a -> Lan j i (Lan k j a)
duplicateLan (Lan f ws) = Lan (Lan f) ws
class IxCopointed w => IxComonad w where
  iextend    :: (w j k a -> b) -> w i k a -> w i j b
  iduplicate :: w i k a -> w i j (w j k a)

class IxCopointed w => IxComonadSwap w where
  iextendSwap :: (w k j a -> b) -> (w k i a -> w j i b)
  iextendSwap f = imap f . iduplicateSwap

  iduplicateSwap :: w k i a -> w j i (w k j a)
instance IxComonadSwap Lan where
  iduplicateSwap :: Lan k i a -> Lan j i (Lan k j a)
  iduplicateSwap = duplicateLan
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Aug 24, 2017

Okay now things start getting funky:

instance MonadTrans Codensity where
  lift :: Monad m => m ~> Codensity m
  lift m = Codensity (=<< m)

for Ran this would be this I guess

liftRan :: IxMonad m => m i j a -> Ran (m j xx) (m i xx) a
liftRan m = Ran (`ibind` m)

or we can make a new Ran to fit ibind to mimic the similarities between (=<< ma) and Codensity

(=<< ma)  :: Monad m => (forall xx. (a -> m xx) -> m xx)
Codensity ::            (forall xx. (a -> m xx) -> m xx) -> Codensity m a
newtype Ran2 :: (k -> k' -> k'' -> Type) -> (k -> k -> Type -> Type) where
  Ran2 :: (forall xx yy. (a -> m j xx yy) -> m i xx yy) -> Ran2 m i j a

type f ~~~> g = forall xx yy zz. f xx yy zz -> g xx yy zz

class IxMonadTrans t where
  ilift :: IxMonad m => m ~~~> t m

instance IxMonadTrans Ran2 where
  ilift :: IxMonad m => m ~~~> Ran2 m
  ilift m = Ran2 (`ibind` m)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Aug 24, 2017

This works for IxMonadZero and IxMonadPlus as well

class IxMonad m => IxMonadZero m where
  imzero :: m i j a

class IxMonadZero m => IxMonadPlus m where
  implus :: m i j a -> m i j a -> m i j a

but because we are dealing with IxMonadSwap super classes I suppose we need to duplicate IxMonadZero & IxMonadPlus as well

class IxMonadSwap m => IxMonadZeroSwap m where
  imzeroSwap :: m i j a

class IxMonadZeroSwap m => IxMonadPlusSwap m where
  implusSwap :: m i j a -> m i j a -> m i j a

but let's skip that and just use Alternative

instance Alternative v => Alternative (Codensity v) where
  empty = Codensity (\_ -> empty)
  Codensity m <|> Codensity n = Codensity (\k -> m k <|> n k)

and we can use the same trick (adding some random constraints)

class IxApplicative f => IxAlternative f where
  iempty :: (Alternative i, Alternative j) => f i j a

  (<|.|>) :: (Alternative i, Alternative j) => f i j a -> f i j a -> f i j a

instance IxAlternative Ran where
  iempty :: (Alternative i, Alternative j) => Ran i j a
  iempty = Ran (\_ -> empty)

  (<|.|>) :: (Alternative i, Alternative j) => Ran i j a -> Ran i j a -> Ran i j a
  Ran m <|.|> Ran n = Ran (\k -> m k <|> n k)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Aug 24, 2017

Wait there is an IxMonadTrans

-- IxMonadTrans :: ((Type -> Type) -> (k -> k -> Type -> Type)) -> Constraint
class IxMonadTrans t where
  ilift :: Monad m => m ~> t m i i
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Aug 25, 2017

okay and it's not compatible with Ran, no idea if IxMonadFixSwap does anything interesting

class IxMonad m => IxMonadFix m where
  imfix :: (a -> m i i a) -> m i i a

class IxMonadSwap m => IxMonadFixSwap m where
  imfixSwap :: (a -> m i i a) -> m i i a

instance IxMonadFixSwap Ran where
  imfixSwap :: (a -> Ran i i a) -> Ran i i a
  imfixSwap f = fix (ibindSwap f)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Aug 25, 2017

class IxComonadTrans t where
  ilower :: Comonad w => t w w a -> w a

instance IxComonadTrans Lan where
  ilower :: Comonad w => Lan w w a -> w a
  ilower (Lan f c) = extend f c

instance IxComonadTrans p => ComonadTrans (Same p) where
  lower :: forall w a. Comonad w => Same p w a -> w a
  lower = coerce (ilower @p @w @a)

instance IxComonad w => Comonad (Same w i) where
  duplicate :: forall a. Same w i a -> Same w i (Same w i a)
  duplicate (Same wiia) = Same a <&> Same where

    a :: forall xx. w i xx (w xx i a)
    a = iduplicate wiia

instance IxCopointed w => IxCopointed (Swap w) where
  iextract :: Swap w i i a -> a
  iextract (Swap f) = iextract f

instance IxComonadSwap w => IxComonad (Swap w) where
  iduplicate :: forall i k j a. Swap w i k a -> Swap w i j (Swap w j k a)
  iduplicate (Swap wika) = Swap (iextendSwap Swap wika)

instance IxComonadTrans l => IxComonadTrans (Swap l) where
  ilower :: Comonad i => Swap l i i ~> i
  ilower (Swap liia) = ilower liia

and now we can finally derive some stuff, I can't say it's worth it but it was fun

newtype Dens m a = Dens { runDesn :: Same (Swap Lan) m a }
  deriving newtype
    (Functor, Comonad, ComonadTrans)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Aug 25, 2017

We are even able to coerce from our Cod to the library one

coerce :: Cod ~~> Codensity
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Aug 25, 2017

and also for Dens if Density were a newtype

newtype Density m a = Density (Lan m m a)

coerce :: Dens ~~> Density
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Sep 21, 2017

We can probably do the same with IxState,

newtype IxState i j a = IxState { runIxState :: i -> (a, j) }

instance IxMonad IxState
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Sep 23, 2017

newtype SameKleisli m a = SameKleisli (Join (Kleisli m) a)
  deriving newtype
    Monoid

instance Category m => Semigroup (Join m a) where
  Join a <> Join b = Join (a . b)

instance Category m => Monoid (Join m a) where
  mempty = Join id

  Join a `mappend` Join b = Join (a . b)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Sep 23, 2017

We can do the """same""" to Control.Monad.Co

newtype CoT' w m' m a = CoT' { runCoT' :: forall r. w (a -> m' r) -> m r }

see http://try.purescript.org/?backend=core&gist=f258eb0faa597465ddce929a6287454d&session=452f70f3-426a-3cfa-dba3-4ecb576a6498

module Main where

import Prelude

import Control.Monad.Eff (Eff)
import Control.Monad.Eff.Console (logShow)
import Data.Const (Const(..))
import Data.Exists (Exists, mkExists, runExists)
import Data.Tuple (Tuple(..))
import TryPureScript (render, withConsole)

-- Here is a pretty lightweight encoding of linear lambda calculus.

-- Linear lambda calculus is the internal language of symmetric monoidal categories,
-- so I'm going to pick one particular symmetric monoidal category to encode my
-- terms in a HOAS style, and parametricity should ensure that I can't represent any
-- non-linear things (try it!)

-- The category I use is the category of functors with natural transformations as the
-- morphisms and Day convolution as the tensor. So tuples are encoded using Day, and 
-- functions are encoded using the internal hom which is right adjoint to Day.

-- I do need to provide some boilerplate terms such as the `\f g -> f (g unit)` here,
-- but those could probably even be filled in by a smart enough compiler
-- (typed holes PRs are welcome :)

test :: forall f a. (f  f  f  f) Unit
test = hom \f1 -> hom \f2 -> day (\f g -> f (g unit)) f2 f1

-- This representation is polymorphic in `f`, so I can't look inside and deconstruct the
-- functor in order to cheat.

-- However, if I want to turn my linear terms back into regular functions, I can do that by
-- instantiating all functors to constant functors, since `Day` acts on constant functors
-- by tupling up the constants, and the internal hom acts like a regular unrestricted function.

test1 :: forall a. a -> a -> Tuple a a
test1 a1 a2 = let x = test `apply_` a1 `apply_` a2 in Tuple (fst_ x) (snd_ x)

main :: Eff _ Unit
main = render =<< withConsole do
  logShow (test1 1 2)

-- Implementation details - Day and its internal hom

data Day1 f g a x y = Day1 (x -> y -> a) (f x) (g y)
data Day2 f g a x = Day2 (Exists (Day1 f g a x))
data Day f g a = Day (Exists (Day2 f g a))

infixl 6 type Day as 

runDay :: forall f g a r. (forall x y. (x -> y -> a) -> f x -> g y -> r) -> Day f g a -> r
runDay f (Day e) = runExists (\(Day2 e1) -> runExists (\(Day1 get fx gy) -> f get fx gy) e1) e

day :: forall f g a x y. (x -> y -> a) -> f x -> g y -> Day f g a
day get fx gy = Day (mkExists (Day2 (mkExists (Day1 get fx gy))))

newtype Hom f g a = Hom (forall r. f (a -> r) -> g r)

infixr 5 type Hom as 

hom :: forall f g a. (forall r. f (a -> r) -> g r) -> Hom f g a
hom = Hom

runHom :: forall f g a r. Hom f g a -> f (a -> r) -> g r
runHom (Hom f) = f

-- Constant functor helpers

apply_ h a = runHom h (Const a)

fst_ = runDay (\_ (Const x) _ -> x)

snd_ = runDay (\_ _ (Const x) -> x)
@Icelandjack

This comment has been minimized.

Copy link
Owner Author

@Icelandjack Icelandjack commented Nov 27, 2017

Edit:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment