Issue with min_type and max_type
The description of the functions Type.Subst.min_type and Type.Subst.max_type in the doc is wrong: the largest subtype of any instance of t is NOT t where all positive occurrences of variables are replaced by 𝟘 and all negative occurrences of variables not in vars are replaced by 𝟙.
Counterexample:
t = (Any->Any) & 'a | (Int->Int) & ~'a
min(t) should be (Any->Any)&(Int->Int)
, but replacing the occurences of 'a as specified would give Empty,
which is a subtype of any instance of t but not the largest.
Moreover, the result of this computation is not preserved by semantic equivalence, as for any 'a
we have (Int->Int) = (Int->Int) & 'a | (Int->Int) & ~'a
but min(Int->Int) = Int->Int
and min((Int->Int) & 'a | (Int->Int) & ~'a) = Empty
. Also, I am not sure Cduce would always simplify the type (Int->Int) & 'a | (Int->Int) & ~'a
into (Int->Int)
as it does not simplify the DNF of functions.
The cases where the functions min_type and max_type are not correct is when a variable appears in both a negative and positive occurence, because then the operation of substituting one of the occurence by something and the other by something else is not preserved by semantic equivalence.
I understand that one of the usecase of this function is to implement the min and max for dynamic types, but as dynamic type variables should always be unique (a given dynamic type variable should not appear twice in a type), the function clean_type should be enough to implement it (as a given dynamic type variable can only be positive or negative but not both). If a dynamic type variable "semantically" appears in both covariant and contravariant positions, it is invalid and thus the fact that clean_type will do nothing is not an issue (assuming that Cduce will simplify trivial partitions of the form t & 'a | t & ~'a
in order to only keep occurences of variables that have a semantic impact, which I don't think is always true when t is a function for instance).
My suggestion is to remove the min_type and max_type functions as the cases where it is correct (when no variable is both in covariant and contravariant position) can easily be handled with clean_type.