Ambiguity and context-dependent overloading.
No Thumbnail Available
Date
2013
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
This paper discusses ambiguity in the context of
languages that support context-dependent overloading, such
as Haskell. A type system for a Haskell-like programming
language that supports context-dependent overloading and
follow the Hindley-Milner approach of providing contextfree
type instantiation, allows distinct derivations of the same
type for ambiguous expressions. Such expressions are usually
rejected by the type inference algorithm, which is thus
not complete with respect to the type system. Also, Haskell’s
open world approach considers a definition of ambiguity that
does not conform to the existence of two or more distinct type
system derivations for the same type. The article presents an
alternative approach, where the standard definition of ambiguity
is followed. A type system is presented that allows only
context-dependent type instantiation, enabling only one type
to be derivable for each expression in a given typing context:
the type of an expression can be instantiated only if required
by the program context where the expression occurs. We
define a notion of greatest instance type for each occurrence
of an expression, which is used in the definition of a standard
dictionary-passing semantics for core Haskell based on
type system derivations, for which coherence is trivial. Type
soundness is obtained as a result of disallowing all ambiguous
expressions and all expressions involving unsatisfiability
in the use of overloaded names. Following the standard definition
of ambiguity, satisfiability is tested—i.e., “the world
is closed” —if only if overloading is (or should have been)
resolved, that is, if and only if there exist unreachable variables in the constraints on types of expressions. Nowadays,
satisfiability is tested in Haskell, in the presence of multiparameter
type classes, only upon the presence of functional
dependencies or an alternative mechanism that specifies conditions
for closing the world, and that may happen when there
exist or not unreachable type variables in constraints. The
satisfiability trigger condition is then given automatically,
by the existence of unreachable variables in constraints, and
does not need to be specified by programmers, using an extra
mechanism.
Description
Keywords
Type systems, Semantics
Citation
RIBEIRO, R. G.; FIGUEIREDO, C. C. de. Ambiguity and context-dependent overloading. Journal of the Brazilian Computer Society, v. 19, n. 3, p. 313-324, set. 2013. Disponível em: <https://link.springer.com/article/10.1007/s13173-013-0103-0>. Acesso em: 27 jul. 2017.