Difference between revisions of "Restrict types"

Revision as of 09:41, 24 June 2007

Research: This page describes research about Eiffel, not the actual language specification.

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:

• TYPE .. TYPE -- monomorphic
• TYPE .. NONE -- polymorphic

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 does not fit into the conformance rules.
If we check this code with the currently given rules it would be rejected:

a_t: T .. T
a_t := Void

{NONE} is no 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.