Expression conformance and anchored types 
Author Message
 Expression conformance and anchored types

I have a question about anchored types of the form

   feature
      add_item (other: like Current)

and the rules for expression conformance when attaching an actual
argument to "other".  For example, the Standard Kernel defines
"is_equal" in GENERAL with the signature

  is_equal (other: like Current): BOOLEAN

and the class STRING subsequently redefines is_equal with the same
signature.  We can call the feature is_equal on a target of type STRING
with (example from EiffelBase):

class FORMAT_INTEGER
   ...

   feature -- Access
      sign_string: STRING
    ...

   feature -- Modify
      set_sign (s : STRING) is
         do
             ...

         ensure
             sign_string.is_equal (s)
         end
    ...

end -- class FORMAT_INTEGER

Although this compiles on all Eiffel implementations, on my reading of
the Eiffel type rules this breaks VNCH -- expression conformance.  The
problem is that for sign_string.is_equal(s), s must be of type like
sign_string, not STRING.  OOSC2 states in section 16.7:

 In the case of anchoring a formal argument or result of a routine, as
 in

   r (other: like Current)

 the actual argument in a call, such as b in a.r (b), must be
 anchor-equivalent to the target a.

Furthermore, this is backed up with an example in the chapter on
typing in section 17.5.  For a class SKIER:

class SKIER feature

   roommate: like Current
   share (other: like  Current) is ... require ... do
         roommate := other
      end
   ...

end -- class SKIER

with descendents BOY and GIRL, the following will be
rejected as type-unsafe:

  s: SKIER; b: BOY; g: GIRL

  !! b;!! g;    -- Creation of a BOY and GIRL objects.
  s := b;     -- Polymorphic assignment.
  s.share (g)

since GIRL does not conform to type like s.

The definition of expression conformance in section 13.9 of ETL states
that

 An expression v of type VT conforms to an expression t of type TT if
 and only if they satisfy any one of the following four conditions.

 1. VT conforms to TT
 2. VT is like t (t in this case must be an entity)
 3. VT and TT are both of the form like x for the same x

(Supplanted by anchor equivalence in OOSC2?)

 4. TT is like x where x is a formal argument to a routine r, v is an
    actual argument in a call to r, and VT conforms to the type of the
    actual argument corresponding to x in the call.

This last is (as explained on page 225 of ETL) to allow calls of the
form

  x: CT; y: DT
  equal (x, y)

  (where CT conforms to DT)

but there is no such exception where x is a target of a call (ie,
Current in like Current) rather than one of the formal arguments.  This
leads to the odd situation of having

  sign_string, s: STRING
  ...

  check
     sign_string /= Void; s /= Void
  end

  equal (sign_string, s)  -- OK
  sign_string.is_equal(s) -- type violation

But in practice this isn't a problem.  It seems there is some implicit
rule operating in Eiffel implementations of the form (warning: I{*filter*}(I
am not a language lawyer!))

    [t of TT conforms to v of VT if]

 5. TT is like Current in a class X where t is a formal argument to a
    feature in class X, x is an entity attached to an object of class X
    (corresponding to Current in X) v is an actual argument in a
    feature call using the target x, and the type VT conforms to the
    type of the target x.

Can anyone clear this up for me?

--



Mon, 26 Mar 2001 03:00:00 GMT  
 Expression conformance and anchored types

Quote:

>But in practice this isn't a problem.  It seems there is some implicit
>rule operating in Eiffel implementations of the form (warning: I{*filter*}(I
>am not a language lawyer!))

>    [t of TT conforms to v of VT if]

Ooops.  I mean, of course, v of VT conforms to t of TT.

Quote:
> 5. TT is like Current in a class X where t is a formal argument to a
>    feature in class X, x is an entity attached to an object of class X
>    (corresponding to Current in X) v is an actual argument in a
>    feature call using the target x, and the type VT conforms to the
>    type of the target x.

>Can anyone clear this up for me?

Still confused though.

--



Mon, 26 Mar 2001 03:00:00 GMT  
 Expression conformance and anchored types
I have a question about anchored types of the form

   feature
      add_item (other: like Current)

and the rules for expression conformance when attaching an actual
argument to "other".  For example, the Standard Kernel defines
"is_equal" in GENERAL with the signature

  is_equal (other: like Current): BOOLEAN

and the class STRING subsequently redefines is_equal with the same
signature.  We can call the feature is_equal on a target of type STRING
with (example from EiffelBase):

class FORMAT_INTEGER
   ...

   feature -- Access
      sign_string: STRING
    ...

   feature -- Modify
      set_sign (s : STRING) is
         do
             ...

         ensure
             sign_string.is_equal (s)
         end
    ...

end -- class FORMAT_INTEGER

Although this compiles on all Eiffel implementations, on my reading of
the Eiffel type rules this breaks VNCH -- expression conformance.  The
problem is that for sign_string.is_equal(s), s must be of type like
sign_string, not STRING.  OOSC2 states in section 16.7:

 In the case of anchoring a formal argument or result of a routine, as
 in

   r (other: like Current)

 the actual argument in a call, such as b in a.r (b), must be
 anchor-equivalent to the target a.

Furthermore, this is backed up with an example in the chapter on
typing in section 17.5.  For a class SKIER:

class SKIER feature

   roommate: like Current
   share (other: like  Current) is ... require ... do
         roommate := other
      end
   ...

end -- class SKIER

with descendents BOY and GIRL, the following will be
rejected as type-unsafe:

  s: SKIER; b: BOY; g: GIRL

  !! b;!! g;    -- Creation of a BOY and GIRL objects.
  s := b;     -- Polymorphic assignment.
  s.share (g)

since GIRL does not conform to type like s.

The definition of expression conformance in section 13.9 of ETL states
that

 An expression v of type VT conforms to an expression t of type TT if
 and only if they satisfy any one of the following four conditions.

 1. VT conforms to TT
 2. VT is like t (t in this case must be an entity)
 3. VT and TT are both of the form like x for the same x

(Supplanted by anchor equivalence in OOSC2?)

 4. TT is like x where x is a formal argument to a routine r, v is an
    actual argument in a call to r, and VT conforms to the type of the
    actual argument corresponding to x in the call.

This last is (as explained on page 225 of ETL) to allow calls of the
form

  x: CT; y: DT
  equal (x, y)

  (where CT conforms to DT)

but there is no such exception where x is a target of a call (ie,
Current in like Current) rather than one of the formal arguments.  This
leads to the odd situation of having

  sign_string, s: STRING
  ...

  check
     sign_string /= Void; s /= Void
  end

  equal (sign_string, s)  -- OK
  sign_string.is_equal(s) -- type violation

But in practice this isn't a problem.  It seems there is some implicit
rule operating in Eiffel implementations of the form (warning: IANALL
(I am not a language lawyer!))

    [v of type VT conforms to t of type TT if]

 5. TT is like Current in a class X where t is a formal argument to a
    feature in class X, x is an entity attached to an object of class X
    (corresponding to Current in X) v is an actual argument in a
    feature call using the target x, and the type VT conforms to the
    type of the target x.

Can anyone clear this up for me?

--



Mon, 26 Mar 2001 03:00:00 GMT  
 
 [ 3 post ] 

 Relevant Pages 

1. Question on anchored type conformance

2. ETL: CNCX(2) Expression conformance

3. Intermediate type of mixed-type expressions

4. problem with generic types conformance

5. Conformance in generic types

6. Generic type and conformance.

7. expanded types conformance

8. Semantics of reattachment/equality for anchored types

9. Object Creation and Anchored Types

10. Creation with anchored type.

11. Anchored types and polymorphism

12. anchored types

 

 
Powered by phpBB® Forum Software