typesafe database layer?

gistfile1.hs

{-# LANGUAGE ConstraintKinds            #-}
{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE Rank2Types                 #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE StandaloneDeriving         #-}
module DB3 where
import           Control.Monad.Free
import           Data.List
import           Data.Proxy
import           Data.Type.Equality
import           Data.Constraint
import           Data.Functor.Identity
import           Data.Functor.Classes
import           GHC.Exts      (Constraint)
import           GHC.TypeLits
import           Hasql

type family TypeName a :: Symbol
type instance TypeName Int    = "int4"
type instance TypeName String = "text"

-- | A (type-level representation of) a column
data Column a = Column Symbol a

-- | A schema. Although it isn't possible in SQL, a schema here also
-- includes joins. This is used at the type level.
data Schema a 
  = R  [Column a]            -- ^ A row definition, e.g. CREATE TABLE foo(...)
  | RC (Schema a) (Schema a) -- ^ A cartesian-product join, e.g. a JOIN b

-- | A column attribute/modifier
data KAttr s 
  = KPrimary      -- ^ PRIMARY KEY
  | KUnique       -- ^ UNIQUE
  | KRef s Symbol -- ^ REFERENCES s(symbol)

data Attr :: [KAttr *] -> * where
  Primary :: Attr '[ 'KPrimary ]
  Unique  :: Attr '[ 'KUnique ]
  Ref :: (KnownSymbol (Name a), KnownSymbol sym)
      => Proxy (Name a) 
      -> Proxy sym 
      -> Attr '[ 'KRef a sym ]
  And :: Attr '[a] -> Attr b -> Attr (a ': b)

class Model a where
  type Name  a :: Symbol
  type Def   a :: Schema *                -- ^ The schema of a table (WITHOUT modifiers)
  type Attrs a (s :: Symbol) :: [KAttr *] -- ^ Modifiers of the table
  model :: TableDef a 
  build :: a -> Table (Def a)

name :: Proxy a -> Proxy (Name a)
name _ = Proxy

-- | Result marker
data Hole a = Hole

class Any a
instance Any a 

-- | A Table.
data TableT :: (* -> *) -> Schema * -> * where
  Col :: m x -> TableT m ('R xs) 
      -> TableT m ('R ('Column sym x ': xs))
  Join :: TableT m a
       -> TableT m b
       -> TableT m ('RC a b)
  Empty :: TableT m ('R '[]) 

data TableDef a where
  TableDef 
    :: { tableName :: String 
       , table     :: TableT (ColProxy a) (Def a) 
       }
    -> TableDef a 

data ColProxy :: * -> * -> * where 
  ColProxy :: (KnownSymbol sym, KnownSymbol (TypeName a))
           => Proxy sym
           -> Proxy (TypeName a)
           -> Attr (Attrs s sym)
           -> ColProxy s a

type Table = TableT Identity

----------------------------------------
-- Ugly syntax :)

{-# INLINE (><) #-}
(><) :: TableT m a -> TableT m b -> TableT m ('RC a b)
(><) = Join

{-# INLINE (!+) #-}
(!+) :: Applicative m => x -> TableT m ('R xs) -> TableT m ('R ('Column sym x ': xs))
(!+) a p = pure a `Col` p

{-# INLINE (!*) #-}
(!*) :: Applicative m => x -> y -> TableT m ('R '[ 'Column nameX x,
                                                   'Column nameY y ])
(!*) a b = pure a `Col` pure b `Col` Empty

infixr 9 `Col`
infixr 4 !+
infixr 4 !*

--------------------------------------------------------------------------------
-- Taking tables and producing idiomatic Haskell things   
   
type family ExpandT (m :: * -> *) (table :: Schema *) (into :: *) where
  ExpandT m ('R ('Column sym a ': xs)) r = m a -> ExpandT m ('R xs) r
  ExpandT m ('R '[])                   r = r
  ExpandT m ('RC a b)                  r = ExpandT m a (ExpandT m b r)
   
type family Expand (table :: Schema *) (into :: *) where
  Expand ('R ('Column sym a ': xs)) r = a -> Expand ('R xs) r
  Expand ('R '[])                   r = r
  Expand ('RC a b)                  r = Expand a (Expand b r)

newtype FuncT m a r where FuncT :: { resultT :: ExpandT m a r } -> FuncT m a r
newtype Func    a r where Func  :: { result  :: Expand a r    } -> Func a r

destruct :: TableT m a -> FuncT m a r -> r
destruct (Col x xs) (FuncT f) = destruct xs (FuncT (f x))
destruct Empty      (FuncT x) = x

{-# INLINE destructM #-}
destructM :: Monad m => (r -> m r') -> TableT m a -> Func a r -> m r'
destructM ret (Col x xs) (Func f) = destructM ret xs . Func =<< fmap f x
destructM ret (Join a b) (Func f) = 
  destructM (\g -> destructM ret b (Func g)) a (Func f)
destructM ret Empty      (Func x) = ret x

{-# INLINE constr #-}
constr :: Expand a r -> Table a -> r
constr f a = runIdentity (destructM Identity a (Func f)) 

{-# INLINE constrM #-}
constrM :: Monad m => Expand a r -> TableT m a -> m r
constrM f a = destructM pure a (Func f)

--------------------------------------------------------------------------------
-- Example

data Tag = Tag Int String deriving (Show)
instance Model Tag where
  type Name  Tag = "tag"
  type Def   Tag = 'R '[ 'Column "id" Int, 'Column "name" String ]
  type Attrs Tag "id"   = '[ 'KPrimary ]
  type Attrs Tag "name" = '[ 'KUnique ]
  model = TableDef 
    { tableName = "tag"
    , table     = ColProxy (Proxy :: Proxy "id")   Proxy Primary `Col` 
                  ColProxy (Proxy :: Proxy "name") Proxy Unique  `Col` Empty
    }
  build (Tag a b) = a !* b

showAttrs :: Attr a -> String
showAttrs Primary = " PRIMARY KEY "
showAttrs Unique  = " UNIQUE "
showAttrs (Ref s a) = "REFERENCES " ++ symbolVal s ++ "(" ++ symbolVal a ++ ")"

showCol :: ColProxy a b -> String
showCol (ColProxy name ty attrs) = 
  symbolVal name ++ " " ++ symbolVal ty ++ showAttrs attrs

showCols :: TableT (ColProxy s) a -> [String]
showCols (Col x xs) = showCol x : showCols xs
showCols Empty      = []

showModel :: TableDef a -> String
showModel (TableDef n cols) = "CREATE TABLE " ++ n ++ "(" ++ 
                              intercalate ", " (showCols cols) ++ ")"

{-# INLINE test #-}
test :: Table (Def Tag)
test  = 0   !* "asdf"
test2 = 'a' !* "fdsa" 
test3 = ()  !+ [2+2] !* (1 + 1 :: Int)
asdf = test >< test2 >< test3

>>> constr _ asdf

<interactive>:11:8:
    Found hole ‘_’
      with type: Int
                 -> [Char] -> Char -> [Char] -> () -> [Integer] -> Int -> r
    Where: ‘r’ is a rigid type variable bound by
               the inferred type of it :: r at <interactive>:11:1
    Relevant bindings include it :: r (bound at <interactive>:11:1)
    In the first argument of ‘constr’, namely ‘_’
    In the expression: constr _ asdf
    In an equation for ‘it’: it = constr _ asdf
>>> constr (,,,,,,) asdf
(0,"asdf",'a',"fdsa",(),[4],2)
>>> constr Tag test
Tag 0 "asdf"