{{ message }}

Instantly share code, notes, and snippets.

# Icelandjack/Ran.markdown

Last active Nov 13, 2020
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)

(>>=) :: forall a b. Same p f a -> (a -> Same p f b) -> Same p f b
(>>=) = coerce ((>>>=) @p @f @f @a @f @b)```

### Icelandjack commented Aug 24, 2017 • edited

 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 commented Aug 24, 2017 • edited

 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 commented Aug 24, 2017 • edited

 So we can implement a `Swap`ping `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 commented Aug 24, 2017 • edited

 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)```

## 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

so it feels right

### 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 commented Aug 24, 2017 • edited

 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 commented Aug 24, 2017 • edited

 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 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 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 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 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 commented Aug 25, 2017

 We are even able to coerce from our `Cod` to the library one `coerce :: Cod ~~> Codensity`

### 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 commented Sep 21, 2017 • edited

 We can probably do the same with `IxState`, ```newtype IxState i j a = IxState { runIxState :: i -> (a, j) } instance IxMonad IxState```

### 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 commented Sep 23, 2017 • edited

 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 }` ```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 commented Nov 27, 2017 • edited

 Edit: See `IxC` (indexed codensity monad) from Session types in Cloud Haskell Thesis: Note argument order, compare to `Ran`