Infinity Lang Type System

Documentation and implementation of the Infinity language type system.

All types within the Infinity language are treated as abstract refinements of infinity.

One side-effect of this is that there are no concrete fixed-width types. That isn't to say that types with a fixed bit-width do not exist in ilang (e.g. Int32, Real32, Nat32, etc.) but that they simply do not have a single universal underlying type.

This can usually be treated as an implementation detail. E.g. on a system with no support for 16-bit integers, Int16 may be represented by the C type int32_t but on other (more traditional) systems it would more probably be represented by int16_t.

Building

Required dependencies:

• CMake
• A C++17 Compiler

To save you the scrolling, the following commands should be used to build the system:

mkdir build && cd build
cmake ..
cmake --build .

Defining a Type

We can think of a type as a restriction on the range of values of some other type. This concept applies to all types in the system, so there must be some type that can represent every value.

This is explicitly every value and not just any value; an instance of this type would hold every single possible value (not just any single one of them) including itself.

This type is named the Infinity type and all types are based on it at the lowest level.

Infinity

Infinity is recursively defined as the refined type of itself and is named so because it stands for the the infinite set containing every possible value known (and unknown) to man. We can not actually create a value of this type (for obvious reasons) but we can refine it to get sub-groups of values e.g. the Complex or Rational numbers.

Root Types

A root type is any type directly refined from Infinity. They are used as the base for value types.

Common root types:

Description	Root Type
An atomic mathematical unit	Number
A string of characters	String
Mapping from keys to values	Map K T
A tree with node values of T	Tree T

Refined Types

A refined type is any type based on a root type or other refined type that can not be directly instantiated. They are called refined types because they are more refined than a root type, but not refined enough to be used directly for values.

Here is a list of common refined types:

Description	Refined Type	Base	C/C++ Type analogue
A linear list of values of T	List T	Tree T	N/A
A contiguously laid out series of T values	Array T	List T	N/A
Complex numbers	Complex	Number	std::pair<Real, Imaginary>
Imaginary numbers	Imaginary	Complex	_Imaginary Real
Real numbers	Real	Complex	float or double
Rational Real numbers	Rational	Real	std::pair<Integer>
Whole numbers	Integer	Rational	int
Counting numbers	Natural	Integer	unsigned int

Value Types

Value types are any refined type that has been sufficiently refined such that a value of that type is representable/instantiable in a finite amount of space and time.

Here is a list of commonly used value types:

In this list, wherever a type is suffixed by an uppercase N, N stands for some desired bit-width.

Value Type	Base Type	Value Syntax	C/C++ Type analogue
StaticArray T N	Array T	[1, -10, 26], [0..9], ...	std::array<T, N>
DynamicArray T	Array T	Same as StaticArray	std::vector<T>
NaturalN	Natural	0, 1, 2, 3, ...	uintN_t
IntegerN	Integer	1, 0, -1, -2, ...	intN_t
RationalN	Rational	1/3, 2/7, 6/21, ...	div_t, ldiv_t, etc.
RealN	Real	0.1, 1.1111, 69.420, 9001, ...	float, double or long double

Composite Types

Composite types are used to construct more complicated types from other types. A composite type may fall into the category of 'refined' or 'value' depending on the types used to construct it.

Name	Base Type	Type Syntax	Value Syntax	C/C++ Type analogue
Ordered map	Map K T	OrderedMap K T	["x0" -> x0, "x1" -> x1, "xn" -> xn...]	std::map<K, T>
Unordered map	Map K T	UnorderedMap K T	Same as above	std::unordered_map<K, T>
Sum type (Descriminated Union)	Infinity	T | U...	Any value of any one of the summed types	std::variant<T, U...>
Product type / Tuple	Infinity	T * U...	(1, "Hello")	std::tuple<T, U...>
Object / Struct	Infinity	{x: T, xs: U...}	Constructor based	struct{ T x; U xs...; }

Type Promotion

Type promotion may only occur from a more refined type to it's base. No lossy conversion is ever performed; if this is required a type conversion is necessary.

Type Conversion

This is the process of converting a value from one group to a non-related group.