Re: [Caml-list] Some Clarifications

[Robert Morelli <morelli@cs.utah.edu>]

David MENTRE wrote:
> 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).

I took a look at it at one time.  What particularly interested me was
the special language Aldor that was created for AXIOM's library
compiler.  Aldor has first class dependent types,  so its type system
is more expressive and consistent than OCaml's.  Because it's so
powerful,  it does indeed have some of the feel of a dynamic OO
language,  but it is not OO and it is statically typed,  using its
typing information for performance and safety.  (A paper coauthored by
Stephen Watts,  the principle designer of the language,  described an
encoding of the C++ object model in Aldor.)

There was some research formalizing a subset of Aldor's type system,
and proposing some minor changes to make it more theoretically
tractable.  There was even a project underway to implement something
using the Curry-Howard correspondence to encode significant assertions
in the type system of a modified Aldor.  (I haven't looked at
this for years,  so anyone interested should look this up to check
current status and details.  Simon Thompson was involved.)

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

It's a small world.  I lost my job at about the same time that AXIOM
was open sourced.  One of the things I considered was seeking funding
to do a research project.  One of the projects in computer science that
would most engage me intellectually,  would be to seek new programming
language paradigms to address the needs of mathematical software.
I briefly contacted Tim Daly during this period to explore whether I
could do something with AXIOM.   Unfortunately,  it was not to be:  no
credentials in computer science,  no proposalware,  not enough time to
cook up enough pseudo-goals and hype,  so I never submitted it.

At the time,  Tim Daly struck me as more of a software developer than
a programming language guy,  so he and Weis may have been talking
different languages,  so to speak.

I believe that mathematical software is one of the most fruitful avenues
for programming language research.  It seems to me that essentially
everything of lasting value in programming languages has come out of
attempting to implement mathematics.

My contention is simply that the program is incomplete;  there's
more to be discovered by implementing more of mathematics.  The
attitude that OCaml is some kind of pinnacle of language development,
already capable of dealing with all problems (and anyone who fails to
agree must simply be ignorant),  is quite depressing to me.  If it
were true,  I don't think good researchers would be developing it.

In fact,  if I may make a personal digression,  what got me interested
in computer science in the first place was doing these mathematical
calculations.  At some point,  I became almost transfixed with the
question of what would be needed to really do them properly.  I
began trying to design my own programming language.  What is amazing
to me in retrospect is that at the time,  I did not know what the terms
"functional programming language,"  "concurrency,"  or "programming
language semantics" meant,  nor did I know that there were researchers
who studied any such things seriously,  yet my design goals shared
a good deal with Haskell,  and my way of handling interaction involved
total concurrency,  like a process algebra.  I also tried to endow my
language with a category theoretic semantics (I believed at the
time this was an original idea).  It seems particularly strange that I
became fascinated with concurrency,  even though I was dealing with a
seemingly static world of mathematical objects,  and I had never done
any form of programming with threads or networking.  At the same time,
I placed the highest priority on stateless programming (which at the
time,  I thought was my own innovation).  I agonized for a long time
about how to reconcile these two diametric tendencies,  and finally came
up with a mechanism (not monads -- I never thought of that).

This experience has convinced me that studying mathematical computations
is very fruitful,  since I was lead to many correct ideas and instincts,
without any background in computer science,  or even much experience
programming.  At the same time,  I have encountered many programmers
with a great deal of experience who seem to have limited judgement
about programming languages.  The distinguishing factor seems to
be a certain kind of aesthetic and feeling for structure that I think
is best developed through mathematics.

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

To me,  this seems to have a pattern.  If the ML type system
can express the intrinsic structure of the objects you're dealing with,
it will constrain you in just the right way.  To the extent that it
can't,  it will get in your way and may necessitate convoluted
work-arounds.  The mental effort that goes into the former case is
valuable,  since it clarifies your problem itself which is an ideal
match to its expression in software.  The effort that goes into the
latter is wasted mental energy,  since it only creates artifice,  rather
than helping you understand your problem.

My assertion has been that the former case arises in the area of
formal methods,  for which the ML language was originally designed,
and in a few other similar niche areas which I have described as
"simple."  I see no shame in this,  but others here apparently believe
they must advocate that functional programming is an ideal fit for every
programming task.

> 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! :-)

A number of people have made this same point.  I think we must be
misunderstanding each other.  Let me just point out,  in case there
is a language barrier,  that the primary use of the word "simple"
in English has a positive connotation.  (The words "simplistic"
and "simple-minded" have negative connotations.)  Simple is good.
The best researchers,  scientists,  and artists,  are driven to
find the simplest possible expressions,  and instinctively reject
complicated ones.  The highest praise I can ever give someone,  is that
they have created something simple,  but expressive.