continuing the discussion of aleph 0 - comments please!

[Jose E. Marchesi]

Hi Chris.

> Hello all,  recently I wrote to the list as follows regarding ℵ0:
>
> For example, from RR § 25.3.1.1
>> >
>> > MODE ℵ0 BOOK =
>> >     STRUCT (FLEXTEXT text,
>> >         POS lpos ¢ logical end of book ¢,
>> >         STRING idf ¢ identification ¢,
>> >         BOOL putting ¢ TRUE if the book may be written to ¢,
>> >         INT users ¢ the number of times the book is opened ¢);
>> >
>> > So the RR 25.1.3 states, in Step 2:
>> >
>> > If, in some form, as possibly made in the step above, ℵ0 occurs followed
>> by
>> > an INDICATOR (a field-selector) I, then that occurrence of ℵ0 is deleted
>> > and each INDICATOR (field-selector) akin {151 .1.3.2.k} to I contained in
>> > any form is replaced by a copy of one same INDICATOR (field-selector)
>> which
>> > does not occur elsewhere in the program and Step 2 is taken again.
>> >
>> > [The RR] replaced the ℵ0 with the dash-question-mark symbol;
>> > but as far as I can tell, ultimately it's not the symbol that's giving me
>> > the heebiejeebies here, it's what do do about it.
>> >
>> > That is, I don't understand - at all - the significance of ℵ0 in the
>> > definition of the BOOK mode above.
>> >
>> > For instance, "ℵ0 occurs followed by an INDICATOR (a field-selector)" -
>> how
>> > closely is "followed"?  "FLEXTEXT text" follows ℵ0 (eventually); does
>> that
>> > count?  Or does the intervening "STRUCT" "OPEN-SYMBOL" preclude the
>> > deletion of ℵ0 in this case?
>> >
>> > Put another way, does
>> >
>> > MODE BOOK =
>> >     STRUCT (FLEXTEXT text,
>> >         POS lpos ¢ logical end of book ¢,
>> >         STRING idf ¢ identification ¢,
>> >         BOOL putting ¢ TRUE if the book may be written to ¢,
>> >         INT users ¢ the number of times the book is opened ¢);
>> >
>> > ie without the ℵ0, have the same semantic import?
>
>
> Jose kindly responded:
>
> ℵ0 is just intended to describe "secret" or inaccessible entities.  Any
>> mode indicant (INDICATOR) or field selector (field-selector) marked by
>> it is substituted by some mode indicant or field selector that only
>> occur once (in their definition) in the program.  i.e. they are
>> conceptually replaced by some unique string that is not referred
>> elsewhere in the program.
>
>
> Ok, I think I understand, in general terms.  "mode ℵ0" is a way of hiding
> the details from users of the mode, similar to what we might call "opaque
> types" in more recent programming languages.

Yes.  Same when applied to some other declared entity as a whole.

> What's not completely obvious to me is that, whereas I think Book must be a
> publicly known mode (even if its details are opaque), I'm pretty sure that
> modes Flextext and Pos are not meant to be publicly known.
>
> Contrast the definition of Book with that of Channel, in the RR pp 141 -
> 142:
>
> mode ℵ0 Book =
>     struct (Flextext text,
>         Pos lpos { logical end of book },
>         string idf { identification },
>         book putting { TRUE if the book may be written to },
>         int users { the number of times the book is opened });
>
> mode ℵ0 Text = ref [ ] [ ] [ ] char;
> mode ℵ0 Flextext = ref flex [ ] flex [ ] flex [ ] char;
> mode ℵ0 Pos = struct (int p, l, c);
>
> mode Channel =
>     struct (proc (ref Book) bool ℵ0 reset, ℵ0 set, ℵ0 get, ℵ0 put, ℵ0 bin,
>         ℵ0 compress, ℵ0 reidf,
>         proc bool ℵ0 estab, proc Pos ℵ0 max pos,
>         proc (ref Book) Conv ℵ0 standconv, int ℵ0 channel number);
>
> mode ℵ0 Conv = struct ([1 : int (skip)] struct (char internal, external) F);
> proc estab possible = (Channel chan) bool: estab of chan;
> proc standconv = (Channel chan) proc (ref Book) Conv: standconv of chan;
>
> Starting with the definition of mode Channel and working back to the
> definition of mode Book:
>
>    1. proc standconv has no ℵ0 so it is published, correct? and yet it is
>    only used elsewhere in the RR by proc establish and proc open

Yes.  standcov is visible to the user.

>    2. proc estab possible has no ℵ0 so it is published, correct? and yet it
>    does not seem to be used anywhere else in the RR

You are supposed to call estab_possible passing some channel, to
determine whether you can "establish" files in that channel.

>    3. mode Conv has ℵ0 so it is non-published, correct?  by the way what is
>    that capital F?  unusual to see a capital letter for a structure name in
>    the RR, is it not?

The mode Conv is not published.

>    4. mode Channel has no ℵ0 so it is published, correct?  so in theory, we
>    know that it is a structure but its fields are non-published

Right.

>    5. modes Text, Flextext and Pos have ℵ0 so they are non-published,
>    correct?

Right.

>    6. mode Book has ℵ0 so it is non-published, correct?  and because it has
>    ℵ0, the fact that it is a structure and the nature of its fields are also
>    non-published, correct?

Right.

> Now it seems to me that proc standconv is wrongly published since it
> returns a result of proc (ref Book) Conv whereas both Book and Conv are
> non-published.

That's no matter.  Algol 68 uses structural equivalence of modes, which
is really orthogonal and simplifies a lot of things, including
(ironically perhaps) effective hidding of information.  If you have
something like:

  module Transput =
  def
      mode Book = C whatever C, Conv = C whatever else C;
      pub mode Channel = struct ([...] proc(ref Book)Conv standconv);

      pub proc standconv = (Channel chan) proc(ref Book)Conv:
         standconv of chan;

      [...]
  fed

As a user of the Transput module you cannot refer to a Book mode by
name, but you can still call standconv and get a procedure that gets a
ref to 'whatever' and then returns a 'whatever else'.  Both 'whatever'
and 'whatever else' modes, or their structure if you like, will be in
the exports of the module, but not named as Book nor as Conv.

So what structural equivalence achieves here is that, as a user, you
know that standconv is returning the "standard conversion routine" to be
used for books opened via that channel, but you cannot (easily) use the
routine directly because you don't know how to interpret the result: it
is to be used internally and all you are supposed to do is to get it and
set it, from a list of pre-defined conversion routines provided by the
same Transput module.

> I also doubt that proc estab possible should be published, but since it
> does not seem to be called... maybe I'm missing something.

I would say it is the user that is supposed to use that routine.

> Moving over to van Vliet's version, mode Book is defined as:
>
> mode ℵ0 Book =
>     Pseudo1 {Some mode, whose values contain at least the following
>         operating-system-dependent information:
>          - the identification string;
>          - some reference to the actual information, and some indication
>            where to read or write the next buffer (see also section 4.4.1);
>          - the logical end of the book ;
>          - information that tells whether the book may again be opened
>            for input or output. ;
>         - the maximum size of the book, as set by 'construct book' (f) or
>           'find book in system' (e).
>         To avoid excessive copying of information, the implementer is
>         advised to define the mode {BOOK as a reference to the necessary
>         data. };
>
> mode ℵ0 Pos = struct (int p, l, c);
>
> Note that van Vliet avoids defining all structure within mode Book with the
> exception of mode Pos which is used elsewhere.

Note how, again, the user can use positions around with no problem,
which are a struct with three integers, only not by name Pos.

> mode Channel is defined as:
>
> mode Channel =
>     Pseudo6 {Some mode, whose values determine at least the
>     following information:
>     - the standard conversion key of the channel (d);
>     - the buffer primitives of the channel (m);
>     - the access properties of the channel (l);
>     - whether or not another file
>       may be "established" (5.2.a) on the channel (c);
>     - the (next) default identification
>       string of a book linked via this channel (4.1.2.g);
>     - the default size of a book linked via this channel (n);
>     - the maximum size of a book linked via this channel (4.1.2.f). };
>
> mode ℵ0 Conv =
>     struct (proc (ref File, char) void write char,
>         proc (ref File, Binchar) void write bin char,
>         proc (ref File, ref char) bool read char,
>         proc (ref file, ref Binchar) bool read bin char);
> proc estab possible (Channel chan) bool:
>     bool(Pseudo7) { a routine which returns true if another file
>         may be "established" (5.2.a) on the channel 'chan' };
> proc standconv = (Channel chan) proc (Book) Conv:
>     proc (Book) Conv(pseudo8) {a routine which may be used to obtain the
> default
>         "conversion key"; note that the actual primitives are not obtained
>         until some specific book is provided also };
>
> Once again, both procs standconv and estab possible are to be published.
> Also notice that, unlike the definition given by the RR, mode Conv is a
> structure of read and write procedures that deal with reading a character
> from or writing a character to a file.
>
> Given all of the foregoing, I don't see any reason why we cannot follow van
> Vliet's code more closely than that of the RR.

I agree.  The van Vliet work was precisely to get something usable from
the more "specification only" nature of the RR transput listings.

>
> I also asked
>
>
>> > Moving on to a concrete question, Jose, do you see sppp dealing with
>> these
>> > ℵ0 things?  Or will we need some other pre-processor to accomplish what
>> is
>> > needed?  Or can we move to the super-language instead?
>
>
> to which Jose responded
>
>  In our case, in practice, this means that entities marked with ℵ0 should
>> not be pub-licized in the module implementing the transput, so:
>
>
>>   module Transput =
>>   def
>>      [...]
>
>
>>      proc book_bounds = (ref File f) Pos: skip; { marked with ℵ0 }
>>      pub proc char_number = (ref File f) int: skip; { not marked with ℵ0 }
>>   fed
>
>
>> Same for modes, priorities and operators.
>
>
>> As for secret field names in structs... thats something not supported by
>> Algol 68 even with the modules system: there are no secret fields and
>> the user can always refer to them should she find out the names somehow.
>> We can probably come with some extension for this if we wanted to, to
>> improve security, but when it comes to implement the transput I think it
>> is ok to just document these fields as non-public.
>
>
> So in short, it seems we're not relying on sppp to deal with our ℵ0
> occurrences, but rather using modules and published / non-published
> components to accommodate this opaqueness, as best as possible.

Right.

> Thus I guess we can imagine, again following van Vliet's version, that
>
>    1. mode Book, mode Pos are not to be published;
>    2. mode Channel and procs estab possible and standconv are to be
>    published;
>    3. and similarly other modes, procs etc whose definition includes ℵ0 are
>    not to be published;
>    4. fields of published structures whose definition includes ℵ0 should
>    not be visible outside the module but, as far as current module features
>    go, we have no way of defining a published but opaque type, so we will
>    document the intended hidden nature of the fields.

Yeah.

An obvious solution would be to add a pragmat #<aleph> associated with
struct fields so we can effectively hide them, but I am (vaguely as of
yet) playing with the idea of introducing an actual aleph0 character
usable in both tags and indicants, that compares false to any other
character other than its particular instance, i.e. using some sort of
globally-unique-id.  This would be to be used to define "unique" modes
in the existing frame of structural equivalence.

This is all vague as of yet, but consider the typical algol68 situation
where you have two different data structures, similar in structure but
different in meaning:

  mode Point = [3]int, Vector = [3]int;

Both points and vectors are structurally defined similarly, but they are
different entities.  If you then wanted to define operators like:

  op + = (Point a, b) Point: skip,
         (Vector a, b) Vector: skip;

you will get a compile-time error, because Points and Vectors are firmly
related (they are in fact the same mode).  The traditional solution is
to use structs instead, because the names of struct fiels are part of
the mode:

  mode Point = struct (int a, b, c), Vector = struct (int x, y, z);

Then Point and Vector are no longer structurally equivalent.

This works well, but technically speaking there may be another struct
(int a, b, c) that is not a Point.  This may happen when importing
modules for example.

So my idea is to have a character allowed in tags that play exactly the
role of Aleph0 in the RR: tags with this character are assured to appear
only exactly once in any particular program.  I thought about using
leading underscores.  So something like:

  mode Point = struct (int _a, _b, _c), Vector = struct (int _a, _b, _c);

The first time _a is found the _ gets internally replaced by an
globally-unique id.  The second _a is found, this time in Vector, the
same happen.  Both ids are part of the modes, as part of the field tags.

When you refer to an aleph0 endowed field:

   _a of x

then you will be referring to the _a of Point if x is a Point or to the
_a of Vector if x happens to be a Vector.

This is all still flaky, but I am thinking in that direction...

> By way of illustration of the latter, assuming that the eventual definition
> of mode Channel follows that of the revised report (recognizing van Vliet
> leaves that as an exercise for the implementor), we might expect to see
>
> pub mode Channel =
>     struct (proc (ref book) bool { hidden } reset, { hidden } set, { hidden
> } get, { hidden } put,
>         { hidden } bin, { hidden } compress, { hidden } reidf,
>         proc bool { hidden } estab, proc pos { hidden } max pos,
>         proc (ref book) conv { hidden } standconv, int { hidden } channel
> number);
>
> or perhaps
>
> pub mode Channel = { opaque }
>     struct (proc (ref book) bool reset, set, get, put,
>         bin, compress, reidf,
>         proc bool estab, proc pos max pos,
>         proc (ref book) conv standconv, int channel number);
>
> The latter appeals to me more than the former, but we may have modes with
> some hidden and some published fields (which would be ugly and weird in
> principle, but who knows).

I prefer the later.

> Comments, thoughts, criticisms much appreciated.

Thank you for working on this! :)