2. Types

Felix provides a rich type system. It consists of the types and features described below.
1. System Types
These are system intrinsic types supported by the compiler. The most important of these are the function and procedure types, but also include special system intrinsics such as procedure continuations.
2. Standard Library Types
These are standard types provided by the library. They include primitives such as boolean, integral and floating numeric types, algebraic types including lists, arrays, and options, and various containers.
3. Type Constructors
These are not types, but methods of combining types. There are two classes:
1. Anonymous Types
These are types denoted by an expression. Whilst they may be given aliases or abbreviations with a typedef, these types are identified by their structure.
2. Nominal Types
These are types specified by a declaration which gives them an identifying name. Each declaration denotes a distinct types. Nominal types include structs and unions.
4. Type Bindings
Type bindings specify types mapping C++ types into the Felix type system. There are several kinds of binding and associated infrastructure, including primitive (abstract) types, cstructs (which are mappings of C structs and unions),
5. Parameterised types: polymorphism
Most type constructors in Felix can be polymorphic.
6. Metatyping
These are not types, but functions which generate types. The type language is a superset of the typed lambda calculus, type functions providing abstraction. However the system also supports the notions of products and sums of types, intersection types, and constraints. The types of these types are called kinds, and kinds themselves are metatyped with the same metatyping system.
7. Type Constraints
8. Overloading

2.1. Function Types

Felix provides two function types, Felix and C function types.

2.1.1. Felix Function Types

Felix function closure types are denoted by:
   D -> C
where D is the domain and C the codomain types. The binary combinator -> is left associative. Values of such a type are constructed by forming closures of function classes which are denoted by a function definition.

Closures bind to the instance of their environment denoted by lexical scoping together with control flow rules, and remain live at least while there is a live reference to them. The local part of a closure denoted by a function is called the stack frame for historical reasons, and the list of stack frames comprising that of the function and its ancestors is known as the display, also for historical reasons.

Closures are applicative objects which can be applied to a value of their domain type D, and which return a value of their codomain type C.

Neither the domain D nor codomain C of a function type may be void.

The special abbreviation:

   {C}
may be used to denote the function type:
   unit -> C
and thus represents lazy evaluation of the function. For example:
  {2}
is the encoding of a boolean predicated on the environment.

Functions may not have side effects. See fundeffor details of defining function classes.

2.1.2. C Function Types

Felix also provides direct access to C functions, whose type is denoted by:
   D --> C
Note that C function closures certainly exist, however they bind only to their primitive static environment.

2.1.3. Procedure Types

A procedure is a subroutine which may and generally should have side-effects and which does not return a value. Procedures have types denoted by one of:
   D -> 0
   D -> void
where D may not be void. (void is an alias for 0 defined in the standard library).

Felix procedures values are constructed by forming the closure of a procedure class. Procedures are quite distinct from functions, since they may participate in synchronous multithreading, whereas functions may not. See syncfor details on synchronous threading. See procdeffor details of defining procedure classes.

2.2. Anonymous Types

An anonymous type is one which is identified by its structure rather than a declared name.

2.2.1. Tuple Types

A tuple is a categorical products whose projection functions are identified positionally, using non-negative integer constant indicies. n-ary tuples exist for all non-negative values of n other than 1. Tuples of one component of type T are identified with type T. The nullary tuple type is denoted by
  1
  unit
where 'unit' is aliased to 1 in the standard library. The sole value of unit type is denoted:
  ()
An n-ary tuple type, of components T0, T1, ... is denoted by:
  T0 * T1 * T2 * ...
and values are denoted:
  v0, v1, v2, ...
You should note that the chain operator * is not associative, although it is associative up to isomorphism.

Tuples support two destructors. The form

  x.(0)
  x.(1)
  ...
can be used with a constant expression denoting the projection. You can also use a tuple pattern in a match expression
  match x with
  | ?v1,?v2, .. => ..
  endmatch

2.2.2. Array Types

A tuple of 2 more or more components, all of which are the same type T, is known as an array. The special sugar
  T ^ n
may be used for arrays of manifestly fixed length, where n is a literally given integer constant. Array values are the same as tuple values, since arrays are just special cases of tuples. However the special notation like:
  [| 1,2,3 |]
can be used for arrays, which results in a compile time error if the component values are not all the same type.

2.2.3. Record Types

A record type is a variant on a tuple, in which the components are named rather than numbered. The types are denoted like:
  struct {
    a:int;
    b:string;
    c:double;
  }
and values are constructed like:
  struct {
    a=1;
    c= 9.2;
    b:string="Hello";
  }
Record types support a generic coercion operation which allows the formation of a new record with a subset of the fields of the argument record, the type of this record is a subtype. See record coercion.

Records can be accessed by the usual dot notation:

  x.a
or using pattern matches:
  match x with
  | struct { a=?i; b=?s; } =>
  ...
Note that record patterns need only match a subtype of the record, that is, only some of the field names need be given.

2.2.4. Sum Types

Sum types are use to express numbered cases. An n-ary sum type, of case types T0, T1, ... is denoted by:
  T0 + T1 + T2 + ...
and variant values are denoted by
  (case 0 of T0 + T2 ...) v0
  (case 1 of T0 + T2 ...) v1
  (case 2 of T0 + T2 ...) v2
  ...
In addition, a sum of n units has the special name:
  n
where n is an non-negative integral constant. Three of these have standard names given by these typedefs:
  typedef void = 0;
  typedef unit = 1;
  typedef bool = 2;
These two variants have standard names:
  case 0 of 2 // false
  case 1 of 2 // true
Sums can be destroyed in pattern matches:
  match x with
  | (case 1) ?a => ...
Note that the sum type does not need to be named, since it is determined by the match argument type.

Note that sum type constructors can also be used as functions, like Haskell but unlike Ocaml. The compiler generates a wrapper function to form the closure automatically on such usage.

The standard function caseno can be used to obtain the zero origin ariant index:

  var x : int = caseno (case 1 of 2); // x is 1

2.2.5. Pointer Types

A Felix pointer to T is denoted by the notation:
  &T
A pointer can be formed by addressing a var kind of variable, and dereferenced in the usual way:
  var x : int = 1;
  var px : &int = &x;
  var y : int = *px; // y is now 1
Pointers cannot dangle: it is safe to address a local variable. Pointers cannot be set to NULL in the abstract language, although they can become NULL by use of facilities in the C_hack module of the standard library. They cannot be incremented or added to.

2.2.6. Type Recursion

Felix provides a fixpoint operator for typing:
  t as v
where v is an identifier in t. For example a list of int may be given by:
  1 + int * ilist as ilist
The postfix fixpoint operator has a low precedence. This encoding is equivalent to:
  typedef ilist = 1 + int * ilist;
except that the former is an expression, allowing the type to be used in combinator form without defining a named alias.

2.3. Nominal Types

A nominal type is one which is declared and identified by its name. Two nominal types may have the same structure and representation, but remain distinct.

2.3.1. Struct Types

Felix struct type definitions resemble C++:
  struct X {
    a : int;
    b : long;
  };
All structs are provided with constructors with the same name as the struct, and which take a tuple argument with the same components in order:
  var x = X(1,2L);
This construction is efficient: tuple and all struct types with the same sequence of components always have the members at the same offsets, and thus are representation compatible.

2.3.2. Union Types

Felix union type definitions come in two flavours: the ML form:
  union X =
    | a of int
    | b of long
  ;
and the C form:
  union X {
    a : int;
    b : long;
  };
These flavours are equivalent. However the ML form also supports constructors without arguments:
  union X =
    | a of int
    | b of long
    | c
  ;
Values of a union type are written like function applications, or constants:
  var x1 : X = a 1;
  var x2 : X = b 1L;
  var x3 : X = c;
Constructor names can be overloaded like ordinary functions. Unions can be decoded with pattern matches:
  match x with
  | a ?x1 => ..
  | b ?x2 => ..
  | c => ..
and the zero origin case number can be found with the caseno function:
  var x : int = caseno (a ?1) ; // x is 0

2.3.3. Enumeration Types

If all the variants of a union have no arguments, the shorthand:
  enum X { a, b=7, c };
can be used. In this form, an equal sign followed by an non-negative integral constant provides a way of fixing the case index. Case indicies are assigned as in C, starting at zero, and each component other than the first being assigned an index one higher than the previous one. Note duplicates and missing cases are both permitted.

2.3.4. Class Types

Felix classes are defined like:
class Y {
  val c : int;
  private var x : int;

  fun fetchc():int =>c+1;
  private fun fetchx():int =>x;
  proc setx(a:int) { x = a; }
  ctor (a:int): x(20000),c(1000) { x = a; }
};
Classes may contain, val, var, fun and proc definitions. Val's may be initialised in constructors but not otherwise modified. The special function introduced by the ctor keyword introduces a constructor, with C++ style member initialiser list.

Class members are all public by default. Var, val, proc and fun members can be declared private, in which case they can only be accessed within a method of the class.

Unlike structs, classes are always passed by reference, that is, a class value is actually a pointer.

Unlike C++, Felix supports method object closures:

  var y <- new Y;
  val f = y.fetchc;  // object closure
  print (f 1); endl; // value of y's c variable + 1
A special new statement is used to construct classes with the form shown above. Constructors are overloaded in the usual way. As a special case one default constructor may be given and called without arguments, even though it really has a unit argument. Note that constructors exist in the scope containing a class definition and are not methods.

Methods exist within class scope and cannot be overloaded.

2.4. Primitive Types

Felix provides a method for importing C/C++ types into Felix:
  type myint = "int";
Such definitions provide the user a way to introduce new primitive types into Felix. Such types are considered abstract. The C++ type must be allocable, default and copy constructible, copy assignable, and destructible, that is, they must be first class data types.

It is also possible to introduce non-first class types, with the adjective incomplete:

  incomplete type myvoid = "void";
Such types can only be used as the argument of some kind of pointer type constructor, or to instantiate a type variable in binding context for which it is suitable.

See Unknown Label:bindings for more information on bindings.

2.5. Standard Types

2.5.1. System Types

2.5.1.1. Fibres

Felix provides a system of cooperative multithreading based on resumable procedural continuations and channels.

The following basic types are defined as bindings to the underlying C++ technology. They are:

TypeRole
Control::fthreadThread of control
Control::contProcedural Continuation
Control::schannel[t]Bidirectional Channel
Control::ischannel[t]Input Channel
Control::oschannel[t]Output Channel

The following operations are used to manage these entities. ...

2.5.2. Arithmetic Types

Felix provides the following standard C arithmetic types. They can be named with any of the usual C names with contractions, or using a Felix alias:

Felix nameFull C name
tinysigned char
utinyunsigned char
shortsigned short int
ushortunsigned short int
intsigned int
uintunsigned int
longsigned long int
ulongunsigned long int
vlongsigned long long
uvlongunsigned long long
floatfloat
doubledouble float
ldoublelong double float

The following aliases are also provided, in this case the C name may not be used:

Felix nameC name
sizesize_t
ptrdiffptrdiff_t
intptrintptr_t
uintptruintptr_t
intmaxintmax_t
uintmaxuintmax_t

The following aliases for exact integers are also provided, in this case the C name may not be used:

Felix nameC name
int8int8_t
uint8uint8_t
int16int8_t
uint16uint16_t
int32int32_t
uint32uint32_t
int64int64_t
uint64uint64_t

Felix guarantees all these integer aliases exist, even if the C99 counterparts do not.

Complex number are provided with one of the follwing bindings, dependent on the configuration.

Felix nameC name
complexfloat _Complex
dcomplexdouble _Complex
lcomplexlong double _Complex

OR

Felix nameC++ name
complexstd::complex<float>
dcomplexstd::complex<double>
lcomplexstd::complex<long double>

The choice between C99 and C++ complex types is implementation dependent and very unfortunate.

In all these cases, where a long version of a type is not provided by C or C++, such as long long and long double, a distinct replacement type is used instead, to ensure C++ level overloads are distinct.

[NOTE: THIS IS NOT IMPLEMENTED. The current system just uses an alias.]

Arithmetic types support the same operations as ISO C99. For the purpose of specifying bitwise operations on signed types, they use a full two's complement representation. Systems on machines with other representations must provide the appropriate glue logic.

Overflow of operations on signed types is undefined behaviour. Operations on unsigned types cannot overflow because it is defined as the modular residual of the underlying operation on integers.

Thus, operations on exact unsigned integral types are fully deterministic, and operations on signed integral types are also deterministic when it does not overflow.

Felix also guarantees 'long' is at least twice the length of 'short'.

[NOTE: THIS IS NOT IMPLEMENTED. Config check required.]

2.5.3. Character and String Types

Felix provides 3 character types:
Felix nameC++ nameNotes
charchar
wcharwchar_t
ucharint32_t
and these string types:
Felix nameElement TypeC++ name
stringcharstd::basic_string<char>
wstringwcharstd::basic_string<wchar_t>
ustringucharstd::basic_string<int32_t>
Use of wchar and wstring is strongly discouraged, and is only provided for compatibility. Char is guaranteed to be an 8 bit clean representation. Note that unicode character type uchar is signed two's complement full 32 bit encoding. Characters support comparison and addition and subtraction of int.

2.5.4. Container Types