5.4.14  Mythryl Types: Elementary Types and Type Constructors

“Using “Void” for a non-empty type is barbaric!”
                            —Robert Harper, co-author of The Definition of Standard ML

Type systems start with a few irreducible elementary types together with some operators which generate new types from previously existing ones. Mythryl’s type system is no exception.

Mythryl’s core elementary types are:

• Void: Like C void, this is the value returned by a function which returns nothing interesting, and the argument value given to a function which really needs no argument. There is exactly one value of this type, which is written (). (Theoreticians prefer to call this type unit, reserving void for the type which has no values at all.)
• Int: The default integer type. This has 31 bits of precision. (See below.)
• Float: The default floating point type. This has 64 bits of precision, and thus actually corresponds to C double.
• Char: One seven-bit ASCII character.

The following core Mythryl vector types are also treated as elementary:

• String: Logically a vector of Char, but treated as elementary.
• Vector: Immutable typeagnostic vectors.
• Rw_Vector: Mutable typeagnostic vectors.

The very special Exception sumtype is also predefined.

Mythryl’s core mechanisms for constructing new types from old are:

• The tuple type constructor: New_Type = (Old_Type_A, Old_Type_B, ... );
• The record type constructor: New_Type = { fieldname_a => Old_Type_A, fieldname_b => Old_Type_B, ... );
• The arrow type constructor for functions: New_Type = Argument_Type -> Result_Type;
• The Ref type constructor for declaring mutable reference cells: New_Type = Ref( Old_Type );

Finally, Mythryl’s sumtype definition facility effectively introduces new programmer-defined types and type constructors.

For example the declaration

    Color = RED | GREEN | BLUE;

effectively defines a new atomic type Color which may be used anywhere an existing elementary type like Int may be used, and the declaration

    Tree(X) = EMPTY | NODE { key: Int, value: X, left_kid: Tree(x), right_kid: Tree(X) };

effectively defines a new type constructor Tree(X) which accepts an existing type and generates a new one.

Several types which in other languages are elementary, are in Mythryl simply standard library declarations, at least in principle.

For example the the Boolean type, which is elementary in many languages, is in Mythryl defined as

    Bool = TRUE | FALSE;

in the standard library, at least in principle. (In practice, the compiler uses special hardwired knowledge of Bool in order to produce better code.)

Similarly, Mythryl lists are in theory simply a type defined in the standard library by a statement like

    List(X) = [] | (X ! List(X));

(In practice, [] and ! are not legal end-user syntax — user-defined constructors must be upper-case alphabetic — and the list construction syntax [ 12, 13, 14 ] is a completely ad hoc convenience specially hacked into the Mythryl grammar. They say that the difference between theory and practice is that in theory they are the same but in practice they are different.)

Complicating the above picture, the messy realities of computer hardware motivate the definition of a few additional elementary types. Integers come in signed and unsigned and various lengths, and the Mythryl compiler needs to know about them all ahead of time to produce good code, so we also have the elementary types

• Int1: 32-bit signed integers.
• Int2: 64-bit signed integers.
• Unt8: 8-bit unsigned integers.
• Unt1: 32-bit unsigned integers.
• Unt2: 64-bit unsigned integers.

Similarly, two additional typelocked vector types are irrelevant in principle but in practice essential to achieving good space/time efficiency:

• Unt8_Rw_Vector: Mutable vectors of 8-bit unsigned integers.
• Float64_Rw_Vector: Mutable vectors of 64-bit floating point numbers.

For those interested, some of the real-world process of defining these early types in the Mythryl compiler source code may be found in src/lib/compiler/front/semantic/symbolmapstack/base-types-and-ops.pkg;