rel8.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE UndecidableInstances #-}

module Brossa.Authorization where

-- brossa-specific

import qualified Brossa.DB.Rel8 as BrossaRel8
import qualified Brossa.DB.Hasql as BrossaHasql

-- generic

import Control.Monad
import Data.Int
import Data.Function (on)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as M
import Data.Text (Text)
import qualified Data.Text as T
import Data.Typeable
import GHC.Generics
import qualified Rel8
import Prelude hiding (id)

--------------------------------------------------------------------------------
-- Final tagless semantics

class ExprSemantics expr where
  (==.) :: (Eq a, Rel8.Sql Rel8.DBEq a) => SomeExpr expr a -> SomeExpr expr a -> SomeExpr expr Bool
  true :: SomeExpr expr Bool
  false :: SomeExpr expr Bool
  not_ :: SomeExpr expr Bool -> SomeExpr expr Bool

class LitSemantics expr a where
  lit :: a -> SomeExpr expr a

class (Monad query, ExprSemantics expr) => QuerySemantics query expr | query -> expr where
  each :: (Typeable t, Lift expr t) => Rel8.TableSchema (t Rel8.Name) -> query (t (SomeExpr expr))
  where_ :: SomeExpr expr Bool -> query ()
  limit :: Word -> query a -> query a

--------------------------------------------------------------------------------
-- Rel8 interpretation type-level parts

instance ExprSemantics Rel8.Expr where
  (==.) x y = some $ on (Rel8.==.) unsome x y
  true = some Rel8.true
  false = some Rel8.false
  not_ = some . Rel8.not_ . unsome

instance Rel8.Serializable (Rel8.Expr a) a => LitSemantics Rel8.Expr a where
  lit = some . Rel8.lit

instance QuerySemantics Rel8.Query Rel8.Expr where
  each = fmap lift . Rel8.each
  where_ = Rel8.where_ . unsome
  limit = Rel8.limit

--------------------------------------------------------------------------------
-- Tagged initial encoding type-level parts

-- Tagged ADT

data Expr a where
  (:==.) :: Eq a => Expr a -> Expr a -> Expr Bool
  True' :: Expr Bool
  False' :: Expr Bool
  Not :: Expr Bool -> Expr Bool
  Lit :: a -> Expr a

data Query a where
  Each :: (Typeable t) => Rel8.TableSchema (t Rel8.Name) -> Query (t Expr)
  Where :: Expr Bool -> Query ()
  Limit :: Word -> Query a -> Query a
  Bind :: Query a -> (a -> Query b) -> Query b
  Pure :: a -> Query a

-- Classes:

instance ExprSemantics Expr where
  (==.) x y = some $ on (:==.) unsome x y
  true = some True'
  false = some False'
  not_ = some . Not . unsome

instance LitSemantics Expr a where
  lit = some . Lit

instance QuerySemantics Query Expr where
  each = fmap lift . Each
  where_ = Where . unsome
  limit = Limit

instance Functor Query where
  fmap = liftM

instance Monad Query where
  return = pure
  (>>=) = Bind

instance Applicative Query where
  (<*>) = ap
  pure = Pure

--------------------------------------------------------------------------------
-- Someness wrapper

-- You need this wrapper because type inference on table.field does
-- not work because the type family `Column` yields `Couldn't match
-- type Column expr a against expr a'.
--
-- To get around this inference problem, we just wrap everything in a
-- newtype, and then the type family works fine.

newtype SomeExpr expr a = SomeExpr (expr a)

instance LitSemantics expr a => LitSemantics (SomeExpr expr) a where
  lit = some . lit

instance ExprSemantics expr => ExprSemantics (SomeExpr expr) where
  true = some true
  false = some false
  not_ = some . not_ . unsome
  (==.) x y = some $ on (==.) unsome x y

some :: expr a -> SomeExpr expr a
some e = SomeExpr e

unsome :: SomeExpr expr a -> expr a
unsome (SomeExpr e) = e

--------------------------------------------------------------------------------
-- Lifting tables

-- | With some Generics-based magic, this could be derived.
class Rel8.Rel8able t => Lift expr t where
  lift :: t expr -> t (SomeExpr expr)
  unlift :: t (SomeExpr expr) -> t expr

--------------------------------------------------------------------------------
-- Interpretation of Expr

-- | With some Generics-based magic, this could be derived.
class EvalTable t where
  evalTable :: t Expr -> t Rel8.Result

evalExpr :: Expr a -> a
evalExpr = go
  where
    go :: Expr a -> a
    go = \case
      Lit a -> a
      Not b -> not $ go b
      True' -> Prelude.True
      False' -> Prelude.False
      (:==.) a b -> go a == go b

data RecordSet = forall t. Typeable t => RecordSet [t Expr]

evalQuery :: Map Text RecordSet -> Query a -> [a]
evalQuery tables = go
  where
    go :: Query a -> [a]
    go = \case
      Pure a -> pure a
      Bind m f -> go m >>= go . f
      Where bool -> guard (evalExpr bool)
      Limit n q -> take (fromIntegral n) $ go q
      Each Rel8.TableSchema {name} ->
        case M.lookup (T.pack name) tables of
          Nothing -> error "Table lookup failed."
          Just (RecordSet rows0) ->
            case cast rows0 of
              Just rows -> rows
              Nothing -> error "Cast failed."

--------------------------------------------------------------------------------
-- Demonstration schema

-- | Chat data
data Chat f = Chat
  { id :: Rel8.Column f ChatId,
    message :: Rel8.Column f Text
  }
  deriving stock (Generic)
  deriving anyclass (Rel8.Rel8able)

deriving stock instance (f ~ Rel8.Result) => Show (Chat f)

deriving stock instance (f ~ Rel8.Result) => Eq (Chat f)

instance EvalTable Chat where
  evalTable Chat{id,message}=Chat{id=evalExpr id,message=evalExpr message}

instance Lift Rel8.Expr Chat where
  lift Chat{id,message}=Chat{id=SomeExpr id,message=SomeExpr message}
  unlift Chat{id,message}=Chat{id=unsome id,message=unsome message}

instance Lift Expr Chat where
  lift Chat{id,message}=Chat{id=SomeExpr id,message=SomeExpr message}
  unlift Chat{id,message}=Chat{id=unsome id,message=unsome message}

-- | Schema for 'Chat'
chatSchema :: Rel8.TableSchema (Chat Rel8.Name)
chatSchema =
  Rel8.TableSchema
    { name = "chat",
      schema = Nothing,
      columns =
        Chat
          { id = "id",
            message = "message"
          }
    }

-- | Id for 'Chat'
newtype ChatId = ChatId {getChatId :: Int64}
  deriving stock (Generic, Eq, Show)
  deriving newtype
    ( Ord,
      Rel8.DBType,
      Rel8.DBEq,
      Rel8.DBOrd
    )

--------------------------------------------------------------------------------
-- Demonstration queries

-- A generic query.  At the end we use @unlift@ to make it available
-- as the expr we wanted underneath.  The constraints like `'Lift expr
-- Chat` and `LitSemantics expr ChatId` can be collapsed via Generic
-- wizardry.)
myQuery :: forall expr query. (Lift expr Chat, QuerySemantics query expr, LitSemantics expr ChatId) => query (Chat expr)
myQuery = do
  chat1 <- each chatSchema
  chat2 <- each chatSchema
  where_ $ chat1.id ==. lit (ChatId 2)
  where_ $ not_ $ chat2.id ==. lit (ChatId 2)
  pure $ unlift $ chat2

-- Can be interpreted as either Rel8 (SQL), ..
myRel8Query :: Rel8.Query (Chat Rel8.Expr)
myRel8Query = myQuery

-- .. or can be interpreted as a Haskell ADT.
myHaskellQuery :: Query (Chat Expr)
myHaskellQuery = myQuery

-- .. or as a SQL transaction.
myRel8Run :: BrossaHasql.Transaction [Chat Rel8.Result]
myRel8Run = BrossaRel8.select myRel8Query

-- And can be executed in-Haskell.
myHaskellRun :: [Chat Rel8.Result]
myHaskellRun =
  fmap evalTable $ evalQuery myDataSet myHaskellQuery
  where
    myDataSet =
      M.fromList
        [ ( "chat",
            RecordSet
              @Chat
              [ Chat {id = Lit (ChatId 1), message = Lit "Yipee!"},
                Chat {id = Lit (ChatId 2), message = Lit "Woohoo!"},
                Chat {id = Lit (ChatId 3), message = Lit "Nope!"}
              ]
          )
        ]