Applicative (Sum f g) where

ApplicativeSum.markdown

Interesting https://www.reddit.com/r/haskell/comments/1u8rp1/with_two_different_functors/

Description of monoidal natural transformations https://gist.github.com/Icelandjack/9e6902690a244286843164e554a8c3db

http://sneezy.cs.nott.ac.uk/darcs/term/Idiomatics.lhs

There's a fairly predictable notion of homomorphism between Applicativefunctors: just pick any natural transformation which respects pure and <*>. There are far too many of these homomorphisms to leave them entirely automatic, so let's try having type-level proxies for them, aka named instances.

class (Applicative a, Applicative b) => AppHom h a b | h -> a b where
  appHom :: h -> a x -> b x

  appHom (pure x)   = pure x
  appHom (f <*> s)  = appHom f <*> appHom s

Guess what? Applicative homomorphisms induce a category of Applicative functors with an initial object...

data Applicative f => InitHom f = InitHom
instance Applicative f => AppHom (InitHom f) Id f where

  appHom :: Id x -> f x
  appHom _ (Id x) = pure x

...and this little chappie...

data (Applicative f, Monoid x) => MonHom f x = MonHom where
instance (Applicative f, Monoid x) => AppHom (MonHom f x) f (Const x) where
  appHom _ _ = Const zero

... which induces a terminal object when x is ().

We'd better have

data Applicative f => IdHom f = IdHom
instance Applicative f => AppHom (IdHom f) f f where
  appHom _ = id

data (Applicative f, Applicative h) => CompHom f h
  = forall g . (Applicative g, AppHom fg f g, AppHom gh g h) => CompHom fg gh
instance (Applicative f, Applicative h) => AppHom (CompHom f h) where
  appHom (CompHom fg gh) = appHom fg . appHom gh

We should check these two:

data (Applicative f, Applicative g) => InnerHom f g = InnerHom
instance (Applicative f, Applicative g) =>
  AppHom (InnerHom f g) g (Comp f g) where
    appHom _ c = Comp (pure c)
data (Applicative f, Applicative g) => OuterHom f g = OuterHom
instance (Applicative f, Applicative g) =>
  AppHom (OuterHom f g) f (Comp f g) where
    appHom _ c = Comp (iI pure c Ii)

It's not yet obvious if it's a good move to pull this stunt: we can't get away with either identity or composition of |AppHom|s.

instance Category (~~>) where
  id = A
  (.) = flip G

data a ~~> b where
  A :: a ~~> a
  B :: f ~~> Const x
  C :: f ~~> Compose f g
  D :: g ~~> Compose f g
  E :: Product f g ~~> f
  F :: Product f g ~~> g
  G :: a ~~> b
    -> b ~~> c
    -> a ~~> c
  H :: f ~~> f'
    -> f ~~> Product f f'
  I :: f ~~> f'
    -> f ~~> Product f' f
  J :: f ~~> f'
    -> Sum f' f ~~> f'
  K :: f ~~> f'
    -> g ~~> g'
    -> Product f g ~~> Product f' g'

data Coprod g h x = Inl (g x) | Inr (h x)

instance (Functor g, Functor h) => Functor (Coprod g h) where
  fmap f (Inl xg)  = Inl (fmap f xg)
  fmap f (Inr xh)  = Inr (fmap f xh)
instance (Traversable g,Traversable h) => Traversable (Coprod g h) where
  traverse f (Inl xg)  = iI Inl (traverse f xg) Ii
  traverse f (Inr xh)  = iI Inr (traverse f xh) Ii

More amusingly, an AppHom makes a Coprod Applicative, in a sense which keeps computations Inr if possible, but leaks them to Inl through appHom if necessary.

instance (AppHom a b) => Applicative (Coprod b a) where
  pure = Inr . pure
  Inr f  <*> Inr s  = Inr (f <*> s)
  Inr f  <*> Inl s  = Inl (appHom f <*> s)
  Inl f  <*> Inr s  = Inl (f <*> appHom s)
  Inl f  <*> Inl s  = Inl (f <*> s)

Actually, that's a lie: <*> here is too strict to obey the laws in some cases where a computation is ⊥. Do we care?

By definition, we have the following:

instance (AppHom a b) => AppHom a (Coprod b a) where
  appHom = Inr

Note that initiality induces an Applicative functor where pure computations are explicitly separated from impure.
Finality adds a one-point impurity. Put 'em together and you got Maybe.

Used in https://pdfs.semanticscholar.org/3a63/d782c6696f5243f5839ee9ce2a76fffab37f.pdf

data Faceted a = Raw a | Faceted Label (Faceted a) (Faceted a)

instance Applicative Faceted where
  pure x = Raw x
  Raw f <*> x = fmap f x
  Faceted k f g <*> x = Faceted k (f <*> x) (g <*> x)

instance Monad Faceted where
  return x = Raw x
  Raw x >>= f = f x
  Faceted k x y >>= f = Faceted k (x >>= f) (y >>= f)

type Faceted a = Lifted (Const Label * Faceted * Faceted) a

can we derive Monad

Maybe using ideal monads

ah duh, it's Free, point still holds

type Faceted = Free F

data F rest = F Label rest rest

data Tree a = Zero a | Succ (Tree (Node a))

data Node a = Node2 a a | Node3 a a a

but we want

class Natural f g where
  eta' :: f ~> g

instance Natural V3 V2 where
  eta' :: V3 ~> V2
  eta' (V3 a b c) = V2 a b
 
instance (Applicative f, Applicative g, Natural g f) => Applicative (Sum f g) where
  pure x = InR $ pure x

  InL ff <*> InL fx = InL      (ff <*>      fx)
  InR gf <*> InR gx = InR      (gf <*>      gx)
  InL ff <*> InR gx = InL      (ff <*> eta' gx)
  InR gf <*> InL fx = InL (eta' gf <*>      fx)

newtype Tree a = Tree (L.Lift (Tree :.: Node) a)
  deriving newtype
    (Functor, Applicative, Foldable, Foldable1)

newtype Node a = Node ((V2 :+: V3) a)
  deriving newtype
    (Functor, Applicative, Foldable, Foldable1)

instance Show a => Show (Tree a) where
  show = \case
    Zero a    -> printf "(S... %s)" (show a)
    Succ tree -> printf "(O... %s)" (show tree)

instance Show a => Show (Node a) where
  show (Node2 a b)   = printf "(%s %s)"    (show a) (show b)
  show (Node3 a b c) = printf "(%s %s %s)" (show a) (show b) (show c)

pattern Zero :: a -> Tree a
pattern Zero a = Tree (L.Pure a)

pattern Succ :: Tree (Node a) -> Tree a
pattern Succ tree = Tree (Other (Compose tree))

pattern Node2 :: a -> a -> Node a
pattern Node2 a b = Node (InL (V2 a b))

pattern Node3 :: a -> a -> a -> Node a
pattern Node3 a b c = Node (InR (V3 a b c))

newtype WGeneric f a = WGeneric (Sum (Rep1 f) f a)

instance (Generic1 f, g ~ Rep1 f) => Natural f g where
  eta' :: f ~> Rep1 f
  eta' = from1

deriving newtype instance 
  (Functor (Rep1 f), Functor f) 
  =>
  Functor (WGeneric f)

deriving newtype instance 
  (Generic1 f, Applicative (Rep1 f), Applicative f) 
  => 
  Applicative (WGeneric f)

Look into (from https://personal.cis.strath.ac.uk/conor.mcbride/so-pigworker.pdf)

class Swap m n where
  swap :: m (n a) -> n (m a)

instance (Swap g f, Monad f, Monad g) => Monad (Compose f g) where
  return = pure

  (>>=) :: forall a b. Compose f g a -> (a -> Compose f g b) -> Compose f g b
  Compose fga >>= k = Compose $ 
    fga >>= \ns -> 
      let nmnt :: g (f (g b))
          nmnt = fmap getCompose (ns >>= (return . k))

          res :: f (g b)
          res = join <$> Main.swap nmnt 

       in res 

newtype ArrayLike a = MkAL 
  (Product
    (Compose Maybe Data.Semigroup.Min)
    ((->) Int)
    a)
  deriving newtype
    (Functor, Applicative, Monad)

instance Swap Data.Semigroup.Min Maybe where
  swap :: Data.Semigroup.Min (Maybe a) -> Maybe (Data.Semigroup.Min a)
  swap = coerce

https://www.reddit.com/r/haskell/comments/6eck5p/are_applicativemonad_instances_possible_for_this/

https://ghc.haskell.org/trac/ghc/ticket/14266#comment:4

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module MultiInstance where

class MultiMonoid x a where
  multi'append :: a -> a -> a
  multi'empty :: a

data Addition
data Multiplication

instance MultiMonoid Addition Int where
  multi'append = (+)
  multi'empty  = 0

instance MultiMonoid Multiplication Int where
  multi'append = (*)
  multi'empty  = 1

example1, example2 :: Int
example1 = multi'append @Addition       2 3 -- 5
example2 = multi'append @Multiplication 2 3 -- 6

class MultiFoldable t where
  multi'foldMap :: forall x m a. (MultiMonoid x m) => (a -> m) -> t a -> m

instance MultiFoldable []
  where
    multi'foldMap :: forall x m a. (MultiMonoid x m) => (a -> m) -> [a] -> m
    multi'foldMap f = go
      where go :: [a] -> m
            go [] = multi'empty @x
            go (x:xs) = multi'append @x (f x) (go xs)

example3, example4 :: Int
example3 = multi'foldMap @[] @Addition       id [1,2,3,4] -- 10
example4 = multi'foldMap @[] @Multiplication id [1,2,3,4] -- 24

So we can do the same for Swap

class Sw (x :: Symbol) f g where
  sw :: g (f a) -> f (g a)

instance (Traversable t, Applicative f) => Sw "seq" f t where 
  sw :: t (f a) -> f (t a)
  sw = sequenceA

newtype Comp (tag :: Symbol) :: (k -> Type) -> (k' -> k) -> (k' -> Type) where
  Comp :: { getComp :: f (g a) } -> Comp tag f g a
  deriving stock
    Functor

instance (Applicative f, Applicative g) => Applicative (Comp tag f g) where
  pure = Comp . pure . pure
  Comp f <*> Comp x = Comp (liftA2 (<*>) f x)

instance (Sw tag f g, Monad f, Monad g) => Monad (Comp tag f g) where
  (>>=) :: forall a b. Comp tag f g a -> (a -> Comp tag f g b) -> Comp tag f g b
  Comp fga >>= k = Comp $ fga >>= \ns -> join <$> sw @tag (getComp <$> (ns >>= (return . k)))

I don't know if these satisfy laws, check later http://web.cecs.pdx.edu/~mpj/pubs/RR-1004.pdf (Composing monads)

newtype MM a = MM (Comp "seq" Maybe Maybe a)
  deriving newtype
    (Functor, Applicative, Monad)

the cool thing is that we are not restricted to that form

newtype MM a = MM (Maybe (Maybe a))
  deriving via (Comp "seq" Maybe Maybe a)
    (Functor, Applicative, Monad)

Referenced by derive via paper

https://stackoverflow.com/a/29454112/165806 read later

https://arxiv.org/pdf/0710.1120v1.pdf and http://web.cecs.pdx.edu/~mpj/pubs/RR-1004.pdf both

Idiom morphisms

http://hss.ulb.uni-bonn.de/2015/4178/4178.pdf

In order to compare computations in different idioms, we need some way of relating them. This is done by so called idiom morphisms, i.e., functions φ :: A x → B x satisfying the laws

φ (pure @A x)  = pure @B x
φ (u <*> @A v) = φ u <*> @B φ v

where A and B are idioms and the pure and (<*>) methods on the left (resp. right) hand side rely on the instances for A (resp. B).

An intuitive description is this: Applying an idiom morphism to an effectful computation is the same as applying the idiom morphism to every subcomputation. To get a feeling for what that actually means, let us discuss some examples, starting with the function
listToMaybe:

listToMaybe :: [a] -> Maybe a
listToMaybe []    = Nothing
listToMaybe (x:_) = Just x

This function connects nondeterminism to partiality by preserving failure and sending computations with multiple results to computations with only one result (i.e., the first one in the list). In both idioms a composite computation succeeds if every subcompu-
tation succeeds. In the list idiom the first result of a successful composite computation stems from combining the first results of the (necessarily also successful) subcomputations. The equations (3.10) and (3.11) can be checked easily and give a formal meaning
to computations in both idioms being related.

  listToMaybe (pure @[] a)
= listToMaybe [a]
= Just a
= pure @Maybe a

  listToMaybe (u <*> @[] v)
= ...
= listToMaybe u <*> @Maybe listToMaybe v

listToMaybe is an applicative morphism but not a monad morphism.

f :: M ~> M'

f (return x) = return x

f (a >>= b) = f a >>= f . b

https://www.cs.ox.ac.uk/ralf.hinze/publications/CSC.pdf

Every structure comes equipped with structure-preserving maps; so do idioms: a natural transformation h :: i ~> k is an idiom homomorphism iff

h (pure a) = pure a

h (x <*> y) = h x <*> h y

Idiom homomorphisms:

head :: Stream ~> Id
tail :: Stream ~> Stream -- idiom endomorphism

pure :: Id ~> Stream

tabulate :: Representable f => (Rep f ->) ~> f

--(?)
index :: Representable f => f ~> (Rep f -> )

Idiom homomorphisms: Lifting Operators and Laws

http://www.cs.ox.ac.uk/ralf.hinze/publications/CEFP09.pdf

Every structure comes equipped with structure-preserving maps; so do idioms: a polymorphic function h :: F ~> G is called an idiom homomorphism if and only if it preserves the idiomatic structure:

h (pure a) = pure a
h (x <*> y) = h x <*> h y

The function pure :: Id ~> F itself is a homomorphism from the identity idiom Id to the idiom F. Condition (2) for pure is equivalent to the homomorphism law, hence its name.

http://www.cs.ox.ac.uk/jeremy.gibbons/publications/ringads.pdf

The well-behaved operations over monadic values are called the algebras for that monad—functions k such that k . return = id and k . mult = k . fmap k. In particular, join is itself a monad algebra.

type Algebra f a = f a -> a

join :: Monad m => Algebra m (m a)

"Perfect Trees and Bit-reversal Permutations" (Ralf Hinze) points out that functor composition distributes left through sums

-- iso
Compose (Sum g g') f <~> Sum (Compose g f) (Compose g' f)

but distributing right goes one way,

Sum (Compose f g) (Compose f g') ~> Compose f (Sum g g')

But when does this make sense?

from' :: AppHom g g' -> Compose Pair (Sum g g') a -> Sum (Compose Pair g) (Compose Pair g') a
from' nat (Compose (InL xs  :# InL ys)) = InL (Compose (xs :# ys))
from' nat (Compose (InL xs  :# InR ys)) = InR (Compose (nat xs :# ys))
from' nat (Compose (InR xs  :# InL ys)) = InR (Compose (xs :# nat ys))
from' nat (Compose (InR xs  :# InR ys)) = InR (Compose (xs :# ys))