From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 ABD2ABC88 for ; Fri, 4 Feb 2005 22:52:50 +0100 (CET) Received: from mail.physik.uni-muenchen.de (mail.physik.uni-muenchen.de [192.54.42.129]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j14LqoWH021322 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Fri, 4 Feb 2005 22:52:50 +0100 Received: from localhost (unknown [127.0.0.1]) by mail.physik.uni-muenchen.de (Postfix) with ESMTP id E049E20031; Fri, 4 Feb 2005 22:52:49 +0100 (CET) Received: from mail.physik.uni-muenchen.de ([127.0.0.1]) by localhost (mail.physik.uni-muenchen.de [127.0.0.1]) (amavisd-new, port 10024) with LMTP id 26051-02-9; Fri, 4 Feb 2005 22:52:47 +0100 (CET) Received: from mailhost.cip.physik.uni-muenchen.de (kaiser.cip.physik.uni-muenchen.de [141.84.136.1]) by mail.physik.uni-muenchen.de (Postfix) with ESMTP id 5E06220026; Fri, 4 Feb 2005 22:52:47 +0100 (CET) Received: from eiger.cip.physik.uni-muenchen.de (eiger.cip.physik.uni-muenchen.de [141.84.136.54]) by mailhost.cip.physik.uni-muenchen.de (Postfix) with ESMTP id 4335126E87; Fri, 4 Feb 2005 22:52:47 +0100 (CET) Received: by eiger.cip.physik.uni-muenchen.de (Postfix, from userid 3092) id 3B90A3CBC; Fri, 4 Feb 2005 22:52:47 +0100 (CET) Received: from localhost (localhost [127.0.0.1]) by eiger.cip.physik.uni-muenchen.de (Postfix) with ESMTP id 38F892D716; Fri, 4 Feb 2005 22:52:47 +0100 (CET) Date: Fri, 4 Feb 2005 22:52:47 +0100 (CET) From: Thomas Fischbacher To: Jon Harrop Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] The boon of static type checking In-Reply-To: <200502041026.56107.jon@jdh30.plus.com> Message-ID: References: <891bd33905020213315a2ebb18@mail.gmail.com> <877e9a170502031856175260c8@mail.gmail.com> <877e9a17050203185674680413@mail.gmail.com> <200502041026.56107.jon@jdh30.plus.com> X-BOFH: Daemons did it MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Virus-Scanned: amavisd-new at physik.uni-muenchen.de X-Miltered: at nez-perce with ID 4203EEB2.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 wrote:01 checker:01 statically:01 polymorphism:01 ocaml:01 error-prone:01 ocaml:01 wrote:01 ocaml's:01 emulated:01 pairs:01 n-tuples:01 minor:01 misses:01 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: On Fri, 4 Feb 2005, Jon Harrop wrote: > > How did > > you feel that the static type checker of C++ didn't provide you with > > similar help? > > As the C++ type system cannot represent (and, therefore, statically check) > polymorphism properly, altering a generic data structure expressed using > templates results in reams of errors, mostly pointing to wrong places. I think the problem indeed is that in C++, the way how things that are easy in Ocaml have to be done via templates is both quite clumsy, error-prone, and furthermore a hell lot of unnecessary work. > Obviously such problems would have been virtually impossible to weed out had I > chosen to use a language with dynamic type checking, which is precisely I why > I left such languages at the door many years ago... At least for Lisp, its dynamic type checking does include a lot of static type analysis as well. Perhaps not as nice as that of ocaml, but certainly at the level one can also expect to get e.g. from C/C++. Just make use of (declare ...), compile functions and don't ignore warnings. As for static type analysis: the Lisp way is: if it turns out to be useful for a specific problem, it could always be added as a library. Sure it would be nice if there were consensus about one single library which provides this for those people who want to use it in lisp. > On Friday 04 February 2005 09:29, Thomas Fischbacher wrote: > > If I multiply a speed (in m/s) with a mass (in kg)... > > Yes, absolutely! I believe you have correctly identified dimensionality as a > very important and useful system of (phantom) types used in physics. It's occasionally useful. We physicists only use it when there really is danger of confusion, but adjust our units in such a way that no spurious conversion as to be performed if this only clutters formulae and gets in the way. In high energy physics, we define time, length, and charge units relative to the eV, setting hbar = c = e = 1. ("Natural units") Some even set pi=1, but that is an entirely different story... > The > OCaml type system goes some way to allowing such things to be enforced. > Dynamically typed languages do not. So how can you come to the conclusion > than going from dynamic typing to OCaml's static typing is a step in the > wrong direction? Dynamic typing is more flexible. My proposal is that in the best of all worlds, static typing should be completely optional, (Of course, if one doesn't use it, one will lose quite a lot of further possibilities. But as a programmer I'd rather like to have the choice, instead of being forced. That, by the way, is one of the nicer aspects of the perl philosophy.) > > So it's even more than "just returning more than one value without having > > to cons" (which already is quite nice - but this essentially can always be > > emulated via going to CPS, which establishes full call/return symmetry). > > It's about giviny gou extra choice. Either: "Nice that you can also > > provide me extra information, but I really don't care here", or: "I can > > as well make use of this other piece of information which you > > already obtained anyway." Same function, same call. > > Sure, but what's wrong with using fst and snd for pairs, and records instead > of n-tuples? You get the same functionality and an explicit definition of > what is happening with only a couple of extra key strokes. In most cases: I have to wrap up my thoughts in a situation where I know things could work much nicer. In some cases: it's really ugly to write an ocaml equivalent to LISP code that uses multiple-value to avoid consing. But, as I said, this is a minor issue, just about as annoying as the fact that in Scheme, one has to work with #t and #f instead of nil and non-nil, and that one is not guaranteed that (car nil) = (cdr nil) = nil, which also frequently turns out to be very convenient. > > > Use the top-level. > > > > That entirely misses the point! > > > > I talked about getting debug traces from an involved run. > > Which you can do from the top level. If you have to output the information > from a running, native-code compiled binary then write the print and > string_of functions yourself: > > let string_of_list f l = "["^String.concat "; " (List.map f l)^"]" > let string_of_pair f (a, b) = "("^f a^", "^f b^")" > print_endline (string_of_list (string_of_pair string_of_int) x) > > Considering the first two can be factored out of a wide variety of programs, > it really isn't a huge amount of typing... When I do algorithmically involved stuff, I frequently pretty soon reach the stage where I pass around structures of hash tables of structures and vectors of structures of vectors of numbers, say. I personally did experience it as painful to have to write specialized print functions for stuff like that. And this is an important issue, I think, as every language has its dark corners of things that would be useful and important, but people just don't do it as it is ugly and clumsy to express. If one such dark corner is getting information in one particular way about what's really going on deep down in the program, this is alarming. > > > As an obvious example, neither Common Lisp or Scheme have > > > pattern-matching. Accessing data via pattern matching is often far more > > > convenient than via c[ad]+r, slot accessors etc. > > > > Sure! But Lisp gives me the freedom to add it via a library. Which also > > kind of says that it's unnecessary to complicate the core language by > > putting in such a conceptually ad-hoc feature. > > That's obviously completely wrong and a blatant troll so I'll stop replying > now. You know nothing about the true way of the lambda. Absolutely *nothing*. ;;;; A simple example showing how to do - in principle - structural ;;;; matching in LISP in a way inspired by ML/Haskell ;;;; ;;;; Dear reader, please first look at the examples close to the end. ;;;; ;;;; (C) 2005 Dr. Thomas Fischbacher (defstruct (constructor (:print-function (lambda (obj stream depth) (declare (ignore depth)) (format stream "#<~A~S>" (string-downcase (symbol-name (constructor-type obj))) (coerce (constructor-args obj) 'list))))) type args) (defun joker-p (x) (and (symbolp x) (let ((n (symbol-name x))) (>= (length n) 1) (eql (schar n 0) #\?)))) (defvar _constructor-match-macros (make-hash-table :test 'eq)) (defun _instantiate-match (val lhs rhs failure &key (joker-p #'joker-p)) (if (funcall joker-p lhs) ;; Case I: Joker match `(let ((,lhs ,val)) ,rhs) (let ((cmm (if (consp lhs) (gethash (car lhs) _constructor-match-macros) nil))) (if cmm ;; Case II: Constructor match (funcall cmm val (cdr lhs) rhs failure :joker-p joker-p) ;; Case III: "otherwise" (if (eq lhs 't) rhs ;; Case IV: immediate match `(if (eql ,lhs ,val) ,rhs ,failure)))))) (defun _make-arg-bindings (sym-args nr-arg rest-params rhs failure &key (joker-p #'joker-p)) (if (null rest-params) rhs (_instantiate-match `(aref ,sym-args ,nr-arg) (car rest-params) (_make-arg-bindings sym-args (1+ nr-arg) (cdr rest-params) rhs failure :joker-p joker-p) failure :joker-p joker-p))) (defun make®ister-constructor-matcher (cname nr-params) (let ((cmm #'(lambda (val params rhs failure &key joker-p) (let ((len-params (length params)) (sym-fail (gensym "fail-")) (sym-args (gensym "args-"))) (if (or (not (listp params)) (/= len-params nr-params)) (error "Bad constructor match: ~A expects ~D args, got: ~S" cname nr-params params)) `(labels ((,sym-fail () ,failure)) (if (not (eq (constructor-type ,val) ',cname)) (,sym-fail) (let ((,sym-args (constructor-args ,val))) ,(_make-arg-bindings sym-args 0 params rhs `(,sym-fail) :joker-p joker-p)))))))) (setf (gethash cname _constructor-match-macros) cmm) (setf (symbol-function cname) #'(lambda (&rest args) (let ((v-args (coerce args '(simple-array * (*))))) (if (/= (length v-args) nr-params) (error "Constructor ~A is ~D-ary. Got args: ~S" cname nr-params args) (make-constructor :type cname :args (coerce args '(simple-array * (*))))))))) t) (defun _match (var list-cases &key sym-val (joker-p #'joker-p)) (if (null list-cases) nil (let* ((case-1 (car list-cases)) (lhs-1 (car case-1)) (rhs-1 `(progn ,@(cdr case-1))) (sym-val* (if sym-val sym-val (gensym "val-"))) (body (_instantiate-match sym-val* lhs-1 rhs-1 (_match var (cdr list-cases) :sym-val sym-val* :joker-p joker-p)))) (if sym-val body `(let ((,sym-val* ,var)) ,body))))) (defmacro match ((var &key (joker-p #'joker-p)) &rest list-cases) (_match var list-cases :joker-p joker-p :sym-val nil)) ;; ========== (make®ister-constructor-matcher 'fruit 1) (make®ister-constructor-matcher 'branch 2) (defun all-fruits (tree) (match (tree) ((fruit ?x) (list ?x)) ((branch ?x ?y) (append (all-fruits ?x) (all-fruits ?y))))) ;;; Believe it or not: we can also use this framework with built-in ;;; data types: (setf (gethash 'cons _constructor-match-macros) #'(lambda (val params rhs failure &key joker-p) (let ((len-params (length params)) (sym-fail (gensym "fail-")) (sym-args (gensym "args-"))) (if (/= 2 len-params) (error "CONS takes two matching args, got: ~S" params)) `(labels ((,sym-fail () ,failure)) (if (not (consp ,val)) (,sym-fail) (let ((,sym-args (coerce (list (car ,val) (cdr ,val)) '(simple-array * (*))))) ;; Clearly, if we were serious here, we would not do ;; such a stupid thing as making a vector from a cons cell ;; (so that we can use the above interface), ;; but use a more specialized variant, say, ;; _make-cons-arg-bindings... ,(_make-arg-bindings sym-args 0 params rhs `(,sym-fail) :joker-p joker-p))))))) ;;; === Example #1 === (defun all-fruits (tree) (match (tree) ((fruit ?x) (list ?x)) ((branch ?x ?y) (append (all-fruits ?x) (all-fruits ?y))))) (defun tree-is-double-branch (tree) (match (tree) ((branch (branch ?a1 ?a2) (branch ?b1 ?b2)) t) (t nil))) #| Log: * (branch (fruit 'big-apple) (branch (fruit 'small-apple) (fruit 'red-apple))) # # #)>)> * (all-fruits (branch (fruit 'big-apple) (branch (fruit 'small-apple) (fruit 'red-apple)))) (BIG-APPLE SMALL-APPLE RED-APPLE) * (tree-is-double-branch (fruit 123)) NIL * (tree-is-double-branch (branch (branch (fruit 'apple) (fruit 'pear)) (branch (fruit 'banana) (fruit 'potato)))) T |# ;;; === Example 2 === (defun my-reverse (list) (labels ((walk (done rest) (match (rest) (nil done) ((cons ?head ?tail) (walk (cons ?head done) ?tail))))) (walk nil list))) #| Log: * (my-reverse '(1 2 3 4 5)) (5 4 3 2 1) * (my-reverse '()) NIL |# ;; xx ;; don't meddle with the affairs of lisp wizards, for you are ;; crunchy, and good with ketchup! ;; xx -- regards, tf@cip.physik.uni-muenchen.de (o_ Thomas Fischbacher - http://www.cip.physik.uni-muenchen.de/~tf //\ (lambda (n) ((lambda (p q r) (p p q r)) (lambda (g x y) V_/_ (if (= x 0) y (g g (- x 1) (* x y)))) n 1)) (Debian GNU)