46 Built-in Types

Predica defines a fixed set of built-in types. Built-in types are available without user declarations.

Boolean type

The Boolean type has exactly two values: false and true.

Integer types

The Integer type denotes mathematical integers.

Predica also defines fixed-width signed and unsigned integer types:

Int8
Int16
Int32
Int64
Uint8
Uint16
Uint32
Uint64

Signed fixed-width integer types include negative and non-negative values within their declared bit width. Unsigned fixed-width integer types include only non-negative values within their declared bit width.

Byte is an alias for Uint8. The two names denote the same type; Byte does not introduce a distinct carrier or require a conversion to or from Uint8.

Real and floating-point types

The Real type denotes mathematical real numbers.

The Float32 and Float64 types contain the mathematical real numbers which are exactly representable as finite values in the corresponding IEEE 754 binary formats. Their carriers exclude infinities and NaN values. They also contain only one mathematical zero: the positive and negative IEEE zero encodings do not denote distinct values of these types.

Float32 and Float64 are subtypes of Real. A value of either type can therefore participate in operations inherited from Real, where it denotes its exact mathematical value.

The IeeeFloat32 and IeeeFloat64 types expose the complete corresponding IEEE 754 formats. Their carriers include finite values, positive and negative zero, positive and negative infinity, and NaN values. They are not subtypes of Real.

There are embeddings from Float32 to both Real and IeeeFloat32, and from Float64 to both Real and IeeeFloat64. The embedding into an IEEE type allows finite real-valued floats to participate in IEEE operations without making the full IEEE type a subtype of Real.

TODO: Specify whether the embedding of the single Float32 or Float64 zero into its IEEE type selects positive zero, is context-dependent, or requires an explicit choice.

Floating-point arithmetic

For operands of type Float32, both addition inherited from Real and addition inherited through IeeeFloat32 are applicable. The corresponding ambiguity also arises for Float64 and for other arithmetic operations. An implementation may treat the expression as unambiguous and select the IEEE operation, but this must be specified as part of Predica overload resolution: IEEE addition is not merely an implementation of exact real addition because the two operations have different denotations when rounding occurs.

TODO: Specify whether an unqualified arithmetic expression on Float32 or Float64 operands prefers the corresponding IEEE operation, remains ambiguous, or is resolved using the expected result type.

TODO: Specify the result types of floating-point arithmetic. In particular, decide whether Float32 + Float32 returns IeeeFloat32, returns Float32 and fails when the IEEE result is not a finite real value, or denotes exact addition and returns Real. Make the corresponding decision for Float64 and the other arithmetic operations.

TODO: Specify the carrier identity and equality of IeeeFloat32 and IeeeFloat64, including whether distinct NaN encodings denote distinct Predica values. Predica equality must be distinguished from IEEE numeric comparison, under which NaN and signed zero have special behaviour.

TODO: Specify whether the IEEE types have an ordinary Predica ordering, expose the IEEE totalOrder relation explicitly, or support only IEEE numeric comparisons.

String and Unicode types

The UnicodeCodePoint type denotes Unicode code points.

The UnicodeScalar type denotes Unicode scalar values. These are Unicode code points excluding surrogate code points.

The encoded string types are constrained vector types:

• Utf8String is a Vector<Byte> containing well-formed UTF-8.
• Utf16String is a Vector<Uint16> containing well-formed UTF-16.
• Utf32String is a Vector<Uint32> in which every element is a Unicode scalar value.

String is an alias for Utf8String. It therefore commits Predica's ordinary string representation to UTF-8 while allowing representation-specific interfaces to require Utf16String or Utf32String explicitly.

The elements of an encoded string are its code units. Consequently, indexing, length, and ordinary vector iteration are code-unit operations. Indexing a Utf8String returns a Byte, indexing a Utf16String returns a Uint16, and indexing a Utf32String returns a Uint32. These operations do not pretend that the \(i\)-th Unicode scalar can be found in constant time in a variable-width encoding.

Unicode interpretation is provided by decoding operations on encoded strings. Such operations can iterate over the UnicodeScalar values, or over those values widened to UnicodeCodePoint. For well-formed UTF-8, every decoded code point is a Unicode scalar because UTF-8 does not encode surrogate code points. Scalars, code points, grapheme clusters, and similar textual views are therefore derived from the encoded vector; they are not the stored elements of String.

Every encoded string can be used as its underlying vector of code units, but the reverse direction requires validation. Not every Vector<Byte> is a Utf8String, and not every Vector<Uint16> is a Utf16String. An operation whose result is not known to preserve encoding validity returns the underlying vector type. For example, an arbitrary byte slice of a Utf8String is not itself known to be a Utf8String.

Carrier sets of primitive types

The carriers of built-in primitive types are not defined in terms of attributes. They are specified directly as follows:

The carriers of Float32 and Float64 are subsets of Real. The carriers of IeeeFloat32 and IeeeFloat64 are instead defined by their adopted IEEE floating-point formats.

Built-in collection types

Predica provides the following built-in collection types:

• Optional<T> contains collections having either zero or one value of type T.
• Set<T> contains finite unordered sets of values of type T. A value occurs at most once in a set.
• Vector<T> contains finite sequences of values of type T. Its length is determined at run time.
• Array<T,N1,...,Nn> contains fixed-shape, \(n\)-dimensional arrays of values of type T. The static integer arguments N1 through Nn give the extent of each dimension and are part of the type. Array<T,N> is the one-dimensional case.
• MortonArray<T,N1,...,Nn> contains fixed-shape, \(n\)-dimensional arrays of values of type T. The static integer arguments N1 through Nn give the extent of each dimension and are part of the type. Elements are arranged in Morton order.
• OrderedMap<K,V> contains finite mappings from keys of type K to values of type V. Each key occurs at most once, and entries are ordered by key. The key type must therefore be ordered.
• UnorderedMap<K,V> contains finite mappings from keys of type K to values of type V. Each key occurs at most once, but the type defines no ordering of its entries.

Optional<T> is a collection type and is distinct from the attribute cardinality qualifier ?. An attribute declared T value? has an extension containing zero or one value of type T; an attribute declared Optional<T> value has an extension containing exactly one value, and that value is itself an optional collection.

Thus Set<T> represents membership without order, Vector<T> represents a run-time-length sequence, and the array types represent collections whose extents are known statically. MortonArray differs from Array by using Morton order to preserve spatial locality across multiple dimensions. The map types associate unique keys with values and differ in whether their entries have a defined key order.

Core language and standard library

Predica does not prescribe an implementation boundary between the core language and its standard library. The language specification covers both and specifies their types and behaviour as a single contract.

An implementation may provide a specified facility as a compiler primitive, as a predeclared library definition, as run-time library code, or as some combination of these. This demarcation is therefore principally an implementation detail. It must not change the meaning of a program or which specified facilities are available to it.