<\body> program types are of type . Every typed program has a unique type. Programs types can be converted to typed programs. In other words, programs types again admit types; the type of a type is either or a category. The file |../../unstable/syntax/typ_syntax.mmx> contains several utility routines for the manipulation of program types. These utility routines are usually prefixed by or . The type is an abbreviation for . program types> Internally, a program is encoded by an expression tree of type (which equals ), each subtree being either of type or . The private conversion routines between the types and are and . The public routines for the syntactic manipulation of programs are <\explain> TYP> <|explain> Getting the type (or category) of a type. <\explain> Boolean> Literal> program is a leaf and converting a leaf to a literal.> <\explain> TYP> Boolean> Int> TYP> <|explain> Creation of a function application (the type of the function must match the types of the arguments), testing whether a program is a compound tree, obtaining the arity of a compound tree and accessing a child of a compound tree. <\explain> <|explain> Standard atomic types, which are exposed to the programmer. <\explain> <|explain> The type of a class. Classes can be converter back and forth to categories with a more precise mathematical structure. <\explain> <|explain> The type of a category. <\explain> <|explain> The type of a keyword, such as , , etc. <\explain> <|explain> Internal types for quantifications. <\explain> <|explain> Standard type constructors provided by the language, which are exposed to the programmer. <\explain> <|explain> Additional types, which are exposed to the programmer. <\explain> <|explain> Logical types. <\explain> <|explain> Free and bound types of a given category as needed during the type resolution process. <\explain> <|explain> Coerce a type so as to match a category (which may be equal to ). The extra arguments provide the necessary information for matching the category. <\explain> <|explain> 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. <\explain> <|explain> Type for indicating that the type should be matched exactly, thereby disallowing any implicit conversions during the type conversion process. <\explain> <|explain> Auxiliary type during the type conversion process, corresponding to a function type with agiven source but undetermined destination. <\explain> <|explain> For the generation of extern declarations. <\explain> Boolean> Boolean> Boolean> Boolean> Boolean> Boolean> Boolean> Boolean> Boolean> Boolean> Boolean> Boolean> Boolean> Boolean> Boolean> Boolean> Boolean> Boolean> <|explain> Predicates corresponding to , , , , , , , , , , , , , , , , and . . If you don't have this file, write to the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.> <\initial> <\collection>