Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <15303.9403151042@frogland.inmos.co.uk>
Subject: Re: HOL90 - Syntax
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Tue, 15 Mar 1994 10:42:24 +0000 (GMT)
In-Reply-To: <"i80fs2.ira.496:15.02.94.07.50.59"@ira.uka.de> from "reetz" at Mar 15, 94 08:50:53 am
Content-Type: text
Content-Length: 2867

reetz has said:
> Konrad writes:
> > The decision to adopt records was made without consulting the HOL
> > community, a point that has been made to me many times (usually by John
> > Harrison). It seems that a reasonable time has passed for people to
> > decide if they like them. So: what do people think?
> 
> IMHO it is not a big thing. Adapting to the new "syntax" was'nt a big
> deal, just a boring one. IMHO, it's a question of taste:
> reading   #conseq   is somewhat nicer than   snd    . Furthermore, my students 
> found it easier to remember. As Jim Grundy has noted, changing back would
> be just another boring work to do I really wouldn't like to.

I thought it was a bit irritating the first time I met it (after all I
*knew* what each element in a tuple was) however I soon realised that
it was a good idea ... especially if you have a function with several
arguments that you use rarely - its quite nice to be able to see  from
the type what info you need to supply rather than having to look up in
the documentation what each bit of a `:string * term * term` does.

Its rather like the experience I had when I first used ML. Before the
only functional language I had used was KRC which was totally untyped.
So I always  *knew* that certain data elements were lists  in whicgh
each element was a tuple of a string and a list of string pairs, or
something like that - I initially found the fact that ML was strongly
typed a restriction (you couldn't pull tricks like suddenly deciding if
the first element was the empty string then the second element was
actually just a pair of strings rather than a list of pairs etc). But I
soon realised the benefits of strong typing. Basically, what the record
idea gives is an extra level of sanity checking in your code.

Finally, I think another reason why it is necessary is that SML handles
tuples differently from ML. In ML the "," operator forms pairs. In SML
it forms tuples which are a specialised type of record. 

In ML:	(1,2,3)	= (1,(2,3))
In SML:	(1,2,3) = {#1=1, #2=2, #3=3}

In ML:	# let (a,b) = (1,2,3);;
	a = 1
	b = (2,3)
In SML:	- val (a,b) = (1,2,3);
	type check error.

So many of the pattern matching tricks used in ML code wouldn't work in
SML in any case - so its simpler to go to the underlying mechanism used
in SML and give them better names that #1, #2, ...

There is the hol88 library which pulls back some of the old syntax, but
personally, whenever I find anything that uses it I spend the necesaary
half hour or so going through the code and converting everything to use
the "proper" syntax.

 

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"I  am  not  a  nut      ---      I  am  a  human  being."