|
Arthur I. Baars and S. Doaitse Swierstra. Typing Dynamic Typing. Proc. ICFP '02, 2002.
We show how, by a careful use of existentially and universally quantified types, one may achieve the [effect of dynamic typing], without extending the language with new or unsafe features. The techniques explained are universally applicable, provided the core language is expressive enough; this is the case for the common implementations of Haskell. The techniques are used in the description of a type checking compiler that, starting from an expression term, constructs a typed function representing the semantics of that expression. In this function the overhead associated with the type checking is only once being paid for; in this sense we have thus achieved static type checking.
They construct a calculus of proofs of type equality. A dynamically typed value is a value paired with a representation of its type. It is eliminated by passing a representation of the expected type, and exhibiting a witness proof that shows the expected type is equal to the one stored with the value.
|
Typing Dynamic Typing