Re: Operation can be dispatching in only one type

[stefan-lucks@see-the.signature]

On Mon, 7 Dec 2009, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 

> > Why not to allow such constraints for subtypes? E.g.
> >
> >   subtype Valid_Window_Type is Window_Type when Is_Valid;
> >
> > then simply:
> >
> >   procedure Do_Something (Window : Valid_Window_Type; ...)
> 
> That's also under consideration, 

Great! 

Isn't that essentially the same as the invariants in Eiffel?

> but there are some problems with it. One 
> problem is that such types are very confusing in array indexes/slices (do 
> the values all participate or just the ones that pass the predicate?) 

One way to solve^H^H^H^H^H^H circumvent this problem would be to prohibit 
that kind of subtyping for discrete types. In Dmity's example above, 
Window_Type is likely to be a record (probably a tagged one). If it is not 
a discrete type, you can't use it as an array index. :-)

In any case, you definitively would not want to allow that kind of type 
for array indexes, if only the values which the predicate being true is 
allowed. How would you efficiently implement something like

   subtype Primes is Positive when Is_Prime;
   A: array (Primes (10_000 .. 20_000)) of T; -- 10_001 primality tests
   B: array (Primes (Start  ..   Stop)) of T; -- Start-Stop+1 such tests
                                              -- possibly at runtime

> Another issue is that not all preconditions/postconditions can be written 
> this way. For one thing, a precondition can depend on multiple parameters at 
> once. Another issues is that the entry condition and exit conditions may be 
> different for a parameter. 

Right. That is precisely why Eiffel distinguishes preconditions, 
postconditions and invariants -- and supports all the three.


-- 
------ Stefan Lucks   --  Bauhaus-University Weimar  --   Germany  ------
               Stefan dot Lucks at uni minus weimar dot de
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------