M. Widera and C. Beierle. **Function Types in
Complete Type Inference**. In Sharon Curtis and Kevin Hammond,
editors, Proceedings of the 3rd Scottish Functional
Programming Workshop, 2001.

#### Remark:

This abstract contains a large number of special
characters, which are not available in HTML. These characters
are denoted as LaTeX source code.
#### Abstract:

We study type checking that is complete in the
sense that it accepts every program whose subexpressions can all be
executed without raising a type error at runtime. In a complete
type checker for every function call (f a) of a function f with an
argument expression a of type t_a it is checked whether f is
applicable to one of the possible values of a, i.e.\ whether
<[t_a]> \cap dom(f) \not= Ø holds where <[t]> denotes
the semantics of a type t. When approximating dom(f) by a type
t_{in} it turns out that the usual function type constructor is not
appropriate for complete type checking: for a function type t_f =
t_{in} -> t_{out} of f the input type t_{in} is usually not
guaranteed to contain all values of dom(f) and the test for common
elements can erroneously fail. We therefore introduce an alternative
notion of function types, called I/O-representation, where the input
types cover a superset of the domain of the denoted functions. We
show that this notion of function types fits into the framework of
complete type checking much better than the usual function type
constructor. Moreover, we argue that complete type checking
overcomes the disadvantages of soft-typing approaches by enabling
the *rejection* of programs instead of just raising a warning.

Available:
PS,
PDF,
BibTeX