Mokhov.hs

-- Selective
class Applicative f => Selective f where
    select :: f (Either a b) -> f (a -> b) -> f b

apS :: Selective f => f (a -> b) -> f a -> f b
apS f x = select (Left <$> f) ((&) <$> x)

-- Free Selective
data Select f a where
    Pure :: a -> Select f a
    Select :: Select f (Either a b) -> f (a -> b) -> Select f b

instance Functor f => Functor (Select f) where
    fmap f (Pure a) = Pure (f a)
    fmap f (Select x y) = Select (fmap f <$> x) (fmap f <$> y) -- Free theorem from Fig. 4

instance Functor f => Applicative (Select f) where
    pure = Pure
    (<*>) = apS -- Law of rigid selective functors

instance Functor f => Selective (Select f) where
    select x (Pure y) = either y id <$> x -- Generalised identity
    select x (Select y z) = Select (select (f <$> x) (g <$> y)) (h <$> z) -- Associativity
      where
        f x' = Right <$> x'
        g y' = \a -> bimap (\x' -> (x',a)) ($ a) y'
        h z' = uncurry z'

-- Tensor product?
--
-- compare to this version of Day product:
--
--   data Day f g a where
--       (:<**>:) :: f x -> g (x -> a) -> Day f g a
--
data Mokhov f g a where
    (:<*?:) :: g (Either a x) -> f (a -> x) -> Mokhov f g x


-- Conversions work out
fromSelect :: Select f a -> Free Mokhov Identity f a
fromSelect (Pure a)     = Done (Identity a)
fromSelect (Select x y) = More (fromSelect x :<*?: y)

toSelect :: Free Mokhov Identity f a -> Select f a
toSelect (Done (Identity a)) = Pure a
toSelect (More (x :<*?: y)) = Select (toSelect x) y

instance HBifunctor Mokhov where
    bfmap = undefined
    hbimap f g (x :<*?: y) = g x :<*?: f y

instance Tensor Mokhov where
    type I Mokhov = Identity

    -- I'm not sure about these
    intro1 fx = Identity (Left ()) :<*?: fmap const fx
    intro2 gx = fmap Left gx :<*?: Identity id

    elim1 (Identity x :<*?: y) = case x of
        Left x' -> fmap ($ x') y 
        Right x' -> error "doesn't quite work"

    elim2 (x :<*?: Identity y) = fmap (either y id)x

    assoc ((x :<*?: y) :<*?: z) = error "I'm lazy" -- _ :<*?: (_ :<*?: _)
    disassoc = error "I'm lazy"

-- Less obscure Tensor
--
-- Recall that  usually Day is defined as:
-- i.e. like liftA2, not <**>
-- 
-- data Day f g a where
--    Day :: f b -> g c -> (b -> c -> a) -> Day f g a
--


data Mokhov' f g a where
    Mokhov :: (Either b (a,c) -> r) -> g (Either a b) -> f c -> Mokhov' f g r

toMokhov' :: (Functor f, Functor g) => Mokhov f g a -> Mokhov' f g a
toMokhov' (x :<*?: y) = Mokhov f x y
  where
    f :: Either x (y, y -> x) -> x
    f = either id (uncurry (&))

fromMokhov' :: (Functor g, Functor f) => Mokhov' f g a -> Mokhov f g a
fromMokhov' (Mokhov f x y) =
    fmap (fmap (f . Left)) x :<*?:
    fmap (curry (f . Right . swap)) y