{-# LANGUAGE DerivingVia #-}

{-# Language DataKinds                  #-}
{-# Language DeriveGeneric              #-}
{-# Language DerivingStrategies         #-}
{-# Language FlexibleInstances          #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language InstanceSigs               #-}
{-# Language MultiParamTypeClasses      #-}
{-# Language PolyKinds                  #-}
{-# Language ScopedTypeVariables        #-}
{-# Language StandaloneDeriving         #-}
{-# Language TypeApplications           #-}
{-# Language TypeFamilies               #-}
{-# Language TypeOperators              #-}
{-# Language UndecidableInstances       #-}
{-# Language EmptyDataDecls             #-}
{-# Language StandaloneKindSignatures   #-}

module Generic.Applicative 
  ( LeftBias(..)
  , RightBias(..)
  , Idiomatically
  , Generically1(..)
  , NewSums(..)
  , module Generic.Applicative.Idiom
  ) where

import Control.Applicative
import Data.Functor.Sum
import Data.Kind

import Generic.Applicative.Internal
import Generic.Applicative.Idiom

type    LeftBias :: tagKind -> (k -> Type) -> (k -> Type) -> (k -> Type)
newtype LeftBias tag f g a = LeftBias (Sum f g a)
 deriving newtype a -> LeftBias tag f g b -> LeftBias tag f g a
(a -> b) -> LeftBias tag f g a -> LeftBias tag f g b
(forall a b. (a -> b) -> LeftBias tag f g a -> LeftBias tag f g b)
-> (forall a b. a -> LeftBias tag f g b -> LeftBias tag f g a)
-> Functor (LeftBias tag f g)
forall tagKind (tag :: tagKind) (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
a -> LeftBias tag f g b -> LeftBias tag f g a
forall tagKind (tag :: tagKind) (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
(a -> b) -> LeftBias tag f g a -> LeftBias tag f g b
forall a b. a -> LeftBias tag f g b -> LeftBias tag f g a
forall a b. (a -> b) -> LeftBias tag f g a -> LeftBias tag f g b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> LeftBias tag f g b -> LeftBias tag f g a
$c<$ :: forall tagKind (tag :: tagKind) (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
a -> LeftBias tag f g b -> LeftBias tag f g a
fmap :: (a -> b) -> LeftBias tag f g a -> LeftBias tag f g b
$cfmap :: forall tagKind (tag :: tagKind) (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
(a -> b) -> LeftBias tag f g a -> LeftBias tag f g b
Functor

-- | An applicative instance of 'Data.Functor.Sum.Sum' biased to the
-- left.
--
-- It injects 'pure' into the 'InL' constructor:
--
-- @
--   pure = LeftBias . InL . pure
-- @
instance Idiom tag f g => Applicative (LeftBias tag f g) where
 pure :: a -> LeftBias tag f g a
 pure :: a -> LeftBias tag f g a
pure = Sum f g a -> LeftBias tag f g a
forall tagKind k (tag :: tagKind) (f :: k -> *) (g :: k -> *)
       (a :: k).
Sum f g a -> LeftBias tag f g a
LeftBias (Sum f g a -> LeftBias tag f g a)
-> (a -> Sum f g a) -> a -> LeftBias tag f g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> Sum f g a
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL (f a -> Sum f g a) -> (a -> f a) -> a -> Sum f g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

 liftA2 :: (a -> b -> c) -> (LeftBias tag f g a -> LeftBias tag f g b -> LeftBias tag f g c)
 liftA2 :: (a -> b -> c)
-> LeftBias tag f g a -> LeftBias tag f g b -> LeftBias tag f g c
liftA2 a -> b -> c
(·) (LeftBias (InL f a
as)) (LeftBias (InL f b
bs)) = Sum f g c -> LeftBias tag f g c
forall tagKind k (tag :: tagKind) (f :: k -> *) (g :: k -> *)
       (a :: k).
Sum f g a -> LeftBias tag f g a
LeftBias (Sum f g c -> LeftBias tag f g c)
-> Sum f g c -> LeftBias tag f g c
forall a b. (a -> b) -> a -> b
$ f c -> Sum f g c
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL (f c -> Sum f g c) -> f c -> Sum f g c
forall a b. (a -> b) -> a -> b
$ (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> b -> c
(·) f a
as f b
bs
 liftA2 a -> b -> c
(·) (LeftBias (InL f a
as)) (LeftBias (InR g b
bs)) = Sum f g c -> LeftBias tag f g c
forall tagKind k (tag :: tagKind) (f :: k -> *) (g :: k -> *)
       (a :: k).
Sum f g a -> LeftBias tag f g a
LeftBias (Sum f g c -> LeftBias tag f g c)
-> Sum f g c -> LeftBias tag f g c
forall a b. (a -> b) -> a -> b
$ g c -> Sum f g c
forall k (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR (g c -> Sum f g c) -> g c -> Sum f g c
forall a b. (a -> b) -> a -> b
$ (a -> b -> c) -> g a -> g b -> g c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> b -> c
(·) (f a -> g a
forall tagKind (tag :: tagKind) (f :: * -> *) (g :: * -> *).
Idiom tag f g =>
f ~> g
idiom @_ @tag f a
as) g b
bs
 liftA2 a -> b -> c
(·) (LeftBias (InR g a
as)) (LeftBias (InL f b
bs)) = Sum f g c -> LeftBias tag f g c
forall tagKind k (tag :: tagKind) (f :: k -> *) (g :: k -> *)
       (a :: k).
Sum f g a -> LeftBias tag f g a
LeftBias (Sum f g c -> LeftBias tag f g c)
-> Sum f g c -> LeftBias tag f g c
forall a b. (a -> b) -> a -> b
$ g c -> Sum f g c
forall k (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR (g c -> Sum f g c) -> g c -> Sum f g c
forall a b. (a -> b) -> a -> b
$ (a -> b -> c) -> g a -> g b -> g c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> b -> c
(·) g a
as (f b -> g b
forall tagKind (tag :: tagKind) (f :: * -> *) (g :: * -> *).
Idiom tag f g =>
f ~> g
idiom @_ @tag f b
bs)
 liftA2 a -> b -> c
(·) (LeftBias (InR g a
as)) (LeftBias (InR g b
bs)) = Sum f g c -> LeftBias tag f g c
forall tagKind k (tag :: tagKind) (f :: k -> *) (g :: k -> *)
       (a :: k).
Sum f g a -> LeftBias tag f g a
LeftBias (Sum f g c -> LeftBias tag f g c)
-> Sum f g c -> LeftBias tag f g c
forall a b. (a -> b) -> a -> b
$ g c -> Sum f g c
forall k (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR (g c -> Sum f g c) -> g c -> Sum f g c
forall a b. (a -> b) -> a -> b
$ (a -> b -> c) -> g a -> g b -> g c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> b -> c
(·) g a
as g b
bs

-- | An applicative instance of 'Data.Functor.Sum.Sum' biased to the
-- right.
--
-- It injects 'pure' into the 'InR' constructor:
--
-- @
--   pure = LeftBias . InR . pure
-- @
type    RightBias :: tagKind -> (k -> Type) -> (k -> Type) -> (k -> Type)
newtype RightBias tag f g a = RightBias (Sum f g a)
 -- deriving newtype Generic1
 deriving newtype a -> RightBias tag f g b -> RightBias tag f g a
(a -> b) -> RightBias tag f g a -> RightBias tag f g b
(forall a b.
 (a -> b) -> RightBias tag f g a -> RightBias tag f g b)
-> (forall a b. a -> RightBias tag f g b -> RightBias tag f g a)
-> Functor (RightBias tag f g)
forall tagKind (tag :: tagKind) (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
a -> RightBias tag f g b -> RightBias tag f g a
forall tagKind (tag :: tagKind) (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
(a -> b) -> RightBias tag f g a -> RightBias tag f g b
forall a b. a -> RightBias tag f g b -> RightBias tag f g a
forall a b. (a -> b) -> RightBias tag f g a -> RightBias tag f g b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> RightBias tag f g b -> RightBias tag f g a
$c<$ :: forall tagKind (tag :: tagKind) (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
a -> RightBias tag f g b -> RightBias tag f g a
fmap :: (a -> b) -> RightBias tag f g a -> RightBias tag f g b
$cfmap :: forall tagKind (tag :: tagKind) (f :: * -> *) (g :: * -> *) a b.
(Functor f, Functor g) =>
(a -> b) -> RightBias tag f g a -> RightBias tag f g b
Functor

instance Idiom tag g f => Applicative (RightBias tag f g) where
 pure :: a -> RightBias tag f g a
 pure :: a -> RightBias tag f g a
pure a
a = Sum f g a -> RightBias tag f g a
forall tagKind k (tag :: tagKind) (f :: k -> *) (g :: k -> *)
       (a :: k).
Sum f g a -> RightBias tag f g a
RightBias (g a -> Sum f g a
forall k (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR (a -> g a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a))

 liftA2 :: (a -> b -> c) -> (RightBias tag f g a -> RightBias tag f g b -> RightBias tag f g c)
 liftA2 :: (a -> b -> c)
-> RightBias tag f g a
-> RightBias tag f g b
-> RightBias tag f g c
liftA2 a -> b -> c
(·) (RightBias (InL f a
as)) (RightBias (InL f b
bs)) = Sum f g c -> RightBias tag f g c
forall tagKind k (tag :: tagKind) (f :: k -> *) (g :: k -> *)
       (a :: k).
Sum f g a -> RightBias tag f g a
RightBias (Sum f g c -> RightBias tag f g c)
-> Sum f g c -> RightBias tag f g c
forall a b. (a -> b) -> a -> b
$ f c -> Sum f g c
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL (f c -> Sum f g c) -> f c -> Sum f g c
forall a b. (a -> b) -> a -> b
$ (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> b -> c
(·) f a
as f b
bs
 liftA2 a -> b -> c
(·) (RightBias (InL f a
as)) (RightBias (InR g b
bs)) = Sum f g c -> RightBias tag f g c
forall tagKind k (tag :: tagKind) (f :: k -> *) (g :: k -> *)
       (a :: k).
Sum f g a -> RightBias tag f g a
RightBias (Sum f g c -> RightBias tag f g c)
-> Sum f g c -> RightBias tag f g c
forall a b. (a -> b) -> a -> b
$ f c -> Sum f g c
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL (f c -> Sum f g c) -> f c -> Sum f g c
forall a b. (a -> b) -> a -> b
$ (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> b -> c
(·) f a
as (g b -> f b
forall tagKind (tag :: tagKind) (f :: * -> *) (g :: * -> *).
Idiom tag f g =>
f ~> g
idiom @_ @tag g b
bs)
 liftA2 a -> b -> c
(·) (RightBias (InR g a
as)) (RightBias (InL f b
bs)) = Sum f g c -> RightBias tag f g c
forall tagKind k (tag :: tagKind) (f :: k -> *) (g :: k -> *)
       (a :: k).
Sum f g a -> RightBias tag f g a
RightBias (Sum f g c -> RightBias tag f g c)
-> Sum f g c -> RightBias tag f g c
forall a b. (a -> b) -> a -> b
$ f c -> Sum f g c
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL (f c -> Sum f g c) -> f c -> Sum f g c
forall a b. (a -> b) -> a -> b
$ (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> b -> c
(·) (g a -> f a
forall tagKind (tag :: tagKind) (f :: * -> *) (g :: * -> *).
Idiom tag f g =>
f ~> g
idiom @_ @tag g a
as) f b
bs
 liftA2 a -> b -> c
(·) (RightBias (InR g a
as)) (RightBias (InR g b
bs)) = Sum f g c -> RightBias tag f g c
forall tagKind k (tag :: tagKind) (f :: k -> *) (g :: k -> *)
       (a :: k).
Sum f g a -> RightBias tag f g a
RightBias (Sum f g c -> RightBias tag f g c)
-> Sum f g c -> RightBias tag f g c
forall a b. (a -> b) -> a -> b
$ g c -> Sum f g c
forall k (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR (g c -> Sum f g c) -> g c -> Sum f g c
forall a b. (a -> b) -> a -> b
$ (a -> b -> c) -> g a -> g b -> g c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> b -> c
(·) g a
as g b
bs

--

data Serve tag
instance (Idiom tag l l', Idiom tag' l' r') => Idiom (Serve tag) l (LeftBias tag' l' r') where
  idiom :: l ~> LeftBias tag' l' r'
  idiom :: l x -> LeftBias tag' l' r' x
idiom = Sum l' r' x -> LeftBias tag' l' r' x
forall tagKind k (tag :: tagKind) (f :: k -> *) (g :: k -> *)
       (a :: k).
Sum f g a -> LeftBias tag f g a
LeftBias (Sum l' r' x -> LeftBias tag' l' r' x)
-> (l x -> Sum l' r' x) -> l x -> LeftBias tag' l' r' x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. l' x -> Sum l' r' x
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL (l' x -> Sum l' r' x) -> (l x -> l' x) -> l x -> Sum l' r' x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tagKind (tag :: tagKind) (f :: * -> *) (g :: * -> *).
Idiom tag f g =>
f ~> g
forall (f :: * -> *) (g :: * -> *). Idiom tag f g => f ~> g
idiom @_ @tag 
instance (Idiom tag l l', Idiom tag' r' l') => Idiom (Serve tag) l (RightBias tag' l' r') where
  idiom :: l ~> RightBias tag' l' r'
  idiom :: l x -> RightBias tag' l' r' x
idiom = Sum l' r' x -> RightBias tag' l' r' x
forall tagKind k (tag :: tagKind) (f :: k -> *) (g :: k -> *)
       (a :: k).
Sum f g a -> RightBias tag f g a
RightBias (Sum l' r' x -> RightBias tag' l' r' x)
-> (l x -> Sum l' r' x) -> l x -> RightBias tag' l' r' x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. l' x -> Sum l' r' x
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL (l' x -> Sum l' r' x) -> (l x -> l' x) -> l x -> Sum l' r' x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tagKind (tag :: tagKind) (f :: * -> *) (g :: * -> *).
Idiom tag f g =>
f ~> g
forall (f :: * -> *) (g :: * -> *). Idiom tag f g => f ~> g
idiom @_ @tag 
instance (Applicative r, Idiom tag l' r, Idiom tag' r' l') => Idiom (Serve tag) (RightBias tag' l' r') r where
  idiom :: RightBias tag' l' r' ~> r
  idiom :: RightBias tag' l' r' x -> r x
idiom (RightBias (InL l' x
ls')) = l' x -> r x
forall tagKind (tag :: tagKind) (f :: * -> *) (g :: * -> *).
Idiom tag f g =>
f ~> g
idiom @_ @tag @l' @r l' x
ls'
  idiom (RightBias (InR r' x
rs')) = l' x -> r x
forall tagKind (tag :: tagKind) (f :: * -> *) (g :: * -> *).
Idiom tag f g =>
f ~> g
idiom @_ @tag @l' @r (r' x -> l' x
forall tagKind (tag :: tagKind) (f :: * -> *) (g :: * -> *).
Idiom tag f g =>
f ~> g
idiom @_ @tag' r' x
rs')

type
  Served :: [SumKind k] -> [SumKind k]
type family
  Served sums where
  Served '[]                  = '[]
  Served '[sum]               = '[sum]
  Served (LeftBias  tag:sums) = LeftBias  (Serve tag):Served sums
  Served (RightBias tag:sums) = RightBias (Serve tag):Served sums
  Served (sum:sums)           = sum:Served sums

-- | A modifier that is used to generically derive 'Applicative' for
-- sum types. 
-- 
-- Types with a single constructor can derive 'Applicative' using
-- @Generically1@ from @GHC.Generics@:
--
-- @
-- Generically1 f = Idiomatically f '[]
-- @
-- 
-- A datatype with multiple constructors requires more input from the
-- user: what constructor should be 'pure' and how to map between two
-- different constructors in a law-abiding way.
-- 
-- This is done by specifying the /appliative morphisms/ ('Idiom')
-- between each constructor.
-- 
-- 'Applicative' for 'Maybe' can be derived via the @Terminal@
-- applicative morphism, biased to the right. @RightBias Terminal@
-- means that when we lift over @Nothing@ and @Just@ it will result in
-- @Nothing@.
--
-- @
-- data Maybe a = Nothing | Just a
--   deriving 
--   stock Generic1
-- 
--   deriving (Functor, Applicative) 
--   via Idiomatically Maybe '[RightBias Terminal] 
-- @
--
-- The same description derives 'Applicative' for @ZipList@:
-- 
-- @
-- type ZipList :: Type -> Type
-- data ZipList a = ZNil | a ::: ZipList
--   deriving 
--   stock Generic1 
-- 
--   deriving (Functor, Applicative)
--   via Idiomatically ZipList '[RightBias Terminal]
-- @
type Idiomatically :: (k -> Type) -> [SumKind k] -> (k -> Type)
type Idiomatically f sums = Generically1 (NewSums (Served sums) f)