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:

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

The very special Exception sumtype is also predefined.

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

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

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

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;

Comments and suggestions to: