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 nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id D2F73BB88 for ; Wed, 20 Jul 2005 09:34:45 +0200 (CEST) Received: from nproxy.gmail.com (nproxy.gmail.com [64.233.182.194]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j6K7YjEd022719 for ; Wed, 20 Jul 2005 09:34:45 +0200 Received: by nproxy.gmail.com with SMTP id x37so362542nfc for ; Wed, 20 Jul 2005 00:34:44 -0700 (PDT) DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:reply-to:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=WtBDG6ArD7+us6BXiLpaYwZY0wnihcLuJJJZbtzpMtczniJuwVHZv06tE/DWtO1stQAZEXQnV/D2kDE1mgwwDn2Ur6/5aTPuleVbuCcOFe212Zg2DJ4Yl7TUKh9JZG0IyrkSpgogsmvx0mNSiaCWQ0lVoi2QP6r44unyigBMHqQ= Received: by 10.48.3.10 with SMTP id 10mr255578nfc; Wed, 20 Jul 2005 00:34:44 -0700 (PDT) Received: by 10.48.237.20 with HTTP; Wed, 20 Jul 2005 00:34:44 -0700 (PDT) Message-ID: <3d13dcfc05072000347a6a4fba@mail.gmail.com> Date: Wed, 20 Jul 2005 09:34:44 +0200 From: David MENTRE Reply-To: To: Robert Morelli Subject: Re: [Caml-list] Some Clarifications Cc: Kyle Consalus , caml-list@yquem.inria.fr In-Reply-To: <42DD5F41.8060801@cs.utah.edu> Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Content-Disposition: inline References: <9cc3782b05071411004b27b6a4@mail.gmail.com> <42DB6161.4030507@cs.utah.edu> <42DD5F41.8060801@cs.utah.edu> X-Miltered: at nez-perce with ID 42DDFE95.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 morelli:01 morelli:01 overloading:01 algebra:01 inference:01 ocaml:01 poses:01 inference:01 notation:01 overloading:01 matrices:01 integers:01 ocaml:01 weis:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.4 required=5.0 tests=RCVD_BY_IP,REPLY_TO_EMPTY autolearn=disabled version=3.0.3 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). 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! :-)