Predicate Logic used in fact-models

This document:

  • explains the predicate logic used in the fact-models packages

  • provides examples

Informal heuristics

TODO: develop this section

  • Product types (records) are ANDed together: does a condition hold for all component predicates?

  • List are ORed together: does a fact at least one of the values in the list?

  • Optionals are optional in the following sense:

    • If a predicate value is None, then the predicate trivially returns True, regardless of the fact’s value.

    • If a predicate value is Some, but the fact is None, then the predicate returns False.

    • If a predicate value is Some p, and the fact is Some x, then predicate evaluates to p x.

At this time, the predicate logic only operates on values based on equality. There are no negation or less/greater than operators.

Examples

Suppose we have the following fact types:

let Habitat = < Forest | Meadow | Urban >
let SampleRecord =
{ species : Text
, habitat : ../Habitat/Fact.dhall
}

With corresponding we have the following predicate constructor types:

let HabitatPredCons = List Habitat
let SampleRecordPredCons =
{ species = Optional (List Text)
, habitat = Optional HabitatPredCons
}
For record types, the field names in the predicate constructor should match the names in the corresponding fact type.

In this case, we have defined all the fields in the SampleRecordPredCons to be optional, meaning that we can query SampleRecord facts based on any or all of its fields.

Suppose we had the following value of SampleRecord:

let exampleRecord : SampleRecord =
{ species = "Pinus taeda"
, habitat = Habitat.Forest
}

Can you guess what the following predicate constructor values should return, given this fact?

let examplePred : SampleRecordPredCons =
{ species = None (List Text)
, habitat = None (List Habitat)
}
Show result

Should be True, since:

  • all of the predicate constructor fields are None.

let examplePred : SampleRecordPredCons =
{ species = None (List Text)
, habitat = Some [Habitat.Forest, Habitat.Urban]
}
Show result

Should be True, since:

  • predicate constructor for species is None

  • predicate constructor for habitat is Some p

  • where p is the list predicate, and the list contains Forest.

let examplePred : SampleRecordPredCons =
{ species = None (List Text)
, habitat = Some [Habitat.Urban]
}
Show result

Should be False, since:

  • predicate constructor for species is None

  • predicate constructor for habitat is Some p

  • where p is the list predicate, but the list does not contain Forest.

let examplePred : SampleRecordPredCons =
{ species = Some ["Isotrema macrophyla"]
, habitat = None (List Habitat)
}
Show result

Should be False, since:

  • predicate constructor for habitat is None

  • predicate constructor for species is Some p

  • where p is the list predicate, but the list does not contain Pinus taeda.

The result above work because of how we’ve defined the type of the predicate constructor. Here are a few other ways we could have defined that type.

let SampleRecordPredCons =
{ species = List Text
, habitat = Optional HabitatPredCons
}

Thus making it required to provide a List of species to the predicate constructor.

let SampleRecordPredCons =
{ species = List Text
, habitat = HabitatPredCons
}

Thus making it required to provide both a List of species and a List of habitats to the predicate constructor.

let SampleRecordPredCons =
{ species = List Text
}

Thus making it required to provide a list of species, and not allowing for querying based on the habitat field.