Types

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

NO WARRANTY

Package Description

This package contains commands for handling types.

[Graphics:Typesgr2.gif][Graphics:Typesgr1.gif]

Usage

[Graphics:Typesgr2.gif][Graphics:Typesgr3.gif]

[Graphics:Typesgr2.gif][Graphics:Typesgr4.gif]

[Graphics:Typesgr2.gif][Graphics:Typesgr5.gif]

[Graphics:Typesgr2.gif][Graphics:Typesgr6.gif]

[Graphics:Typesgr2.gif][Graphics:Typesgr7.gif]

[Graphics:Typesgr2.gif][Graphics:Typesgr8.gif]

[Graphics:Typesgr2.gif][Graphics:Typesgr9.gif]

[Graphics:Typesgr2.gif][Graphics:Typesgr10.gif]

[Graphics:Typesgr2.gif][Graphics:Typesgr11.gif]

[Graphics:Typesgr2.gif][Graphics:Typesgr12.gif]

[Graphics:Typesgr2.gif][Graphics:Typesgr13.gif]

[Graphics:Typesgr2.gif][Graphics:Typesgr14.gif]

[Graphics:Typesgr2.gif][Graphics:Typesgr15.gif]

[Graphics:Typesgr2.gif][Graphics:Typesgr16.gif]

[Graphics:Typesgr2.gif][Graphics:Typesgr17.gif]

Implementation

Begin

[Graphics:Typesgr2.gif][Graphics:Typesgr18.gif]

TypeConstructor

Syntax call
TypeConstructor
[[Graphics:Typesgr19.gif], ... , [Graphics:Typesgr20.gif]]
Input
a sequence [Graphics:Typesgr21.gif], ... , [Graphics:Typesgr22.gif] of Mathematica symbols
Output
the list { [Graphics:Typesgr23.gif], ... , [Graphics:Typesgr24.gif]}
Effect
declare [Graphics:Typesgr25.gif], ... , [Graphics:Typesgr26.gif] as type constructors by extending the default definition of IsTypeConstructor
declare [Graphics:Typesgr27.gif], ... , [Graphics:Typesgr28.gif] as constructors by extending the default definition of IsConstructor
Implementation

[Graphics:Typesgr2.gif][Graphics:Typesgr29.gif]

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

[Graphics:Typesgr2.gif][Graphics:Typesgr30.gif]

TyVars

Syntax call
TyVars[&tgr;]

Input
&tgr; : a type expression
Output
the set [Graphics:Typesgr31.gif]of type variables appearing in &tgr;;
type variable is any Mathematica symbol which is not a declared type constructor
Implementation

[Graphics:Typesgr2.gif][Graphics:Typesgr32.gif]

FormTypeExpr

Syntax call
FormTypeExpr[ type--vars, &tgr; ]
Input

[Graphics:Typesgr33.gif]
Output
an object F such that every call F[ ] returns a pair {type--vars', &tgr;'} where
[Graphics:Typesgr34.gif]
Usage
F is the encoding of the polymorphic type [Graphics:Typesgr35.gif]&tgr; .
It can be used for generating valid instances of polymorphic type expressions during type checking (Tc and TcX calls).
Implementation

[Graphics:Typesgr2.gif][Graphics:Typesgr36.gif]

DeclareType

Syntax call
DeclareType[
[Graphics:Typesgr37.gif]"7[Graphics:Typesgr38.gif], ... ,[Graphics:Typesgr39.gif]"7[Graphics:Typesgr40.gif]]
Input
A sequence of type signatures [Graphics:Typesgr41.gif] "7[Graphics:Typesgr42.gif] ( 1 <= i <= n )
Output
The list {[Graphics:Typesgr43.gif],. .. ,[Graphics:Typesgr44.gif]} of declared function symbols
Side Effect
assign the (polymorphic) type [Graphics:Typesgr45.gif][Graphics:Typesgr46.gif] to [Graphics:Typesgr47.gif] ( 1 <= i <= n )
Implementation

[Graphics:Typesgr2.gif][Graphics:Typesgr48.gif]

[Graphics:Typesgr2.gif][Graphics:Typesgr49.gif]

[Graphics:Typesgr2.gif][Graphics:Typesgr50.gif]

EraseType

Syntax call
EraseType[
[Graphics:Typesgr51.gif], ... ,[Graphics:Typesgr52.gif]]
Input
A sequence of symbols [Graphics:Typesgr53.gif] ( 1 <= i <= n )
Effect
remove the type information attached to [Graphics:Typesgr54.gif] ( 1 <= i <= n )
Implementation

[Graphics:Typesgr2.gif][Graphics:Typesgr55.gif]

IsTypeConstructor

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

[Graphics:Typesgr2.gif][Graphics:Typesgr56.gif]

IsFunType

Syntax call
IsFunType[ &tgr;
]
Input
&tgr; : a type expression
Output
True if &tgr; is of the form [Graphics:Typesgr57.gif][Graphics:Typesgr58.gif] (i.e. a function type)
False otherwise
Implementation

[Graphics:Typesgr2.gif][Graphics:Typesgr59.gif]

IsFunOnCPType

Syntax call
IsFunOnCPType[ &tgr; ]

Input
&tgr; : a type expression
Output
True if &tgr; is of the form [Graphics:Typesgr60.gif] " [Graphics:Typesgr61.gif]% [Graphics:Typesgr62.gif] ( i.e. a Cartesian product)
False otherwise
Implementation

[Graphics:Typesgr2.gif][Graphics:Typesgr63.gif]

End

[Graphics:Typesgr2.gif][Graphics:Typesgr64.gif]

[Graphics:Typesgr2.gif][Graphics:Typesgr65.gif]