Products represent types where multiple elements exist simultaneously. The operands of the product are types. The structure of a product type is determined by the fixed order of the operands.
A Product Type is a compound type formed by combining multiple types.
An instance of a product type in it's simplest form is a called a tuple.
Such a type only accepts one constructor that takes a variadic number of inputs and builds the product of them. A product type has a fixed length and the types of the elements is fixed. Formally it can be written as :
\( (x_1, x_2, ..., x_n) : T_1 \times T_2 \times ... \times T_n \)
This can be read as : the tuple is composed of elements of types \( T_1 \) to \( T_n\) with corresponding values \( x_1 \) to \( x_n \).
The corresponding definition in kumi could look like the following:
To extract values from a tuple, there are projections that are term constructors. A projection (often noted \( \pi \)) is a function that given a product type returns the elements at the desired index. Formally it is denoted as :
\( \pi_1(x) : T_1, \pi_2(x) : T_2, ..., \pi_n(x) : T_n \)
In kumi this corresponds to the get functions
A product type follows List Algebra.
Product types can also be composed of homogeneous types, such a tuple does not differ from array types. In most programming models homogeneous product types can be efficiently stored via contiguous location in memory without needing to insert padding. By definition, an homogeneous product type can be iterated on by indexing as the gap between two consecutive elements is fixed. This property does not hold for their heterogeneous counterpart.
The C++ standard library provides an implementation of a tuple type as well as some special cases. Kumi provides a generic yet optimized representation of them. Each type provided in the standard can be represented efficiently.
| STL type | Kumi |
|---|---|
| std::pair<T1,T2>; | kumi::tuple<T1,T2> |
| std::tuple<Ts...>; | kumi::tuple<Ts...> |
| std::array<T,5>; | kumi::tuple<T,T,T,T,T> |
| std::complex<T>; | kumi::tuple<T,T> |
A Record Type identifies its components by a unique label rather than a position.
An instance of a record type is called a struct in many programming languages. (Let aside considerations about object oriented progamming, inheritance, etc...)
A Record Type is the labeled version of a Product, it can be seen as the product of mathematical sets. Similarily to tuples, it accepts one constructor that takes a variadic number of input that are in this case fields.
Formally it can be written as :
\( \{l_1 : x_1, l_2 : x_2, ..., l_n : x_n\} : T_1 \times T_2 \times ... \times T_n \)
This can be read as : the record is composed of elements of types \( T_1 \) to \( T_n\) with corresponding values \( x_1 \) to \( x_n \) that are labeled with \( l_1 \) to \( l_n \).
The corresponding definition in kumi could look like the following:
To extract values from a record, there are projections that are term constructors. A projection (often noted \( \pi \)) is a function that given a product type returns the elements. In a record, projections are generally labeled instead of indexed. Formally it is denoted as :
\( \pi_{l_1}(x) : T_1, \pi_{l_2}(x) : T_2, ..., \pi_{l_n}(x) : T_n \)
In kumi this corresponds to the get functions
One could also use standard projections that are index, this simply modifies the semantic and the type that is returned. Where \( T \) denotes the type of the value stored in a record, \( \{l:T\} \) denotes the combination of the label and the type of the field. This is the return type of an indexed access on a record.
It follows Set Algebra on top of List Algebra.
Operation on records are traditionally not structural in the sens that they operate per label, never per element. However, as they are internally represented by a tuple, such operation are permitted. As an example, one could "rotate" a record \( n \) positions to the left. Mathematically this might not make a lot of sens whereas for a programmer that has to consider memory representation, this is potentially critical to have.
Reference Wikipedia: Tuple Reference Wikipedia: Record
