Type Declarations
The primitive type is used to annotate any s-expression. The notation is
(type X α)
as in '(type X number)'. This is not in any sense a normal function since the type α is discarded
in evaluation (i.e. (type X α) evaluates to the normal form of X. The type declaration
is not ignored by the type checker which actually expects the expression to have the type attached to it
and will signal an error if this is not so.
The degree to which any implementation of Kλ uses the information provided by this annotation will depend
on the platform and the implementation. Shen 11 and later will, if required, automatically generate copious
type annotations in Kλ which can be used by Kλ implementors or platform providers of Shen to optimise the
resultant code. The command '(optimise +)' enables this feature. The default is '(optimise -)'.
Optimisation of the type declarations in a type checked Shen function F is expected to preserve the I/O
features of F only with respect to type secure input. Thus
(define =n
{number --> number --> boolean}
N N -> true
_ _ -> false)
may return an error on non-numeric inputs when optimised. |
