©1998 Research Institute for Symbolic Computation (RISC-Linz)
This package contains commands for handling types.
Syntax call
TypeConstructor[, ... , ]
Input
a sequence , ... , of Mathematica symbols
Output
the list { , ... , }
Effect
declare , ... , as type constructors by extending the default definition of IsTypeConstructor
declare , ... , as constructors by extending the default definition of IsConstructor
Implementation
Syntax call
IsTyped[ term ]
Input
term : a term
Output
True if term is a typed symbol, i.e. a typed variable or a typed operator
False otherwise
Implementation
Syntax call
TyVars[&tgr;]
Input
&tgr; : a type expression
Output
the set of type variables appearing in &tgr;;
type variable is any Mathematica symbol which is not a declared type constructor
Implementation
Syntax call
FormTypeExpr[ type--vars, &tgr; ]
Input
Output
an object F such that every call F[ ] returns a pair {type--vars', &tgr;'} where
Usage
F is the encoding of the polymorphic type &tgr; .
It can be used for generating valid instances of polymorphic type expressions during type checking (Tc and TcX calls).
Implementation
Syntax call
DeclareType["7, ... ,"7]
Input
A sequence of type signatures "7 ( 1 <= i <= n )
Output
The list {,. .. ,} of declared function symbols
Side Effect
assign the (polymorphic) type to ( 1 <= i <= n )
Implementation
Syntax call
EraseType[, ... ,]
Input
A sequence of symbols ( 1 <= i <= n )
Effect
remove the type information attached to ( 1 <= i <= n )
Implementation
Syntax call
IsTypeConstructor[ term ]
Input
term : a term
Output
True if term is a declared type constructor
False otherwise
Implementation
Syntax call
IsFunType[ &tgr; ]
Input
&tgr; : a type expression
Output
True if &tgr; is of the form → (i.e. a function type)
False otherwise
Implementation
Syntax call
IsFunOnCPType[ &tgr; ]
Input
&tgr; : a type expression
Output
True if &tgr; is of the form ô "ï ô õ% ( i.e. a Cartesian product)
False otherwise
Implementation