Value Types

Each value type is a new type. See the reference section about declaring value types for details and the concept guide Value Types for an extensive introduction.

This section discusses one particular example of a value type, declared with the following:

value type V = Int, String

By declaring the value type V you implicitly declare two relations:

• A constructor relation ^V(i, s, v) that creates the value type v from the arguments i and s.
• A type relation V(v) that checks if the argument v has the value type V.

Note that data types can be defined from any number of arguments and not just from two as shown above.

Construction

The constructor relation ^V is an infinite relation that maps pairs of integers and strings to values of type V:

// read query
 
value type V = Int, String        // Declaration
 
def output = ^V[44, "secret"]     // Construct a value of type `V`.

Membership

To test whether a value belongs to the value type V, just give it as an argument to V:

// read query
 
value type V = Int, String        // Declaration
 
def v = ^V[44, "secret"]          // A value
 
def output = V(v)   // Test for membership.

Note that V is an infinite relation, so V(x) cannot be used to ground variable x.

Noteworthy Operations

You may define your own operations on each of your value types. See Extracting the Representation of a Value (General Case) in the Value Types concept guide for an example. Rel does not provide anything by default, except a test for equality:

// read query
 
value type V = Int, String
value type W = Int, String
 
def v = ^V[0, "zero"]; ^V[1, "one"]
def w = ^V[1, "one"];  ^V[0, "zero"]
 
def output:A { equal(v, w) }
def output:B { ^V[2, "two"]  = ^V[2, "two"] }
def output:C { ^V[2, "two"] != ^V[2, "TWO"] }
def output:D { ^V[2, "two"] != ^W[2, "two"] }

Notice that the value produced by ^V[2, "two"] is not equal to the one produced by ^W[2, "two"]: these values belong to different types.

Next: Entity Types