Typed Datalog API

TypedDatalog.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall #-}

import           Control.Monad.ST ( RealWorld )
import           Control.Monad ( guard )
import           Data.Functor.Const ( Const(..) )
import           Data.Parameterized.Classes
import           Data.Parameterized.Context
import qualified Data.Parameterized.HashTable as PH
import qualified Data.Parameterized.Map as MapF
import qualified Data.Parameterized.Nonce as PN

-- | A relation has a name and is represented by its type (which is an
-- assignment of run-time type representatives)
data Relation r tps where
  Relation :: String
           -> Assignment r tps
           -> Assignment (Const String) tps
           -> Relation r tps

data Term r a tp where
  LogicVar :: r tp -> String -> Term r a tp
  BindVar :: Binder r tp -> Term r a tp
  Anything :: Term r a tp
  Atom :: r tp -> a tp -> Term r a tp

-- | A clause is a sequence of terms (with types congruent with the relation backing the term)
data Clause r a tps where
  Clause :: Relation r tps -> Assignment (Term r a) tps -> Clause r a tps

data Adornment tp where
  Free :: Int -> Adornment tp
  BoundAtom :: Adornment tp
  Bound :: Int -> Adornment tp

data AdornedClause r a tps where
  AdornedClause :: Relation r tps
                -> Assignment (Term r a) tps
                -> Assignment Adornment tps
                -> AdornedClause r a tps

data Literal clause r a tps where
  Literal :: clause r a tps -> Literal clause r a tps
  NegatedLiteral :: clause r a tps -> Literal clause r a tps
  ConditionalClause :: (Assignment a tps -> Bool)
                    -> Assignment (Term r a) tps
                    -> Literal clause r a tps

-- FIXME: The Clause needs to become an AdornedClause once we have enough
-- information from the Body to determine variable bindings
--
-- Note: Adornments are only computed during the magic sets transformation,
-- which maybe isn't needed initially
--
-- Question: What do the magic sets clauses look like? Can we generate them in a
-- type-safe way?  That could get very complicated.  Or it might be very easy.
data Rule r a where
  Rule :: Relation r tps
       -> Assignment (Binder r) tps
       -> Assignment (Literal Clause r a) ctx
       -> Rule r a

data TupleStore r a tps =
  TupleStore { tsRelation :: Relation r tps
             , tsData :: [Assignment a tps]
             -- ^ Original (base) data
             , tsTuples :: PH.HashTable RealWorld (Assignment a) (Const ())
             -- ^ Tuples generated during evaluation; they are in a hash table
             -- for easy uniqueness
             , tsDelta  :: [Assignment a tps]
             }

data Database r a = Database (MapF.MapF (Relation r) (TupleStore r a))

{- Tuple Creation

- Tuples for relation `Relation r tps` will be of type `Assignment a tps`
- We will create each new tuple via Assignment.generate
- Create a skeleton of value extractors for each Rule (extractors will be
  in terms of Index, to make things total)
- Join becomes creation of an Assignment mirroring the structure of the
  list of literals in the target rule (generate then becomes an easy thing)

-}

data Binder r tp where
  Binder :: r tp -> String -> Binder r tp

instance (TestEquality r) => TestEquality (Binder r) where
  testEquality (Binder r1 s1) (Binder r2 s2) = do
    guard (s1 == s2)
    Refl <- testEquality r1 r2
    return Refl

-- | Assert a rule
--
-- The LHS is a relation with binding variables
--
-- The RHS is the body, which is a conjunction of body literals that bind
-- the same number (and types) of variables as the LHS
(|-) :: (Relation r tps, Assignment (Binder r) tps)
     -> Assignment (Literal Clause r a) ctx
     -> Rule r a
(rel, binders) |- body = Rule rel binders body
infixr 0 |-

lit :: Relation r tps -> Assignment (Term r a) tps -> Literal Clause r a tps
lit r ts = Literal (Clause r ts)

negLit :: Relation r tps -> Assignment (Term r a) tps -> Literal Clause r a tps
negLit r ts = NegatedLiteral (Clause r ts)

-- | Conditions can have both literals and variables (e.g., X < 5 is a reasonable condition)
cond :: String
     -> (Assignment a tps -> Bool)
     -> Assignment (Term r a) tps
     -> Literal Clause r a tps
cond _ p ts = ConditionalClause p ts

-- To query, provide a relation and a "list" of binding variables and atoms
--
-- query :: Relation r tps -> ??? -> Assignment a tps

----------------------------------------------------
-- Testing to see if these types are actually usable

data TestTypes = TInt
               | TString
               | TCity

data TestAtom (tp :: TestTypes) where
  AInt :: Int -> TestAtom 'TInt
  AString :: String -> TestAtom 'TString
  ACity :: String -> TestAtom 'TCity

data TestRepr (tp :: TestTypes) where
  IntRepr :: TestRepr 'TInt
  StringRepr :: TestRepr 'TString
  CityRepr :: TestRepr 'TCity

instance TestEquality TestRepr where
  testEquality IntRepr IntRepr = Just Refl
  testEquality StringRepr StringRepr = Just Refl
  testEquality CityRepr CityRepr = Just Refl
  testEquality _ _ = Nothing

test :: IO ()
test = do
  let cityR = Relation "City" (Empty :> CityRepr :> IntRepr :> IntRepr)
                              (Empty :> Const "City" :> Const "TimeZone" :> Const "Population")
  let adjacentR = Relation "Adjacent" (Empty :> CityRepr :> CityRepr :> IntRepr)
                                      (Empty :> Const "Source" :> Const "Source" :> Const "Distance")

  -- Every pair of cities that is adjacent and in the same timezone
  let sameTZAdjacentR = Relation "SameTZAdjacent" (Empty :> CityRepr :> CityRepr)
                                                  (Empty :> Const "City1" :> Const "City2")

  -- A city binder, to be referenced on the LHS
  let city1B = Binder CityRepr "city1"
  let city2B = Binder CityRepr "city2"
  let tz = LogicVar IntRepr "TZ"

  let r = (sameTZAdjacentR, Empty :> city1B :> city2B) |-
            empty
            :> lit adjacentR (empty :> BindVar city1B :> BindVar city2B :> Anything)
            :> lit cityR (empty :> BindVar city1B :> tz :> Anything)
            :> lit cityR (empty :> BindVar city2B :> tz :> Anything)


  _ <- undefined r
  return ()