Re: [Caml-list] Some Clarifications

[David MENTRE <david.mentre@gmail.com>]

Hello Robert,

[As a side note, you did not answered my question on which software
you consider of large scale. ]

Just two remarks on your post:

2005/7/19, Robert Morelli <morelli@cs.utah.edu>:
> One of the areas where I do much of my programming is in mathematical
> software.  I view this as one of the most difficult areas,  at the
> opposite extreme from simple domains like formal methods and language
> tools.  The problems with characterizing mathematical objects come
> up peripherally here with representations of numbers.  This always leads
> to endless,  inconclusive discussions of issues like operator
> overloading,  inheritance and multiple inheritance,  multiple dispatch,
> multiple views of a data structure,  constraints, etc., etc.

You should take a look at Axiom:
http://page.axiom-developer.org/zope/mathaction/FrontPage

This is an old Computer Algebra System, developed for 30 years at IBM
and now free software (BSD-like license). It has a complete typing of
mathematical expressions. The type system is very different from ML
systems however: no type inference. It is closer to a dynamic OO
language, but the types are not computer types but mathematical ones,
based on mathematical properties of objects (you know more about the
subject than me).

To come back to OCaml, Axiom interactive type system poses interesting
questions regarding type inference and interactive systems.
Mathematical notation is based on operator overloading: use the same
"+" as an operation on matrices or on integers, but the two "+" are
not the same operations, even if they have the same mathematical
properties. ML type systems are very bad when you need to manipulate
objects of different types (in OCaml, you would need +, +., +/, +b,
etc.). Maybe there is some interesting research to be done in that
area. Pierre Weis (of OCaml fame) discussed ones with Tim Daly (Axiom
lead developer) but did not catched the issue (at least this is how I
interpreted the discussion).


> The fundamental point is that OO puts interaction at the
> center of the paradigm,  not abstract characterization.  That has
> huge consequences and it's what makes the whole idea of a "theory"
> of large scale design meaningful.  OO commits to a certain way of
> organizing interaction,  state changes,  behavior changes, ....  that's
> attractive in practice (but requires deeper theory than FP).

I disagree on most of your arguments when comparing OO et FP (for the
same reasons as others have developed on the previous thread).
However, I agree on issues regarding  interactivity and ML typing, and
more generally on the rigid aspects of ML typing in *certain*
contexts.

As a programmer, ML typing is very rigid and this is a good point: I'm
sure that in all over my program, the datastructure is *never* misued
and that certain invariants are ensured. ML typing and moreover type
inference is a must have for library programmers.

However, as an interactive user (cf. my above comment on Axiom) or as
a system architect, I sometimes misses the flexibility of dynamic OO
system. Ok, they allow the system to be incoherent, but this is
sometimes *useful*, for example when you refactor a big system and you
want to test a subset of your modifications. The other point, as I
said, is the use of overloading. It is natural in dynamic OO systems,
it is very unpleasant in OCaml (although I haven't dug into GCaml, I
had a bad experience with OCaml objects).

I sometimes dream of a system that would allow me to have *both*
static typing and type inference like ML and dynamic typing like Lisp
or OO languages. The best of both worlds! :) In my opinion, the
interesting part is how to mix the two paradigms smoothly, e.g. how to
have meaningful error messages, how to define types for certain
objects but let the type inference system do the job for most of my
code, etc.

Yours,
d.

PS: formal methods or language tools are *not* simple domains! :-)