Language.Souffle.Experimental

This module provides an experimental DSL for generating Souffle Datalog code, directly from Haskell.

The module is meant to be imported unqualified, unlike the rest of this library. This allows for a syntax that is very close to the corresponding Datalog syntax you would normally write.

The functions and operators provided by this module follow a naming scheme:

• If there is no clash with something imported via Prelude, the function or operator is named exactly the same as in Souffle.
• If there is a clash for functions, an apostrophe is appended (e.g. "max" in Datalog is max' in Haskell).
• Most operators (besides those from the Num typeclass) start with a "." (e.g. .^ is the "^" operator in Datalog)

The DSL makes heavy use of Haskell's typesystem to avoid many kinds of errors. This being said, not everything can be checked at compile-time (for example performing comparisons on ungrounded variables can't be checked). For this reason you should regularly write the Datalog code to a file while prototyping your algorithm and check it using the Souffle executable for errors.

A large subset of the Souffle language is covered, with some exceptions such as "$", aggregates, ... There are no special functions for supporting components either, but this is automatically possible by making use of polymorphism in Haskell.

Here's an example snippet of Haskell code that can generate Datalog code:

   -- Assuming we have 2 types of facts named Edge and Reachable:
   data Edge = Edge String String
   data Reachable = Reachable String String

   program = do
     Predicate edge <- predicateFor @Edge
     Predicate reachable <- predicateFor @Reachable
     a <- var "a"
     b <- var "b"
     c <- var "c"
     reachable(a, b) |- edge(a, b)
     reachable(a, b) |- do
       edge(a, c)
       reachable(c, b)
   

When rendered to a file (using renderIO), this generates the following Souffle code:

   .decl edge(t1: symbol, t2: symbol)
   .input edge
   .decl reachable(t1: symbol, t2: symbol)
   .output reachable
   reachable(a, b) :-
     edge(a, b)
   reachable(a, b) :- do
     edge(a, c)
     reachable(c, b)
   

For more examples, take a look at the tests.

DSL-related types and functions

Types

newtype Predicate a

A datatype that contains a function for generating Datalog AST fragments that can be glued together using other functions in this module.

The rank-N type allows using the inner function in multiple places to generate different parts of the AST. This is one of the key things that allows writing Haskell code in a very smilar way to the Datalog code.

The inner function uses the Structure of a type to compute what the shape of the input tuple for the predicate should be. For example, if a fact has a data constructor containing a Float and a String, the resulting tuple will be of type (Term ctx Float, Term ctx String).

Currently, only facts with up to 10 fields are supported. If you need more fields, please file an issue on Github.

Constructors

Predicate (forall f ctx. Fragment f ctx => Tuple ctx (Structure a) -> f ctx ())

class Fragment f ctx

A typeclass used for generating AST fragments of Datalog code. The generated fragments can be further glued together using the various functions in this module.

Minimal complete definition

toFragment

Instances

Fragment (Body :: UsageContext -> Type -> Type) 'Relation

Defined in Language.Souffle.Experimental

Methods

toFragment :: forall k (ts :: [Type]) (a :: k). ToTerms ts => TypeInfo a ts -> Name -> Tuple 'Relation ts -> Body 'Relation ()

Fragment (Head :: UsageContext -> Type -> Type) 'Relation

Defined in Language.Souffle.Experimental

Methods

toFragment :: forall k (ts :: [Type]) (a :: k). ToTerms ts => TypeInfo a ts -> Name -> Tuple 'Relation ts -> Head 'Relation ()

Fragment (DSL prog :: UsageContext -> Type -> Type) 'Definition

Defined in Language.Souffle.Experimental

Methods

toFragment :: forall k (ts :: [Type]) (a :: k). ToTerms ts => TypeInfo a ts -> Name -> Tuple 'Definition ts -> DSL prog 'Definition ()

type Tuple ctx ts = TupleOf (MapType (Term ctx) ts)

A type synonym for a tuple consisting of Datalog Terms. Only tuples containing up to 10 elements are currently supported.

data DSL prog ctx a

The main monad in which Datalog AST fragments are combined together using other functions in this module.

• The "prog" type variable is used for performing many compile time checks. This variable is filled (automatically) with a type that implements the Program typeclass.
• The "ctx" type variable is the context in which a DSL fragment is used. For more information, see UsageContext.
• The "a" type variable is the value contained inside (just like other monads).

Instances

Fragment (DSL prog :: UsageContext -> Type -> Type) 'Definition

Defined in Language.Souffle.Experimental

Methods

toFragment :: forall k (ts :: [Type]) (a :: k). ToTerms ts => TypeInfo a ts -> Name -> Tuple 'Definition ts -> DSL prog 'Definition ()

Monad (DSL prog ctx)

Defined in Language.Souffle.Experimental

Methods

(>>=) :: DSL prog ctx a -> (a -> DSL prog ctx b) -> DSL prog ctx b

(>>) :: DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx b

return :: a -> DSL prog ctx a

Functor (DSL prog ctx)

Defined in Language.Souffle.Experimental

Methods

fmap :: (a -> b) -> DSL prog ctx a -> DSL prog ctx b

(<$) :: a -> DSL prog ctx b -> DSL prog ctx a

Applicative (DSL prog ctx)

Defined in Language.Souffle.Experimental

Methods

pure :: a -> DSL prog ctx a

(<*>) :: DSL prog ctx (a -> b) -> DSL prog ctx a -> DSL prog ctx b

liftA2 :: (a -> b -> c) -> DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx c

(*>) :: DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx b

(<*) :: DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx a

data Head ctx unused

Data type representing the head of a relation (the part before ":-" in a Datalog relation).

• The "ctx" type variable is the context in which this type is used. For this type, this will always be Relation. The variable is there to perform some compile-time checks.
• The "unused" type variable is unused and only there so the type has the same kind as Body and DSL.

See also |-.

Instances

Fragment (Head :: UsageContext -> Type -> Type) 'Relation

Defined in Language.Souffle.Experimental

Methods

toFragment :: forall k (ts :: [Type]) (a :: k). ToTerms ts => TypeInfo a ts -> Name -> Tuple 'Relation ts -> Head 'Relation ()

data Body ctx a

Data type representing the body of a relation (what follows after ":-" in a Datalog relation).

By being a monad, it supports do-notation which allows for a syntax that is quite close to Datalog.

• The "ctx" type variable is the context in which this type is used. For this type, this will always be Relation. The variable is there to perform some compile-time checks.
• The "a" type variable is the value contained inside (just like other monads).

See also |-.

Instances

Fragment (Body :: UsageContext -> Type -> Type) 'Relation

Defined in Language.Souffle.Experimental

Methods

toFragment :: forall k (ts :: [Type]) (a :: k). ToTerms ts => TypeInfo a ts -> Name -> Tuple 'Relation ts -> Body 'Relation ()

Monad (Body ctx)

Defined in Language.Souffle.Experimental

Methods

(>>=) :: Body ctx a -> (a -> Body ctx b) -> Body ctx b

(>>) :: Body ctx a -> Body ctx b -> Body ctx b

return :: a -> Body ctx a

Functor (Body ctx)

Defined in Language.Souffle.Experimental

Methods

fmap :: (a -> b) -> Body ctx a -> Body ctx b

(<$) :: a -> Body ctx b -> Body ctx a

Applicative (Body ctx)

Defined in Language.Souffle.Experimental

Methods

pure :: a -> Body ctx a

(<*>) :: Body ctx (a -> b) -> Body ctx a -> Body ctx b

liftA2 :: (a -> b -> c) -> Body ctx a -> Body ctx b -> Body ctx c

(*>) :: Body ctx a -> Body ctx b -> Body ctx b

(<*) :: Body ctx a -> Body ctx b -> Body ctx a

data Term ctx ty

Data type for representing Datalog terms.

All constructors are hidden, but with the Num, Fractional and IsString instances it is possible to create terms using Haskell syntax for literals. For non-literal values, smart constructors are provided. (See for example underscore / __.)

Instances

Fractional (Term ctx Float)

Defined in Language.Souffle.Experimental

Methods

(/) :: Term ctx Float -> Term ctx Float -> Term ctx Float

recip :: Term ctx Float -> Term ctx Float

fromRational :: Rational -> Term ctx Float

(SupportsArithmetic ty, Num ty) => Num (Term ctx ty)

Defined in Language.Souffle.Experimental

Methods

(+) :: Term ctx ty -> Term ctx ty -> Term ctx ty

(-) :: Term ctx ty -> Term ctx ty -> Term ctx ty

(*) :: Term ctx ty -> Term ctx ty -> Term ctx ty

negate :: Term ctx ty -> Term ctx ty

abs :: Term ctx ty -> Term ctx ty

signum :: Term ctx ty -> Term ctx ty

fromInteger :: Integer -> Term ctx ty

IsString (Term ctx Text)

Defined in Language.Souffle.Experimental

Methods

fromString :: String -> Term ctx Text

IsString (Term ctx Text)

Defined in Language.Souffle.Experimental

Methods

fromString :: String -> Term ctx Text

IsString (Term ctx String)

Defined in Language.Souffle.Experimental

Methods

fromString :: String -> Term ctx String

type VarName = Text

Type representing a variable name in Datalog.

data UsageContext

A type level tag describing in which context a DSL fragment is used. This is only used on the type level and helps catch some semantic errors at compile time.

Constructors

Definition

A DSL fragment is used in a top level definition.

Relation

A DSL fragment is used inside a relation (either head or body of a relation).

Instances

Fragment (Body :: UsageContext -> Type -> Type) 'Relation

Defined in Language.Souffle.Experimental

Methods

toFragment :: forall k (ts :: [Type]) (a :: k). ToTerms ts => TypeInfo a ts -> Name -> Tuple 'Relation ts -> Body 'Relation ()

Fragment (Head :: UsageContext -> Type -> Type) 'Relation

Defined in Language.Souffle.Experimental

Methods

toFragment :: forall k (ts :: [Type]) (a :: k). ToTerms ts => TypeInfo a ts -> Name -> Tuple 'Relation ts -> Head 'Relation ()

Fragment (DSL prog :: UsageContext -> Type -> Type) 'Definition

Defined in Language.Souffle.Experimental

Methods

toFragment :: forall k (ts :: [Type]) (a :: k). ToTerms ts => TypeInfo a ts -> Name -> Tuple 'Definition ts -> DSL prog 'Definition ()

data Direction

A datatype describing which operations a certain fact supports. The direction is from the datalog perspective, so that it aligns with ".decl" statements in Souffle.

Constructors

Input

Fact can only be stored in Datalog (using addFact/addFacts).

Output

Fact can only be read from Datalog (using getFacts/findFact).

InputOutput

Fact supports both reading from / writing to Datalog.

Internal

Supports neither reading from / writing to Datalog. This is used for facts that are only visible inside Datalog itself.

type ToPredicate prog a = (Fact a, FactMetadata a, ContainsFact prog a, SimpleProduct a, Assert (Length (Structure a) <=? 10) BigTupleError, KnownDLTypes (Structure a), KnownDirection (FactDirection a), KnownSymbols (AccessorNames a), ToTerms (Structure a))

Constraint that makes sure a type can be converted to a predicate function. It gives a user-friendly error in case any of the sub-constraints are not met.

class (Fact a, SimpleProduct a) => FactMetadata a where

A typeclass for optionally configuring extra settings (for performance reasons).

Minimal complete definition

Nothing

Methods

factOpts :: Proxy a -> Metadata a

An optional function for configuring fact metadata.

By default no extra options are configured. For more information, see the Metadata type.

data Metadata a

A data type that allows for finetuning of fact settings (for performance reasons).

Constructors

Metadata (StructureOpt a) (InlineOpt (FactDirection a))

data StructureOpt (a :: Type) where

Datatype describing the way a fact is stored inside Datalog. A different choice of storage type can lead to an improvement in performance (potentially).

For more information, see this link and this link.

Constructors

Automatic :: StructureOpt a

Automatically choose the underlying storage for a relation. This is the storage type that is used by default.

For Souffle, it will choose a direct btree for facts with arity <= 6. For larger facts, it will use an indirect btree.

BTree :: StructureOpt a

Uses a direct btree structure.

Brie :: StructureOpt a

Uses a brie structure. This can improve performance in some cases and is more memory efficient for particularly large relations.

EqRel :: (IsBinaryRelation a, Structure a ~ '[t, t]) => StructureOpt a

A high performance datastructure optimised specifically for equivalence relations. This is only valid for binary facts with 2 fields of the same type.

data InlineOpt (d :: Direction) where

Datatype indicating if we should inline a fact or not.

Constructors

Inline :: InlineOpt 'Internal

Inlines the fact, only possible for internal facts.

NoInline :: InlineOpt d

Does not inline the fact.

Basic building blocks

predicateFor :: forall a prog. ToPredicate prog a => DSL prog 'Definition (Predicate a)

Generates a function for a type that implements Fact and is a SimpleProduct. The predicate function takes the same amount of arguments as the original fact type. Calling the function with a tuple of arguments, creates fragments of datalog code that can be glued together using other functions in this module.

Note: You need to specify for which fact you want to return a predicate for using TypeApplications.

var :: NoVarsInAtom ctx => VarName -> DSL prog ctx' (Term ctx ty)

Generates a unique variable, using the name argument as a hint.

The type of the variable is determined the first predicate it is used in. The NoVarsInAtom constraint generates a user-friendly type error if the generated variable is used inside a relation (which is not valid in Datalog).

Note: If a variable is created but not used using this function, you will get a compile-time error because it can't deduce the constraint.

__ :: Term ctx ty

Term representing a wildcard ("_") in Datalog. Note that in the DSL this is with 2 underscores. (Single underscore is reserved for typed holes!)

underscore :: Term ctx ty

Term representing a wildcard ("_") in Datalog.

(|-) :: Head 'Relation a -> Body 'Relation () -> DSL prog 'Definition () infixl 0

Turnstile operator from Datalog, used in relations.

This is used for creating a DSL fragment that contains a relation. NOTE: |- is used instead of :- due to limitations of the Haskell syntax.

(\/) :: Body ctx () -> Body ctx () -> Body ctx ()

Creates a fragment that is the logical disjunction (OR) of 2 sub-fragments. This corresponds with ";" in Datalog.

not' :: Body ctx a -> Body ctx ()

Creates a fragment that is the logical negation of a sub-fragment. This is equivalent to "!" in Datalog. (But this operator can't be used in Haskell since it only allows unary negation as a prefix operator.)

Souffle operators

(.<) :: Num ty => Term ctx ty -> Term ctx ty -> Body ctx () infix 1

Creates a less than constraint (a < b), for use in the body of a relation.

(.<=) :: Num ty => Term ctx ty -> Term ctx ty -> Body ctx () infix 1

Creates a less than or equal constraint (a <= b), for use in the body of a relation.

(.>) :: Num ty => Term ctx ty -> Term ctx ty -> Body ctx () infix 1

Creates a greater than constraint (a > b), for use in the body of a relation.

(.>=) :: Num ty => Term ctx ty -> Term ctx ty -> Body ctx () infix 1

Creates a greater than or equal constraint (a >= b), for use in the body of a relation.

(.=) :: Term ctx ty -> Term ctx ty -> Body ctx () infix 1

Creates a constraint that 2 terms should be equal to each other (a = b), for use in the body of a relation.

(.!=) :: Term ctx ty -> Term ctx ty -> Body ctx () infix 1

Creates a constraint that 2 terms should not be equal to each other (a != b), for use in the body of a relation.

(.^) :: Num ty => Term ctx ty -> Term ctx ty -> Term ctx ty

Exponentiation operator ("^" in Datalog).

(.%) :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty

Remainder operator ("%" in Datalog).

band :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty

Binary AND operator.

bor :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty

Binary OR operator.

bxor :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty

Binary XOR operator.

lor :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty

Logical OR operator.

land :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty

Logical AND operator.

Souffle functions

max' :: Num ty => Term ctx ty -> Term ctx ty -> Term ctx ty

"max" function.

min' :: Num ty => Term ctx ty -> Term ctx ty -> Term ctx ty

"min" function.

cat :: ToString ty => Term ctx ty -> Term ctx ty -> Term ctx ty

"cat" function (string concatenation).

contains :: ToString ty => Term ctx ty -> Term ctx ty -> Body ctx ()

"contains" predicate, checks if 2nd string contains the first.

match :: ToString ty => Term ctx ty -> Term ctx ty -> Body ctx ()

"match" predicate, checks if a wildcard string matches a given string.

ord :: ToString ty => Term ctx ty -> Term ctx Int32

"ord" function.

strlen :: ToString ty => Term ctx ty -> Term ctx Int32

"strlen" function.

substr :: ToString ty => Term ctx ty -> Term ctx Int32 -> Term ctx Int32 -> Term ctx ty

"substr" function.

to_number :: ToString ty => Term ctx ty -> Term ctx Int32

"to_number" function.

to_string :: ToString ty => Term ctx Int32 -> Term ctx ty

"to_string" function.

Functions for running a Datalog DSL fragment / AST directly.

runSouffleInterpretedWith :: (MonadIO m, Program prog) => Config -> prog -> DSL prog 'Definition () -> (Maybe (Handle prog) -> SouffleM a) -> m a

This function runs the DSL fragment directly using the souffle interpreter executable.

It does this by saving the fragment to a file in the directory specified by the cfgDatalogDir field in the interpreter settings. Depending on the chosen settings, the fact and output files may not be automatically cleaned up after running the souffle interpreter. See runSouffleWith for more information on automatic cleanup.

runSouffleInterpreted :: (MonadIO m, Program prog) => prog -> DSL prog 'Definition () -> (Maybe (Handle prog) -> SouffleM a) -> m a

This function runs the DSL fragment directly using the souffle interpreter executable.

It does this by saving the fragment to a temporary file right before running the souffle interpreter. All created files are automatically cleaned up after the souffle related actions have been executed. If this is not your intended behavior, see runSouffleInterpretedWith which allows passing in different interpreter settings.

embedProgram :: Program prog => prog -> DSL prog 'Definition () -> Q [Dec]

Embeds a Datalog program from a DSL fragment directly in a Haskell file.

Note that due to TemplateHaskell staging restrictions, this function must be used in a different module than the module where Program and Fact instances are defined.

In order to use this function correctly, you have to add the following line to the top of the module where embedProgram is used in order for the embedded C++ code to be compiled correctly:

{-# OPTIONS_GHC -optc-std=c++17 -D__EMBEDDED_SOUFFLE__ #-}

Rendering functions

render :: Program prog => prog -> DSL prog 'Definition () -> Text

Renders a DSL fragment to the corresponding Datalog code.

renderIO :: Program prog => prog -> FilePath -> DSL prog 'Definition () -> IO ()

Renders a DSL fragment to the corresponding Datalog code and writes it to a file.

Helper type families useful in some situations

type family Structure a :: [Type] where ...

A helper type family for computing the list of types used in a data type. (The type family assumes a data type with a single data constructor.)

Equations

Structure a = Collect (Rep a)

type family NoVarsInAtom (ctx :: UsageContext) :: Constraint where ...

A type family used for generating a user-friendly type error in case you use a variable in a DSL fragment where it is not allowed (outside of relations).

Equations

NoVarsInAtom ctx = Assert (ctx == 'Relation) NoVarsInAtomError

class Num ty => SupportsArithmetic ty

A helper typeclass, mainly used for avoiding a lot of boilerplate in the Num instance for Term.

Minimal complete definition

fromInteger'

Instances

SupportsArithmetic Float

Defined in Language.Souffle.Experimental

Methods

fromInteger' :: forall (ctx :: UsageContext). Integer -> Term ctx Float

SupportsArithmetic Int32

Defined in Language.Souffle.Experimental

Methods

fromInteger' :: forall (ctx :: UsageContext). Integer -> Term ctx Int32

SupportsArithmetic Word32

Defined in Language.Souffle.Experimental

Methods

fromInteger' :: forall (ctx :: UsageContext). Integer -> Term ctx Word32