[Axiom-developer] Re: rep, per, Rep in SPAD/Aldor

[Gabriel Dos Reis]

Ralf --

  Sorry for the late reply: too many things to fit in only 24 hours/day.

I'll briefly address part of your posting.  I'll address the remaining
later, not that I think it is unimportant (au contraire!), but just that
a more detailled useful answer requires more time from me (which 
unfortunately I don't have right now, like most of you). I'll be going 
(again!) on travel in a few hours.   Many thanks for taking the time to 
expand on this ; it is a very important issue. 

On Fri, 13 Jul 2007, Ralf Hemmecke wrote:

| > However, I do believe that `rep' and `per' are fundamentally part
| > of the language semantics of domain.
| 
| Oh. You explicitly say "domain" (you don't include "package").

Yes, this is important only for things that provide concrete representation.

| So I somehow
| have to agree. But not really. You know that by using "pretend", I could
| remove any uses of Rep, per, rep.

Yes.  But my point is that doing that obscures the semantics.   First and
foremost, `pretend' is an act of violence in the logical conversation
with the translator/compiler: it means `shut up! This is not open for
debate; I know what I'm doing.'  That would be fine, if indeed the
writer also knows what she is doing and what she wrote is indeed what she
intended.  However, that is not true in general.  
Consequently, every use of pretend (whether hidden behind macro or not)
increases the 'trusted code base' (TCB), in addition of trusting the
compiler and other components.  From a verification point of view, that is a
serious problem (or unacceptable trend).

Secondly, what we want to convey with `rep' is not that one can take 
object foo, restrict its interpretation at type T and then do an 
`on faith interpretation of its sequence of bytes representation as 
an object at type U'.   Rather, what we want to say is that object foo 
at type T is the result of a (hopefully injective) mapping from U and we 
are interested in its pre-image.  

That is fundamental to the semantics of Spad domain.  How thar pair
of dual injections is called is really immaterial to developing the
semantics, and you're quite right that you could call it ying/yang
and as far as the semantics is concerned, nothing will change -- just like
Hilbert said one could work out geometry in terms on table and
beer mug instead of line and points.  However, there is another 
component: we need to have a standard name to designate those semantics
objects, just like we need a standard name for the sine and cosine
function to ease communication.  

In conclusion: (1) the semantics of rep/per at the source level
should not be defined in terms of pretend -- even if you could use
it to illustrate some uses (not all).  (2) We need to standardize
on common names for common semantics, and having this automatically
check is Good.


| Of course, nobody should write that code but
| rather follow the convention with Rep. What you want is to turn a convention
| into a rule.

Well, it you take it that way then we must not forget that language
is social convention.

| All I want to say is that this conflicts a bit with the design
| goals of Aldor: rather remove restrictions than introducing new features. I
| actually thought that you adhere to this principle. ;-)

Yes, I'm for removing unnecessary restrictions.  But, I do not view
the fact giving rep/per would a clearer semantics as a restriction. 

-- Gaby