Preventing CAT calls in Generics

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 the object returned by item on line 3 is not of type STUDENT but of type PERSON.

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_integer_stack whose item feature guarantees, that the returned object will be of type STUDENT. This solution will now extend the type system 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]

The semantics are that where ever G occurs as a return type it will be instantiated as STUDENT. And wherever G occurs as an argument type it will be instantiated as EMLPOYED_STUDENT.

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

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

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 covariant and for result types to be contra-variant. This is actually a very important as it is the basis where the conformance is based uppon.

class T 
end
 
class U 
inherit T 
  -- no covariant feature redefinition
end

Type conformance

obsolete?

Generic conformance

-- 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 (T)

Type declaration:

an_agent: PROCEDURE [ANY..NONE, TUPLE..TUPLE [ANY..T]]  --> like agent (T)
  -- signature for call has to be inverted: TUPLE [T..NONE]..NONE
 
  -- 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

<todo>