{-|
Module: Squeal.PostgreSQL.Session.Indexed
Description: indexed session monad
Copyright: (c) Eitan Chatav, 2019
Maintainer: eitan@morphism.tech
Stability: experimental

`Squeal.PostgreSQL.Indexed` provides an indexed monad transformer
class and a class extending it to run `Definition`s.
-}

{-# LANGUAGE
    DataKinds
  , DefaultSignatures
  , FlexibleContexts
  , FlexibleInstances
  , FunctionalDependencies
  , PolyKinds
  , MultiParamTypeClasses
  , QuantifiedConstraints
  , RankNTypes
  , TypeApplications
  , TypeFamilies
  , UndecidableInstances
#-}

module Squeal.PostgreSQL.Session.Indexed
  ( IndexedMonadTrans (..)
  , Indexed (..)
  , IndexedMonadTransPQ (..)
  , indexedDefine
  ) where

import Control.Category (Category (..))
import Control.Monad
import Control.Monad.IO.Class
import Control.Monad.Trans
import Data.Function ((&))
import Prelude hiding (id, (.))

import Squeal.PostgreSQL.Definition

{- | An [Atkey indexed monad]
(https://bentnib.org/paramnotions-jfp.pdf)
is a `Functor` [enriched category]
(https://ncatlab.org/nlab/show/enriched+category).
An indexed monad transformer transforms a `Monad` into an indexed monad,
and is a monad transformer when its source and target are the same,
enabling use of standard @do@ notation for endo-index operations.
-}
class
  ( forall i j m. Monad m => Functor (t i j m)
  , forall i m. Monad m => Monad (t i i m)
  , forall i. MonadTrans (t i i)
  ) => IndexedMonadTrans t where

  {-# MINIMAL pqJoin | pqBind #-}

  -- | indexed analog of `<*>`
  pqAp
    :: Monad m
    => t i j m (x -> y)
    -> t j k m x
    -> t i k m y
  pqAp t i j m (x -> y)
tf t j k m x
tx = ((x -> y) -> t j k m y) -> t i j m (x -> y) -> t i k m y
forall k (t :: k -> k -> (* -> *) -> * -> *) (m :: * -> *) x
       (j :: k) (k :: k) y (i :: k).
(IndexedMonadTrans t, Monad m) =>
(x -> t j k m y) -> t i j m x -> t i k m y
pqBind ((x -> y) -> t j k m x -> t j k m y
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t j k m x
tx) t i j m (x -> y)
tf

  -- | indexed analog of `join`
  pqJoin
    :: Monad m
    => t i j m (t j k m y)
    -> t i k m y
  pqJoin t i j m (t j k m y)
t = t i j m (t j k m y)
t t i j m (t j k m y)
-> (t i j m (t j k m y) -> t i k m y) -> t i k m y
forall a b. a -> (a -> b) -> b
& (t j k m y -> t j k m y) -> t i j m (t j k m y) -> t i k m y
forall k (t :: k -> k -> (* -> *) -> * -> *) (m :: * -> *) x
       (j :: k) (k :: k) y (i :: k).
(IndexedMonadTrans t, Monad m) =>
(x -> t j k m y) -> t i j m x -> t i k m y
pqBind t j k m y -> t j k m y
forall k (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

  -- | indexed analog of `=<<`
  pqBind
    :: Monad m
    => (x -> t j k m y)
    -> t i j m x
    -> t i k m y
  pqBind x -> t j k m y
f t i j m x
t = t i j m (t j k m y) -> t i k m y
forall k (t :: k -> k -> (* -> *) -> * -> *) (m :: * -> *) (i :: k)
       (j :: k) (k :: k) y.
(IndexedMonadTrans t, Monad m) =>
t i j m (t j k m y) -> t i k m y
pqJoin (x -> t j k m y
f (x -> t j k m y) -> t i j m x -> t i j m (t j k m y)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> t i j m x
t)

  -- | indexed analog of flipped `>>`
  pqThen
    :: Monad m
    => t j k m y
    -> t i j m x
    -> t i k m y
  pqThen t j k m y
pq2 t i j m x
pq1 = t i j m x
pq1 t i j m x -> (t i j m x -> t i k m y) -> t i k m y
forall a b. a -> (a -> b) -> b
& (x -> t j k m y) -> t i j m x -> t i k m y
forall k (t :: k -> k -> (* -> *) -> * -> *) (m :: * -> *) x
       (j :: k) (k :: k) y (i :: k).
(IndexedMonadTrans t, Monad m) =>
(x -> t j k m y) -> t i j m x -> t i k m y
pqBind (\ x
_ -> t j k m y
pq2)

  -- | indexed analog of `<=<`
  pqAndThen
    :: Monad m
    => (y -> t j k m z)
    -> (x -> t i j m y)
    -> x -> t i k m z
  pqAndThen y -> t j k m z
g x -> t i j m y
f x
x = (y -> t j k m z) -> t i j m y -> t i k m z
forall k (t :: k -> k -> (* -> *) -> * -> *) (m :: * -> *) x
       (j :: k) (k :: k) y (i :: k).
(IndexedMonadTrans t, Monad m) =>
(x -> t j k m y) -> t i j m x -> t i k m y
pqBind y -> t j k m z
g (x -> t i j m y
f x
x)

{- | `Indexed` reshuffles the type parameters of an `IndexedMonadTrans`,
exposing its `Category` instance.-}
newtype Indexed t m r i j = Indexed {Indexed t m r i j -> t i j m r
runIndexed :: t i j m r}
instance
  ( IndexedMonadTrans t
  , Monad m
  , Monoid r
  ) => Category (Indexed t m r) where
    id :: Indexed t m r a a
id = t a a m r -> Indexed t m r a a
forall k k k k (t :: k -> k -> k -> k -> *) (m :: k) (r :: k)
       (i :: k) (j :: k).
t i j m r -> Indexed t m r i j
Indexed (r -> t a a m r
forall (f :: * -> *) a. Applicative f => a -> f a
pure r
forall a. Monoid a => a
mempty)
    Indexed t b c m r
g . :: Indexed t m r b c -> Indexed t m r a b -> Indexed t m r a c
. Indexed t a b m r
f = t a c m r -> Indexed t m r a c
forall k k k k (t :: k -> k -> k -> k -> *) (m :: k) (r :: k)
       (i :: k) (j :: k).
t i j m r -> Indexed t m r i j
Indexed (t a c m r -> Indexed t m r a c) -> t a c m r -> Indexed t m r a c
forall a b. (a -> b) -> a -> b
$ t a b m (r -> r) -> t b c m r -> t a c m r
forall k (t :: k -> k -> (* -> *) -> * -> *) (m :: * -> *) (i :: k)
       (j :: k) x y (k :: k).
(IndexedMonadTrans t, Monad m) =>
t i j m (x -> y) -> t j k m x -> t i k m y
pqAp ((r -> r -> r) -> t a b m r -> t a b m (r -> r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap r -> r -> r
forall a. Semigroup a => a -> a -> a
(<>) t a b m r
f) t b c m r
g

{- | `IndexedMonadTransPQ` is a class for indexed monad transformers
that support running `Definition`s using `define` which acts functorially in effect.

* @define id = return ()@
* @define (statement1 >>> statement2) = define statement1 & pqThen (define statement2)@
-}
class IndexedMonadTrans pq => IndexedMonadTransPQ pq where
  define :: MonadIO io => Definition db0 db1 -> pq db0 db1 io ()

{- | Run a pure SQL `Definition` functorially in effect

* @indexedDefine id = id@
* @indexedDefine (def1 >>> def2) = indexedDefine def1 >>> indexedDefine def2@
-}
indexedDefine
  :: (IndexedMonadTransPQ pq, MonadIO io)
  => Definition db0 db1 -> Indexed pq io () db0 db1
indexedDefine :: Definition db0 db1 -> Indexed pq io () db0 db1
indexedDefine = pq db0 db1 io () -> Indexed pq io () db0 db1
forall k k k k (t :: k -> k -> k -> k -> *) (m :: k) (r :: k)
       (i :: k) (j :: k).
t i j m r -> Indexed t m r i j
Indexed (pq db0 db1 io () -> Indexed pq io () db0 db1)
-> (Definition db0 db1 -> pq db0 db1 io ())
-> Definition db0 db1
-> Indexed pq io () db0 db1
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Definition db0 db1 -> pq db0 db1 io ()
forall (pq :: SchemasType -> SchemasType -> (* -> *) -> * -> *)
       (io :: * -> *) (db0 :: SchemasType) (db1 :: SchemasType).
(IndexedMonadTransPQ pq, MonadIO io) =>
Definition db0 db1 -> pq db0 db1 io ()
define