[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
traytel at in.tum.de
Fri Aug 19 10:32:30 CEST 2011
On 19.08.2011 01:38, Gerwin Klein wrote:
> Should we ask a wider audience (isabelle-users) if anybody else has
> good reasons against/for a change?
Another small advantage of set as an own datatype arises in the context
We use map functions to lift coercions between base types to coercions
between type constructors. E.g. "nat list" is subtype of "int list" with
the coercion "map int", provided that "int" is declared as a coercion
and "map" as map function for "'a list". This is a typical example of a
covariant map function (i.e. the lifting does not invert the direction
of the subtype relation).
On the other hand, the generic map function for "'a => 'b" ("% f g h x.
g (h (f x)) :: ('a => 'b) => ('c => 'd) => ('b => 'c) => ('a => 'd)") is
contravariant in the first argument. Concretely that means that "int =>
bool" is a subtype of "nat => bool", provided the above map function and
the coercion "int". In contrast, the corresponding map function for sets
as predicates ("image :: ('a => 'b) => ('a => bool) => ('b => bool)")
is, as one would expect, covariant in the first argument.
The current implementation of subtyping allows to declare only one map
function for a type constructor. Thus, we can have either the
contravariant or the covariant map for the function type, but not both
at the same time. The introduction of set as an own datatype would
resolve this issue.
More information about the isabelle-dev