Type Checker

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

NO WARRANTY

Package Description

This package contains the implementation of the type checker used by the CFLP calculus. The type checker is based on the Hindley--Milner type system.

[Graphics:TypeCheckergr2.gif][Graphics:TypeCheckergr1.gif]

Usage

[Graphics:TypeCheckergr2.gif][Graphics:TypeCheckergr3.gif]

Implementation

Begin

[Graphics:TypeCheckergr2.gif][Graphics:TypeCheckergr4.gif]

[Graphics:TypeCheckergr2.gif][Graphics:TypeCheckergr5.gif]

NewTyVar

Syntax call
NewTyVar
[ ]
Output
a fresh type variable
Implementation

[Graphics:TypeCheckergr2.gif][Graphics:TypeCheckergr6.gif]

Tc

Syntax call
Tc
[ term ]
Input
term
: a term
Output
the type of term if term is well typed
"⊥" otherwise
Implementation

[Graphics:TypeCheckergr2.gif][Graphics:TypeCheckergr7.gif]

TcX

Syntax call
TcX
[ term, &tgr; , type--eqs, type--vars ]
Input
[Graphics:TypeCheckergr8.gif]
Output
a pair {type--eqs', type--vars'} where
[Graphics:TypeCheckergr9.gif]
Implementation

[Graphics:TypeCheckergr2.gif][Graphics:TypeCheckergr10.gif]

TcXList

Syntax call
TcXList
[{ term1, term2, ... }, { type1, type2, ... }, type--eqs, type--vars ]
Input
[Graphics:TypeCheckergr11.gif]
Output
a pair {type--eqs', type--vars'} where
[Graphics:TypeCheckergr12.gif]
Implementation

[Graphics:TypeCheckergr2.gif][Graphics:TypeCheckergr13.gif]

ListToCons

Syntax call
ListToCons
[ expr ]
Input
a Mathematica expression expr
Output
the expression obtained from expr by replacing all Mathematica lists that are not lambda arguments
with the corresponding CFLP lists.
Implementation

[Graphics:TypeCheckergr2.gif][Graphics:TypeCheckergr14.gif]

End

[Graphics:TypeCheckergr2.gif][Graphics:TypeCheckergr15.gif]

[Graphics:TypeCheckergr2.gif][Graphics:TypeCheckergr16.gif]