Hi all,
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
of subtyping.
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.
Cheers,
Dmitriy
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
