Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
To: info-hol@leopard.cs.byu.edu
Subject: Re: HOL90 - Syntax
In-Reply-To: Your message of "Tue, 15 Mar 94 15:24:21 +0100." <94Mar15.152423met.8111@sunbroy14.informatik.tu-muenchen.de>
Date: Tue, 15 Mar 94 15:22:21 +0000
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:131070:940315152234"@cl.cam.ac.uk>


As far as the specific example quoted is concerned, the type constructors are
in any case completely unnecessary, unless you are worried about "compilation"
time. The following version uses quotation and is in my opinion more readable
as well as faster. (Cf. the replies to Phil's "partial evaluation" message of
last month.) I am assuming of course that this code is to be compiled after the
basic types have been set up.

  let mk_arith_op =
    let num_ty = ":num" and fun_ty = ":num->num->num" in
    \tok ftok (t1,t2).
       (list_mk_comb (mk_const(tok,fun_ty),[t1;t2]) ? failwith ftok);;

On the general point, I think all the pros and cons that Konrad and I have
discussed privately have now been aired here, and it might be worth
summarizing. Records:

  * Provide documentation for code;

  * Provide more informative destructor names;

  * Allow quite nice syntax for matching only certain fields.

but:

 * They make code more verbose and the "documentation" supplied is usually
   redundant, as Richard has pointed out.

 * They force users to memorize yet more arbitrary names (is it "ant" or
   "antecedant" or "antecedent" in mk_imp...?)

 * They enforce a tortured programming style by forcing distinctions which are
   not useful. Having to do things like:

     map (fn (t1,t2) => {redex = t2, residue = t1})

   is exactly the thing I find most irritating. It is as if the authors of Unix
   software tools had all chosen a different format for I/O.

For me the disadvantages completely overwhelm the advantages, and I include
substitution patterns in that assessment: I have never had the slightest
trouble remembering which way round they go. I admit there is something to be
said for records in, say, "define_type", which I can never remember how to use.

John.