Types

©1998 Research Institute for Symbolic Computation (RISC-Linz)

Package Description

This package contains commands for handling types.

Usage

Implementation

Begin

TypeConstructor

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

IsTyped

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

TyVars

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

FormTypeExpr

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

DeclareType

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

EraseType

Syntax call
EraseType[, ... ,]
Input
A sequence of symbols ( 1 <= i <= n )
Effect
remove the type information attached to ( 1 <= i <= n )
Implementation

IsTypeConstructor

Syntax call
IsTypeConstructor[ term ]
Input
term : a term
Output
True if term is a declared type constructor
False otherwise
Implementation

IsFunType

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

IsFunOnCPType

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

End