Knowledge Values.
A value is a concrete representation of knowledge. It is a snapshot of all properties associated with some object, i.e., an ordered tuple of slots. The value has no identity and that differs it from the object, as the value is essentially a property of an object - not an object itself.
From another perspective, a value is an extensible record, with fields reified into first-class slots, the record type into the cls
values, and an additional constraint that all field types must be an instance of the domain type class (i.e., have a default and an ordering).
Each value has a class. The class value itself is indexed with the class and sort indices. The first index denotes the set of properties that could be associated with the value. The second index further partitions values of that class into subsets, to so that domain specific relations between values could be expressed explicitly with the host language type system.
The value sort is an arbitrary value, which can also be used to store additional static information about the value, i.e., the information that is common to all instances of the sort.
Total ordering and age
In addition to be partially ordered by their information content, values are also totally ordered, so that they could be organized into finite sets and maps.
The total order is induced from the information order, so that if a value x
is ordered before y
in the information order, then it will be also ordered before y
in the total order. And if x
and y
have the same information content, then they are considered equal. Values with non-comparable information content are ordered by their time-stamp.
Every time a new value created it is assigned a time-stamp. A new value is created by all functions that has 'a value
return type, except the refine
function. Each time-stamp is unique and no two values could have the same time-stamps unless they are physically the same, or are de-serializations of the same value, or are refinements of the same value. In other words, values with equal time-stamps are guaranteed to bear the same information.
Time-stamp values correlate with the order of evaluation. A value that was evaluated more recently will have a higher time-stamp. Therefore time-stamps define an age of a value. A value which has a smaller time-stamp is younger than a value that has a larger time-stamp.
a witness of the ordering
empty cls
the empty value of class cls
.
The empty value has the least information content, i.e., all slots are empty.
val is_empty : _ value -> bool
is_empty x
iff all properties of x
are empty.
order x y
orders x
and y
by their information content.
join x y
joins pairwise all slots of x
and y
.
Each slot of x
and y
are joined using the Domain.join
function. The result is either a pairwise join or a conflict if any of the joins ended up with a conflict.
val merge :
?on_conflict:[ `drop_old | `drop_new | `drop_right | `drop_left ] ->
'a value ->
'a value ->
'a value
merge x y
joins x
and y
and resolves conflicts.
Performs a pairwise join of x
and y
and in case if any of the joins yields a conflict uses the provided strategy to resolve it.
get p v
gets a value of the property p
.
put p v x
sets a value of the property p
.
has p x
if property p
of x
is not empty.
refine v s
refines the sort of v
to s
.
Since, this function doesn't change the information stored in the value, the time-stamp of the returned value is the same, therefore v = refine v s
.
module type S = sig ... end
derive cls
derives the implementation of the S
structure.
pp ppf v
outputs v
to the formatter ppf
.
Prints all slots of the value v
.
pp_slots slots ppf v
prints the specified set of slots.
Prints only slots that has a name in slots
.