Re: [Caml-list] Re: OCAML Downcasting?

["Marcin 'Qrczak' Kowalczyk" <qrczak@knm.org.pl>]

skaller <skaller@users.sourceforge.net> writes:

>> Attempts to avoid downcasts are often unmodular, they require to
>> specify all possible variants in one place.
>
> It makes no difference. You have do specify them all anyhow,
> downcast or not.

It makes a difference because specifying them at the type definition
would introduce a dependency loop between modules. And it would be
unmodular: it would require changing some base module whenever a far
client module is added.

Apply this reasoning to the exn type. Why don't you define all exn
constructors in one place?

> The unstated assumption is that you want early error detection
> and efficiency which static typing promises.

It's impossible in general. Only some errors are detectable statically
in practice.

> In the static typing world, 'safe' means errors are always
> detected at compile time.

No practical language is safe according to this definition, so this
definition is useless.

> Generally, we'd like to make programs safer where possible.

This is the catch: "where possible". I would add: "where practical";
sometimes the cost outweights the benefits. For example static
detection of possible division by 0 would be impractical. You would
have to either embed a proof checker in the language in order to be
able to convince the compiler that the number can't be 0, or not use
exceptions at all and have all partial functions return a result in
"option" type or similar, with manual propagation of errors.

And guess what? No language I know checks division by 0 statically
(except proof checkers, but they are not suitable for writing big
programs - too much work). Because it would make programs less robust,
not more. Because you would not use exceptions, and manual propagation
of errors is more error-prone than using exceptions, and it causes
more problems when the set of possible exceptions raised in a given
part of code is changed.

> The problem with downcasting as a general technique is that it
> bypasses static safety where it is in fact desired and is available.

It's not available because it can't express what downcasts provide:
the ability to add "constructors" to a type in a modular way.

According to your beliefs, you should advocate removing exceptions
from OCaml. Because they make the type independent from the set of
ways in which a program can fail, and thus remove the ability to
statically check whether all possible errors are caught. You should
always use explicit algebraic types to encode the outcome, no?

-- 
   __("<         Marcin Kowalczyk
   \__/       qrczak@knm.org.pl
    ^^     http://qrnik.knm.org.pl/~qrczak/

-------------------
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