Seilerm: enhanced Void/NONE example

2007-06-24T23:27:20Z

enhanced Void/NONE example

Juliant at 18:41, 24 June 2007

2007-06-24T18:41:28Z

Juliant: /* Default behavior */

2007-06-23T02:07:45Z

‎Default behavior

Juliant at 02:07, 23 June 2007

2007-06-23T02:07:04Z

Juliant at 01:54, 23 June 2007

2007-06-23T01:54:36Z

New page

[[Category:ECMA]]
[[Category:Catcall]]
== 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:

<e>
a_type: TYPE restrict TYPE_SET
</e>

An actual type set for <e>TYPE_SET</e> 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''.
<e>
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
</e>

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:
<e>
{ANIMAL} := {CAT} -- Does NOT conform. There is just an ANIMAL in the set!
</e>
<e>ANIMAL .. NONE</e> creates the set <e>{ANIMAL, CAT, DOG, ..., NONE}</e>

One can see now that the {CAT} is a subset of it and per definition the two sets conform:
<e>
{ANIMAL, CAT, DOG, ..., NONE} := {CAT}
</e>

=== Default behavior ===
An important decision to be made is what the default behavior is for:
<e>
a_type: TYPE
</e>
There are a couple of trade offs here. The possibilities are as follows:
* <e>TYPE .. TYPE -- monomorphic</e>
* <e>TYPE .. NONE -- polymorphic</e>
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.
<e>
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
</e>

=== 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 <e>la := lc</e> was moved to the invalid cases.

<e>
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

</e>
<e>
-- 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
</e>

== Issues ==
=== Void and NONE ===
Note that the fact that ''Void'' is of type <e>NONE</e> does not fit into the conformance rules.<br/>
If we check this code with the currently given rules it would be rejected:
<e>
a_t: T .. T
a_t := Void
</e>

<e>{NONE}</e> is no subset of <e>{T}</e>.

=== Lists ===
There are some interesting cases:
<e>
lla: LIST [LIST [ANIMAL]] restrict {LIST [LIST [ANIMAL]] .. LIST [LIST [CAT]]}
</e>
Now we apply the definition of the interval using the current conformance rules for types given by the ECMA standard.
<e>
T .. U -- Types conforming to T and to which U conforms
</e>
The following set is described by the interval above:
<e>
{LIST [LIST [ANIMAL]], LIST [LIST [CAT]]}
</e>
So we are allowed to assign a <e>LIST [LIST [CAT]]</e> to `l'.<br/>
Now the result type of item is <e>LIST [ANIMAL]</e>:
<e>
lla.item (1) -- LIST [ANIMAL]
</e>
But then one could produce a CAT call like this:
<e>
lla.item (1).put (create {DOG})
</e>
Here the whole code:
<e>
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
</e>
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.

@@ Line 123: / Line 123: @@
 == Issues ==
 === Void and NONE ===
-Note that the fact that ''Void'' is of type <e>NONE</e> does not fit into the conformance rules.<br/>
+Note that the fact that ''Void'' is of type <e>NONE</e> prohibits some assignments.<br/>
 If we check this code with the currently given rules it would be rejected:
 <e>
-a_t: T .. T
+a_t: T restrict T
 a_t := Void
 </e>
 <e>{NONE}</e> is no subset of <e>{T}</e>.
 === Lists ===

@@ Line 1: / Line 1: @@
 [[Category:ECMA]]
 [[Category:Catcall]]
 == 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.

@@ Line 63: / Line 63: @@
 * <e>TYPE .. TYPE -- monomorphic</e>
 * <e>TYPE .. NONE -- polymorphic</e>
-The choice made [Restrict types mail|here] is the second one: polymorphic
+The choice made [[Restrict types mail|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?

Restrict types - Revision history

Seilerm: enhanced Void/NONE example

Juliant at 18:41, 24 June 2007

Juliant: /* Default behavior */

Juliant at 02:07, 23 June 2007

Juliant at 01:54, 23 June 2007