Difference between revisions of "Preventing CAT calls in Generics"

m (Semantics)
Line 39: Line 39:
 
Currently no static check will prohibit you from writing things like this. At runtime on ''line 2'' the first CAT call occurs, which most likely wont do any harm to a list. But the object returned by <e>item</e> on ''line 3'' is not of type <e>STUDENT</e> but of type <e>PERSON</e> and at least now we have a serious problem if one invokes features specific to a student on <e>l_student</e>.
 
Currently no static check will prohibit you from writing things like this. At runtime on ''line 2'' the first CAT call occurs, which most likely wont do any harm to a list. But the object returned by <e>item</e> on ''line 3'' is not of type <e>STUDENT</e> but of type <e>PERSON</e> and at least now we have a serious problem if one invokes features specific to a student on <e>l_student</e>.
  
The issue is that the <e>put</e> feature of <e>l_person_stack</e> allows you to put objects of type <e>PERSON</e> on the stack even though the actual type of the attached object is <e>STACK [STUDENT]</e> and is referenced by <e>l_integer_stack</e> whose item feature guarantees, that the returned object will be of type <e>STUDENT</e>.
+
The issue is that the <e>put</e> feature of <e>l_person_stack</e> allows you to put objects of type <e>PERSON</e> on the stack even though the actual type of the attached object is <e>STACK [STUDENT]</e> and is referenced by <e>l_student_stack</e> whose <e>item</e> feature guarantees, that the returned object will be of type <e>STUDENT</e>.
 
This solution will now extend the type system and the generic derivation of Eiffel in such away, that the type of a formal occurring as an argument in a feature declaration and the type of a formal occurring as a result type can be set independently. The type system will be extended with rules which allow only assignments between generic types if it cannot possibly lead to problems like the one mentioned above.
 
This solution will now extend the type system and the generic derivation of Eiffel in such away, that the type of a formal occurring as an argument in a feature declaration and the type of a formal occurring as a result type can be set independently. The type system will be extended with rules which allow only assignments between generic types if it cannot possibly lead to problems like the one mentioned above.
  
Line 98: Line 98:
  
 
{{Note| Why do we need that?
 
{{Note| Why do we need that?
We want to ensure that one has a read only list as if we would do <e>LIST [ANY..NONE]</e> one would not be allowed to assign a <e>LIST [INTEGER]</e> to it as one can put Void into a list of type <e>LIST [ANY..NONE]</e> which is invalid for a list of integer as <e>INTEGER</e> is expanded.}}
+
We want to ensure that one has a read only list. One cannot use a <e>LIST [ANY..NONE]</e> because one would not be allowed to assign a <e>LIST [INTEGER]</e> to it. This is because one can put Void into a list of type <e>LIST [ANY..NONE]</e>, which is invalid for a list of integer as <e>INTEGER</e> is expanded.}}
  
 
== Validity ==
 
== Validity ==

Revision as of 13:11, 8 April 2007

Warning.png Warning: Warning: Article under development

Introduction

The problem with the way generics are implemented in Eiffel right now is that CAT calls can occur.

class PERSON
end
 
class STUDENT
inherit
 PERSON
end
 
class EMPLOYEE
inherit
 PERSON
end
 
class EMPLOYED_STUDENT
inherit
 EMPLOYEE
 STUDENT
end
local
  l_person: PERSON
  l_student: STUDENT
  l_any_stack: STACK [PERSON]
  l_integer_stack: STACK [STUDENT]
do
  l_person_stack := l_student_stack -- line 1
  l_person_stack.put (l_person) -- line 2
  l_student := l_student_stack.item -- line 3

Currently no static check will prohibit you from writing things like this. At runtime on line 2 the first CAT call occurs, which most likely wont do any harm to a list. But the object returned by item on line 3 is not of type STUDENT but of type PERSON and at least now we have a serious problem if one invokes features specific to a student on l_student.

The issue is that the put feature of l_person_stack allows you to put objects of type PERSON on the stack even though the actual type of the attached object is STACK [STUDENT] and is referenced by l_student_stack whose item feature guarantees, that the returned object will be of type STUDENT. This solution will now extend the type system and the generic derivation of Eiffel in such away, that the type of a formal occurring as an argument in a feature declaration and the type of a formal occurring as a result type can be set independently. The type system will be extended with rules which allow only assignments between generic types if it cannot possibly lead to problems like the one mentioned above.

Syntax

LIST [G] can be declared in the following way:

l_list: LIST [PERSON..EXMLPOYED_STUDENT]

LIST[A] is a shorthand for LIST[A..A]. LIST[A..] is also a possible syntax.

Another syntax could look as follows:

<type_for_arguments>:<type_for_return_types>

This would more resemble an actual generated signature of a feature which looks initially like

class EXAMPLE [G]
feature
  example (a_g: G): G
end

A type declaration with this syntax would look like:

local
 l_example: EXAMPLE [EMLPOYED_STYDENT: STUDENT]
 l_employed_student: EMPLOYED_STUDENT
 l_person: PERSON
do
 -- l_example.example (a_g: EMPLOYED_STUDENT): STUDENT 
  l_person := l_example.example (l_employed_student) -- valid
end

LIST[:A] is the equivalent to LIST[A..]. LIST[A] is a shorthand for LIST[A: A].

But let's stick with the initial syntax for now.

Semantics

As we already pointed out, this solution is an extension to the type system. It helps you to proper derive an interface of a generic type. For example an actual type parameter for G in LIST [G] is PERSON..EMPLOYED_STUDENT. The interface generated by this derivation is simply that the first type (PERSON) is taken wherever G occurs as a return type. The second type (EMPLOYED_STUDENT) is taken wherever G occurs as an argument type.

(generic derived) class LIST[PERSON..EMPLOYED_STUDENT]
 
  put (v: EMPLOYED_STUDENT)
 
  item: PERSON

If we encounter a form like LIST [A..] it simply means that no feature which has the formal in the argument can be called.

Information.png Note: Why do we need that? We want to ensure that one has a read only list. One cannot use a LIST [ANY..NONE] because one would not be allowed to assign a LIST [INTEGER] to it. This is because one can put Void into a list of type LIST [ANY..NONE], which is invalid for a list of integer as INTEGER is expanded.

Validity

LIST[<first_type>..<second_type>]

Such a generic derivation is valid if:

  • 1: the second type conforms to the constraint of the formal.
  • 2: the second type conforms to the first type

Conformance Rules

We make another more abstract example to illustrate the conformance rules. They can easily be derived by applying the fact that its save for argument types to be contra-variant and for result types to be covariant. This is actually a very important as it is the basis where the conformance is based uppon.

Interface conformance rule:

An interface B is conform to an interface A if for every feature f_a in A 
there is a corresponding feature f_b available from B and for each feature 
the arguments of f_a conform to those of f_b and the result type of f_b is 
conform to the one of f_a.
local
  l_a: A
  l_b: B
do
    -- is legal if the interface conformance rule holds
  l_a := l_b
end


Example of an actual generic conformance table

class T 
end
 
class U 
inherit T 
  -- no covariant feature redefinition
end
conforms to LIST [ANY] LIST [T] LIST [T..NONE] LIST [ANY..T] LIST [U]
LIST [ANY] true false false true false
LIST [T] false true true true false
LIST [T..NONE] false false true false false
LIST [ANY..T] false false false true false
LIST [U] false false true false true
-- legal
T := LIST [T..NONE] .item
LIST [T..NONE] .put (Void)
 
  -- illegal
U := LIST [T..NONE] .item
LIST [T..NONE] .put (T)
 
  -- legal
LIST [ANY..T] .put (T)
LIST [ANY..T] .put (U)
ANY := LIST [ANY..T] .item
 
  -- illegal
LIST [ANY..T] .put (ANY)
T := LIST [ANY..T] .item

Agents

The neat thing about this extension is, that there is no need to cut down the expressiveness of the agent mechanism to make them perfectly save to use with full support for all legal situations.

Procedure class:

class PROCEDURE [BASE_TYPE, OPEN_ARGS -> TUPLE []]
    -- Signature of call is generated by the compiler. To visualize this we add _reflected to the argument tuple.
  call (args: OPEN_ARGS_reflected)
    do end
 
end

Agent example

Type declaration:

an_agent: PROCEDURE [ANY..NONE, TUPLE..TUPLE [ANY..T]]  --> like agent (T)
  -- This signature promises that the caller is going to give at least one argument which conforms to T.
  -- Note: The signature for the call routine has to be reflected by the compiler into : TUPLE [T..]..NONE
  --       This is because we can give a tuple containing more than one element and it element type has to conform to T.
 
 
  -- legal
an_agent.call ([T])
an_agent.call ([T, ...])
an_agent.call ([U, ...])
 
  -- illegal
an_agent.call ([])

Instantiation:

agent_empty := agent () do end --> PROCEDURE [ANY, TUPLE []]
agent_any := agent (a: ANY) do end --> PROCEDURE [ANY, TUPLE [ANY]]
agent_t := agent (t: T) do end --> PROCEDURE [ANY, TUPLE [T]]
agent_u := agent (u: U) do end --> PROCEDURE [ANY, TUPLE [U]]
 
  -- legal
an_agent := agent_empty
an_agent := agent_any
an_agent := agent_t
 
  -- illegal
an_agent := agent_u

There might be a concern about the fact that the compiler generates the signature of the call method. But I think that its not wrong to have compiler support for agents, as they are such a fundamental core concept that is simply important that one could sacrifice expressive power or type safety just to avoid explicit support from the compiler.

How to generate the call signature for a given agent type

To build the signature of the call routine one simply takes he second parameter and move it as the first. As the second parameter we put NONE.

Example:

TUPLE [ANY..T, ANY..U, ANY..V]

leads to

TUPLE [T..,U..,V..]

This basically states that all I want is to be able to read an object of at least type T, U, V and that I'm not going to put anything into this tuple.