From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 645BBD561 for ; Wed, 27 Jul 2005 17:37:28 +0200 (CEST) Received: from rwcrmhc12.comcast.net (rwcrmhc13.comcast.net [204.127.198.39]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j6RFbQWE009201 for ; Wed, 27 Jul 2005 17:37:27 +0200 Received: from [192.168.1.4] (c-24-10-253-157.hsd1.ut.comcast.net[24.10.253.157]) by comcast.net (rwcrmhc13) with ESMTP id <2005072715372401500a34lbe>; Wed, 27 Jul 2005 15:37:25 +0000 Message-ID: <42E7AA34.9070801@cs.utah.edu> Date: Wed, 27 Jul 2005 09:37:24 -0600 From: Robert Morelli User-Agent: Mozilla Thunderbird 1.0 (X11/20041206) X-Accept-Language: en-us, en MIME-Version: 1.0 To: David MENTRE Cc: Kyle Consalus , caml-list@yquem.inria.fr Subject: Re: [Caml-list] Some Clarifications References: <9cc3782b05071411004b27b6a4@mail.gmail.com> <42DB6161.4030507@cs.utah.edu> <42DD5F41.8060801@cs.utah.edu> <3d13dcfc05072000347a6a4fba@mail.gmail.com> In-Reply-To: <3d13dcfc05072000347a6a4fba@mail.gmail.com> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 42E7AA36.002 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; morelli:01 morelli:01 caml-list:01 overloading:01 algebra:01 inference:01 aldor:01 compiler:01 aldor:01 ocaml's:01 statically:01 model:01 formalizing:01 subset:01 minor:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.8 required=5.0 tests=SPF_SOFTFAIL autolearn=disabled version=3.0.3 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 : > >>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.