Program types

Mathemagix program types are of type TYP. Every typed program p: PRG has a unique type p.t. Programs types can be converted to typed programs. In other words, programs types again admit types; the type of a type is either $Class or a category. The file typ_syntax.mmx contains several utility routines for the manipulation of program types. These utility routines are usually prefixed by $ or typ$. The type TYPS is an abbreviation for Vector TYP.

Internal representation of Mathemagix program types

Internally, a TYP program is encoded by an expression tree of type GEN (which equals Generic), each subtree being either of type Literal or Compound. The private conversion routines between the types TYP and GEN are postfix .v and typ. The public routines for the syntactic manipulation of MMX programs are

postfix .t: TYP -> TYP

Getting the type (or category) of a type.

literal?: TYP -> Boolean

convert: TYP -> Literal

Testing whether a TYP program is a leaf and converting a leaf to a literal.

postfix (): (TYP, Tuple TYP) -> TYP

compound?: TYP -> Boolean

prefix #: TYP -> Int

postfix []: (TYP, Int) -> TYP

Creation of a function application (the type of the function must match the types of the arguments), testing whether a TYP program is a compound tree, obtaining the arity of a compound tree and accessing a child of a compound tree.

Atomic types

$Void: TYP

$Volatile: TYP

$Boolean: TYP

$Int: TYP

$Double: TYP

$String: TYP

$Generic: TYP

$Literal: TYP

$Compound: TYP

$Syntactic: TYP

$Exception: TYP

$Environment: TYP

$Printer: TYP

$This: TYP

Standard atomic types, which are exposed to the programmer.

$Class: TYP

The type of a class. Classes can be converter back and forth to categories with a more precise mathematical structure.

$Category: TYP

The type of a category.

$Keyword: TYP

The type of a keyword, such as if, for, etc.

$Any: TYP

$Aux: TYP

Internal types for quantifications.

Compound types

$Alias (tp: TYP): TYP

$Cross (tps: Tuple TYP): TYP

$Tuple (tp: TYP): TYP

$Generator (tp: TYP): TYP

$Function (srcs: TYPS, dest: TYP): TYP

Standard type constructors provided by the language, which are exposed to the programmer.

$Vector (tp: TYP): TYP

$Table (ftp: TYP, ttp: TYP): TYP

Additional types, which are exposed to the programmer.

$And (tps: Tuple TYP): TYP

$Or (tps: Tuple TYP): TYP

$Forall (ql: PRGS, tmpl: TYP): TYP

$Exists (ql: PRGS, tmpl: TYP): TYP

Logical types.

$Free (i: Int, car: TYP): TYP

$Bound (i: Int, car: TYP): TYP

Free and bound types of a given category as needed during the type resolution process.

$Coerce (tp: TYP, cat: TYP, x: Tuple PRG): TYP

Coerce a type so as to match a category cat (which may be equal to $Class). The extra arguments x provide the necessary information for matching the category.

$Penalty (p: Penalty, tp: TYP): TYP

Explicitly integrate a penalty into a type. This is for instance useful during the type conversion process, where only the source and destination types are exposed and not the corresponding values.

$Explicit (tp: TYP): TYP

Type for indicating that the type tp should be matched exactly, thereby disallowing any implicit conversions during the type conversion process.

$Dual (ftp: TYP): TYP

Auxiliary type during the type conversion process, corresponding to a function type with a given source but undetermined destination.

$Extern (tp: TYP): TYP

For the generation of extern declarations.

Alias?: TYP -> Boolean

Cross?: TYP -> Boolean

Tuple?: TYP -> Boolean

Generator?: TYP -> Boolean

Function?: TYP -> Boolean

Vector?: TYP -> Boolean

Table?: TYP -> Boolean

And?: TYP -> Boolean

Or?: TYP -> Boolean

Forall?: TYP -> Boolean

Exists?: TYP -> Boolean

Free?: TYP -> Boolean

Bound?: TYP -> Boolean

Coerce?: TYP -> Boolean

Penalty?: TYP -> Boolean

Explicit?: TYP -> Boolean

Dual?: TYP -> Boolean

Extern?: TYP -> Boolean

Predicates corresponding to $Alias, $Cross, $Tuple, $Generator, $Function, $Vector, $Table, $And, $Or, $Forall, $Exists, $Free, $Bound, $Coerce, $Penalty, $Explicit, $Dual and $Extern.

Permission is granted to copy, distribute and/or modify this document under the terms of the GNU General Public License. If you don't have this file, write to the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.