RE: [Axiom-developer] Cast = pretend in Spad/Aldor?

[Bill Page]

On November 23, 2005 5:56 AM Ralf Hemmecke wrote:
> ...
> >> Bill Page wrote:
> >>> http://wiki.axiom-developer.org/RepAndPer
> 
> Just one comment to this website. I don't think that
> rep: % -> Rep could be seen as a forgetful functor.
> Surely, it forgets the signatures of % (ie, its category),
> but it also introduces a structure.

For reference, here is a link to my current favourite online
source:

http://en.wikipedia.org/wiki/Forgetful_functor

Remember that a functor is a morphism (mapping) from one
category (in the sense of category theory) to another. In Axiom
these categories are implemented as domains.

A functor does not actually add or delete structure as such.
The structure remains present in the underlying categories. In
the case of a forgetful functor the image of the source category
in the target looses some of the structure that was present in
the source, but that does not preclude the target category from
having more structure of a different kind.

So what I am suggesting is that 'rep' is a forgetful functor that
is faithful but not full. It can tell us for example that an
object of Float i.e. an Axiom floating point number, corresponds
to a object of record(mantissa:Integer, exponent:Integer) but
certainly the domain record(mantissa:Integer, exponent:Integer)
as a product category has additional structure.

> 
> Take, for example,
> 
> IntegerGroup: Group == add {
>    Rep == Integer;
>    (x: %) + (y: %): % == per(rep x + rep y);
>    ...
> }
> 
> Here rep forgets the Group structure of % and gains (at 
> least) the Ring structure of Integer.

I think this is a good example. The forgetting part is quite
simple, but the really important job is actually done by 'per'.
Here this functor maps the + operation of Integer into the +
operation of IntegerGroup.

> > 
> > I would be interested to learn of any examples where this sort
> > of use of 'pretend' [as system level code] was essential, i.e.
> > where it can not be replaced with some operations defined on
> > the underlying domains.
> 
> I think it was nowhere essential. If a programmer thinks for
> some efficiency reasons to pretend that some A is some
> particular type B that might come from the fact that A does
> not provide certain functions. I would argue, that in this case
> A is simply not rich enough. So the design was not the best
> from the beginning.

I agree.

> 
> See also
>    http://www.aldor.org/docs/HTML/chap7.html#6
>

Here is read:

"Primitive conversions

The language provides one primitive type conversion operation:
pretend. A ``pretend'' expression is used to lie about the type
of a value.

      Expr pretend Type

causes the value computed by Expr to be treated as though it were
of type Type. pretend is the only operator in Aldor which is not
type-safe: using pretend can lead to unchecked type errors which
only reveal themselves when a program is executed. For this reason
pretend should be used with caution. For example, one could use
``pretend'' to examine the bit-level representation of data when a
type does not provide operations to do so.

Two additional type-safe operations are defined in Aldor using
pretend: rep and per. These operators convert between the public
and private views of a type, and are discussed in section 7.8."

--------

Thank you! That is exactly the kind of statement I was looking
for. I guess I must have read that as one time or other but had
forgotten where.

> I cannot remember that I have seen pretend being used in some 
> essential way. Anyway, if it were essential, then I'd rather like
> to have all such domains defined at a very low level and forbid
> "pretend" for all users who are going to implement mathematics.
> 
> There is some use of "pretend" though, where I could not do 
> without it.
>
> bar(F: Field): F == ...
> foo(R: Ring): () == {
>    ...
>    if R has Field then result:= bar(R);
>                   else result:= 1;
>    result;
> }
> 
> The Aldor compiler should be able to compile such code, but the
> current implementation does not realize in all cases that in
> bar(R) the R is actually a field, so I'd have to say
> "bar(R pretend Field)".
> However, that is a weakness of the compiler and not a necessity
> for "pretend". (P.S.: I don't claim that this particular piece
> of code above does not compile, but I remember that I experienced
> cases, where the structure was similar.)

I agree that such a case would be a compiler error. The use of
'pretend' here is clearly type-safe. I wonder if we can find
examples of this in the Axiom Spad code?

> 
> >> For Rep, rep and per, I (personally) believe they should have
> >> been language primitives, except that add-inheritance confuses
> >> the issue a little. They should definitely be thought of as
> >> primitive.
> 
> I fully agree, although I don't quite understand that part 
> "except that add-inheritance confuses the issue a little".
> But I think the language designers were minimalistic. Instead
> of introducing two primitives "rep" and "per", they introduced
> only "pretend".

Since 'pretend' is manifestly type-unsafe and considerably more
dangerous than what is required for 'rep' and 'per', it seems to
me that this design in not consistent with the goals of Aldor.

> 
> >> There is an idea of adding a third operation 'per?', defined
> >> by the programmer which tests if an object of type Rep is
> >> really a member of %, and would be called immediately before
> >> each 'per' operation.  I'd hate to be forced to write it each
> >> time though.
> 
> How can they be different anyway? To me it is even not completely
> clear whether Rep is a language primitive or not. I don't remember 
> that I have read anything about Rep being a primitive, furthermore,
> some time ago one would have written "Rep ==> Integer" and not 
> "Rep==Integer" as it is suggested now. See
> http://www.aldor.org/docs/HTML/chap7.html#8 (subsection 
> Representation).
>

Since 'rep' need not be full (i.e. not surjective) there may be
objects and operations of 'Rep' that do not correspond to any
object or operation of %. But my argument was that we need only
be concerned about those object of 'Rep' that are manipulated
internally by the logic of domain %. I think correct logic
implies that these objects will all be in the image of 'rep'.

As you said earlier, it seems that 'rep', 'per' and 'Rep' where
not chosen by the Aldor language designers as primitive but
rather defined by a macro, just as in Spad. As far as I know for
the purposes of the 'rep' and 'per' macros you can still use the
notation "Rep ==> Integer" interchangeably with "Rep==Integer",
is this not the case?

If the concept of representation in domains was to be made a
primitive in the Aldor language, then I think one might wish
for more syntactic sugar than provided at present. For example
why not a construct like:

  IntegerGroup: Group == add {
     internal Integer;

     (x: %) + (y: %): % == ::(x:: + y::);
     ...
  }

where we must distinguish infix (conversion), prefix ('per') and
postfix ('rep') use of the type symbol :: But I have to admit I
have not spent much time thinking about the consequences of such
notational change. Probably there are better ideas.

> > since the representation is supposed to be purely internal to
> > the domain, right?.
> 
> And this is an advantage. Let's look at the Aldor libraries. 
> There are two variants, libaldor.al and libaldord.al. The second
> one is a "DEBUG" version and sometimes quite handy to find bugs.
> Take, for example, the implementation of PritiveArray in both
> libraries.
> 
> It starts like this.
> 
> PrimitiveArray(T:Type): PrimitiveArrayType T == add {
>    import from Machine;
> #if DEBUG
>    Rep == Record(sz:Z, data:Arr);
>    local size(x:%):Z == {import from Rep;
>      empty? x => 0; rep(x).sz
>    }
>    local arr(x:Arr, n:Z):% == {import from Rep;
>      zero? n => empty; per [n,x]
>    }
>    local data(x:%):Arr == {
>      import from Rep;
>      empty? x => (nil$Pointer) pretend Arr;
>      rep(x).data;
>    }
> #else
>    Rep == Arr;
>    local data(x:%):Arr          == rep x;
>    local arr(x:Arr, n:Z):% == per x;
>    local arr(x:Arr):%   == per x;
> #endif
>    array(p:Pointer, n:Z):% == arr(p pretend Arr, n);
>    pointer(a:%):Pointer == data(a) pretend Pointer;
> 
> So if you are going to use PrimitiveArray later in your program,
> you could hardly use "pretend" until you happen to have the 
> sources and know the dependency on the DEBUG flag.
>

For sure. There are probably many other cases where one might
want to change the internal representation of some domain without
affecting any other code in the library. The indiscriminate use
of 'pretend' could make this dangerous.
 
> But for the outside world both are indistinguishable, because 
> they are both of PrimitiveArrayType(T).
> 
> Oh, I am just realizing here is also a "pretend Arr". That is 
> low level programming and completely hidden in PrimitiveArray.
> But this also looks like efficiency considerations. If there were
> a better documentation of Arr available then it would certainly
> be unnecessary. But then maybe Arr would use "pretend" or is
> completely implemented in C or so. One has to start somewhere,
> so consider PrimitiveArray as a primitive type and never worry
> about "pretend" anymore when building on it.
> 

I do not understand the use of 'pretend' in the statements

   array(p:Pointer, n:Z):% == arr(p pretend Arr, n);
   pointer(a:%):Pointer == data(a) pretend Pointer;

above. Also the meaning of type Pointer also worries me.
Could you explain this or refer me to the appropriate section
of the Aldor documentation?

Ralf, thank you very much for your comments!

Regards,
Bill Page.