Were nested quantifiers (either existentials or universals) considered in
the context of OCaml?  If not, are there plans to add them?  Thanks.

Walid.

On Wed, 6 Nov 2002, Xavier Leroy wrote:

|> I am sometimes lacking the dynamic cast (with a runtime test) in
|> Ocaml. Assuming that I have the usual point and colored_point classes
|> (as in the 3.06 Manual), I want to deal with point array-s and test if
|> the 3rd point is in fact a colored point.
|> Is there some type-theoritical issues here?
|
|There was a long thread on this topic on this list not long ago.
|Several approaches were discussed: using datatypes (Point of point |
|CPoint of cpoint), extensible datatypes (via the type "exn" of
|exceptions), etc.  See also Coca-ML:
|http://www.pps.jussieu.fr/~emmanuel/Public/Dev/coca-ml/index-en.html
|
|This said, my opinion on downcasts is that they are a low-level,
|dangerous feature that is best replaced by advanced, statically-typed
|constructs like OCaml provides.  (Some day, I'll have a bumper sticker
|custom-made that reads "Caml programmers do it statically".)
|
|In my (admittedly limited) experience with Java, 95% of downcasts in
|Java code fall in one of the following scenarios:
|- when using container classes (program puts a Foo in a Hashtable,
|  reads it back as Object, needs downcast to Foo);
|- when using binary methods (equal(), compare())
|- to encode sum types (a Foo is a Bar or a Gee).
|
|The OCaml type system is able to type-check all three scenarios
|statically, using parameterized classes, "mytype" specialization,
|and datatypes / variants (respectively).
|
|The remaining 5% of downcasts were kludges where the programmer
|managed to ruin a perfectly good class hierarchy by sprinkling type
|tests everywhere, rather than subclassing and redefining virtual
|methods adequately in classic OO fashion.
|
|To be fair, I may have missed some legitimate uses of downcasts in
|complicated situations.  But I believe these legitimate uses are
|uncommon enough that it is best to find another way to express the
|desired behavior, rather than extend OCaml with downcasts.
|
|That you can do self-modifying code in assembler, Duff's device in C,
|or downcasts in Java doesn't mean that you want to do it in OCaml as
|well :-)
|
|- Xavier Leroy
|-------------------
|To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
|Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
|Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
|

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners