Re: [Caml-list] The boon of static type checking

[Thomas Fischbacher <Thomas.Fischbacher@Physik.Uni-Muenchen.DE>]

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&register-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&register-constructor-matcher 'fruit 1)
(make&register-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)))

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