[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[Dmitriy Traytel]

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