Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
To: David Shepherd <des@inmos.co.uk>
Cc: info-hol@cs.uidaho.edu (info-hol mailing list)
Subject: Re: HOL90 - Syntax
In-Reply-To: Your message of "Tue, 15 Mar 94 10:42:24 GMT." <15303.9403151042@frogland.inmos.co.uk>
Date: Tue, 15 Mar 94 12:01:05 +0000
From: Richard Boulton <Richard.Boulton@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:035350:940315120118"@cl.cam.ac.uk>

I agree that for many functions, using records is a good idea. As David says,
it helps to have some clue as to what each argument is meant to be. A good
example is the substitution lists taken by some HOL functions. I've always
found it difficult to remember whether the thing to be substituted comes first
or second when pairs are used. Having them labelled is a big help.

However, in the case of the HOL type and term constructor and destructor
functions, I think the ordering (and usually the purpose) of the components of a
tuple are obvious. The order is simply the left-to-right order in the concrete
syntax. Thus, mk_comb takes the (ope)rator first and the (ope)rand second,
dest_eq returns a pair in which the first element is the LHS and the second is
the RHS, etc.

But what are the advantages of tuples over records? Well, as someone who writes
code for HOL far more than I actually use the system for proof, I find that the
use of records in term constructors/destructors makes code more verbose and in
particular it often makes the difference between something fitting on one line
or not. A further advantage of tuples is that a destructor can be mapped over a
list of terms and then pulled apart using `split' (and `zip' in the other
direction), whereas with records a special-purpose ML abstraction has to be
written.

Here is an example from the arith library (hol90):

   fun mk_arith_op tok ftok =
    let val num_ty = mk_type{Tyop = "num",Args = []}
        val fun_ty = mk_type{Tyop = "fun",
                             Args = [num_ty,mk_type{Tyop = "fun",
                                                    Args = [num_ty,num_ty]}]}
    in  fn (t1,t2) => (mk_comb{Rator = mk_comb{Rator = mk_const{Name = tok,
                                                                Ty = fun_ty},
                                               Rand = t1},
                               Rand = t2}
                       handle _ => failwith ftok)
    end;

And in HOL88:

   let mk_arith_op tok ftok =
    let num_ty = mk_type(`num`,[])
    in  let fun_ty = mk_type(`fun`,[num_ty;mk_type(`fun`,[num_ty;num_ty])])
    in  \(t1,t2). (mk_comb(mk_comb(mk_const(tok,fun_ty),t1),t2)
                   ? failwith ftok);;

I see that I manage to shoot myself in the foot with this example in that
mk_type doesn't actually take its arguments in the order of the concrete
syntax, but there is still no ambiguity because they are of different types.

In conclusion, I would like to see tuples used for the type and term
constructors/destructors, with records retained for functions that take
substitution lists and where the meaning of each component is not obvious from
the concrete syntax.

Richard.