Sciweavers

SFP
2001

Function Types in Complete Type Inference

13 years 11 months ago
Function Types in Complete Type Inference
: 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 ta it is checked whether f is applicable to one of the possible values of a, i.e. whether [ta] dom(f) = /0 holds where [t] denotes the semantics of a type t. When approximating dom(f) by a type tin it turns out that the usual function type constructor is not appropriate for complete type checking: for a function type tf = tin tout of f the input type tin 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 ty...
Manfred Widera, Christoph Beierle
Added 31 Oct 2010
Updated 31 Oct 2010
Type Conference
Year 2001
Where SFP
Authors Manfred Widera, Christoph Beierle
Comments (0)