Restrict types
Research: This page describes research about Eiffel, not the actual language specification.
Contents
Introduction
This solution uses enhancements to the type system to ensure CAT call freeness. It tackles the problem on the type basis for each entity declaration (which includes variables and generic parameters). The programmer declares a set of types and depending on the type declaration of a target of a qualified call all problematic features regarding CAT are disabled.
A call on a target is only valid if it cannot become possibly invalid at run-time due to polymorphism and covariantly redefined features or changed export status. This is achieved as the compiler checks that for all types which could be attached to a variable that all calls are valid. To help the compiler the programmer restricts the set of possible types.
Syntax and semantic
There were various proposals for syntax. They all express sets of types. Some include set operations and simplified construction by using construct to describe intervals. In the end it all comes down to the fact that the notion of a type in Eiffel is enhanced to a set of types.
The last proposal on the ECMA mailinglist is introduced here in a simplified, less formal manner:
a_type: TYPE restrict TYPE_SET
An actual type set for TYPE_SET can be constructed in many different ways. This proposal includes syntactic sugar to create sets out of given intervals and includes the set operations union, intersection and subtraction.
ANY .. NONE -- Fits all types ANY > -- Means the same > NONE -- Means the same T > -- T and conforming types > T -- Types to which T conforms to T .. U -- Types conforming to T and to which U conforms X .. Y -- Types conforming to X and to which Y conforms {T .. U} + {X .. Y} -- Types that satisfy any of the preceding two conditions {T .. U} - {X .. Y} -- Types that satisfy the first of those but not the second {T .. U} * {X .. Y} -- Types that satisfy both
Once the compiler has a set of types it computes all features which are CAT free. This relies on the fact that all types are known at compile time.
A call on a target is only valid if it cannot become possibly invalid at run-time due to polymorphism and covariantly redefined features or changed export status.
This is achieved as the compiler checks that for all types which could be attached to a variable that all calls are valid.
To help the compiler the programmer restricts the set of possible types.
Conformance rules
The conformance rule for the new introduced entity type-set is given by the subset relation:
T restrict S conforms to T restrict S' only if S is a subset of S'
A few examples for some type sets help one to get started:
{ANIMAL} := {CAT} -- Does NOT conform. There is just an ANIMAL in the set!
ANIMAL .. NONE creates the set {ANIMAL, CAT, DOG, ..., NONE}
One can see now that the {CAT} is a subset of it and per definition the two sets conform:
{ANIMAL, CAT, DOG, ..., NONE} := {CAT}
Default behavior
An important decision to be made is what the default behavior is for:
a_type: TYPE
There are a couple of trade offs here. The possibilities are as follows:
The choice made here is the second one: polymorphic The article does not explain how exactly generic types are handled. Are generic parameters monomorphic? What are the conformance rules for generics?
Examples
See the introduction to examples for information about the classes used.
Cats and dogs
Here is a list of valid and invalid assignments. A valid assignment in this context means that the right type conforms to the left type of the assignment.
local zoo_member: ANIMAL -- Polymorph is default: The type set contains any descendant of ANIMAL. animal: ANIMAL restrict ANIMAL cat: CAT restrict CAT dog: DOG restrict DOG animal_not_hungry: ANIMAL restrict ANIMAL .. NONE -- One cannot call `eat' as it is covariantly redefined in CAT animal_only_eating_cat_food: ANIMAL restrict ANIMAL .. CAT -- They can eat, but only cat food. food: FOOD restrict FOOD -- Food cat_food: CAT_FOOD restrict CAT_FOOD -- Cat food do animal := zoo_member -- Invalid! Default for ANIMAL is ANIMAL .. NONE, this is not a subset of {ANIMAL} animal := cat -- Invalid! {CAT} is not a subset of {ANIMAL} animal := dog -- Invalid! Rejected out of the same reason as the cat, -- but to assign the dog would be save. animal_not_hungry := cat -- Valid animal_not_hungry := dog -- Valid animal_only_eating_cat_food := cat -- Valid animal_only_eating_cat_food := dog -- Invalid, but would be save for this example. end
Generics
This mechanism partly describes the handling of generic types. The only major difference between the version presented here and the one in the wiki is that la := lc was moved to the invalid cases.
lc: LIST [CAT]; lo: LIST [OCTOPUS] la: LIST [ANIMAL] lac: LIST [ANIMAL restrict {CAT}] laa: LIST [ANIMAL restrict] -- Monomorphic list -- All OK. lac := lc ; la := lo -- INVALD: la := lc ; laa := la ; laa := lac ; laa := lc ; laa := lo ; lac := lo
-- OK lac.item.eat (cf) -- INVALID: lac.item.eat (f) -- INVALID: la.item.eat (f) -- INVALID: la.item.eat (cf) -- Becomes valid if OCTOPUS is removed from system
Issues
Void and NONE
Note that the fact that Void is of type NONE prohibits some assignments.
If we check this code with the currently given rules it would be rejected:
a_t: T restrict T a_t := Void
{NONE} is no subset of {T}.
So if the programmer wants to do this he has to declare `a_t' differently:
a_t: T restrict {T, NONE} a_t := Void
Now {NONE}is a subset of {T}.
Lists
There are some interesting cases:
lla: LIST [LIST [ANIMAL]] restrict {LIST [LIST [ANIMAL]] .. LIST [LIST [CAT]]}
Now we apply the definition of the interval using the current conformance rules for types given by the ECMA standard.
T .. U -- Types conforming to T and to which U conforms
The following set is described by the interval above:
{LIST [LIST [ANIMAL]], LIST [LIST [CAT]]}
So we are allowed to assign a LIST [LIST [CAT]] to `l'.
Now the result type of item is LIST [ANIMAL]:
lla.item (1) -- LIST [ANIMAL]
But then one could produce a CAT call like this:
lla.item (1).put (create {DOG})
Here the whole code:
local lla: LIST [LIST [ANIMAL]] restrict {LIST [LIST [ANIMAL]] .. LIST [LIST [CAT]]} llc: LIST [LIST [CAT]] la: LIST [ANIMAL] do create llc... lla := llc -- Type of `llc' is in type set of `lla' la := lla.item (1) -- Dynamic type of la is LIST [CAT] la.put (create {DOG}) -- Now there is an instance of DOG in LIST [CAT] end
This is indeed bad because cats can have features which dogs do not have, calling them would lead to system failure. We might try to fix this by changing the conformance for generics and the rule how intervals are generated.
Conclusion
The solution in its current state solves CAT calls only for ordinary types. But it might be possible to enhance it to solve generic types as well.
