A Typical Synergy : Dynamic types and generalised algebraic datatypes

Autor: Noort, T. van, Achten, P., Plasmeijer, R., Scholz, S.-B.
Přispěvatelé: Scholz, S.-B.
Rok vydání: 2011
Předmět:
Zdroj: Lecture Notes in Computer Science ; 6041, 179-197. Berlin : Springer
STARTPAGE=179;ENDPAGE=197;TITLE=Lecture Notes in Computer Science ; 6041
Implementation and Application of Functional Languages ISBN: 9783642164774
IFL
Scholz, S.-B. (ed.), Implementation and Application of Functional Languages, pp. 179-197
Popis: We present a typical synergy between dynamic types (dynamics) and generalised algebraic datatypes (GADTs). The former provides a clean approach to integrating dynamic typing in a statically typed language. It allows values to be wrapped together with their type in a uniform package, deferring type unification until run time using a pattern match annotated with the desired type. The latter allows for the explicit specification of constructor types, as to enforce their structural validity. In contrast to ADTs, GADTs are heterogeneous structures since each constructor type is implicitly universally quantified. Unfortunately, pattern matching only enforces structural validity and does not provide instantiation information on polymorphic types. Consequently, functions that manipulate such values, such as a type-safe update function, are cumbersome due to boilerplate type representation administration. In this paper we focus on improving such functions by providing a new GADT annotation via a natural synergy with dynamics. We formally define the semantics of the annotation and touch on novel other applications of this technique such as type dispatching and enforcing type equality invariants on GADT values.
Databáze: OpenAIRE
Externí odkaz: