Inproceedings,
Type class polymorphism in an institutional framework
Recent Trends in Algebraic Development Techniques, 17th International Workshop (WADT 2004), volume 3423 of Lecture Notes in Computer Science, page 234-248. Springer; Berlin; http://www.springer.de, (2005)
Abstract
Higher-order logic with ML-style type class
polymorphism is widely used as a specification formalism. Its
polymorphic entities (types, operators, axioms) can easily be equipped
with a `naive' semantics defined in terms of collections of
instances. However, this semantics has the unpleasant property that
while model reduction preserves satisfaction of sentences, model
expansion generally does not. In other words, unless further measures
are taken, type class polymorphism fails to constitute a proper
institution, being only a so-called rps preinstitution; this is
unfortunate, as it means that one cannot use institution-independent or
heterogeneous structuring languages, proof calculi, and tools with it.
Here, we suggest to remedy this problem by modifying the notion of model
to include information also about its potential future extensions. Our
construction works at a high level of generality in the sense that it
provides, for any preinstitution, an institution in which the original
preinstitution can be represented. The semantics of polymorphism used in
the specification language HasCASL makes use of this result. In fact,
HasCASL's polymorphism is a special case of a general notion of
polymorphism in institutions introduced here, and our construction
leads to the right notion of semantic consequence when applied to this
generic polymorphism. The appropriateness of the
construction for other frameworks that share the same problem depends on
methodological questions to be decided case by case. In particular, it
turns out that our method is apparently unsuitable for observational
logics, while it works well with abstract state machine formalisms such as
state-based CASL.
