headers
Bill Page | 2 Apr 2009 19:00
Gravatar

Re: [open-axiom-devel] rep/per again

> | On Thu, Apr 2, 2009 at 12:06 AM, Gabriel Dos Reis wrote:
> | > If you're not proposing to export the Rep, then your proposal is a bit
> | > obscure to me.  Would you mind clarifying why the above does not
> | > amount to exporting the Rep of SomeDomain?
> | >
> Bill Page wrote:
> | Because it is not part of the 'with' clause and appears to the right
> | of ==.
>

On Thu, Apr 2, 2009 at 10:38 AM, Gabriel Dos Reis wrote:
> But with your construct, in the capsule I would be able to tell what
> Rep(SomeDomain) is.   That reveals the Rep of SomeDomain, and
> effectively exports it.
>

Let's take a real example from 'src/algebra/tree.spad.pamphlet':

<<domain BSTREE BinarySearchTree>>=
)abbrev domain BSTREE BinarySearchTree
++ Description: BinarySearchTree(S) is the domain of
++ a binary trees where elements are ordered across the tree.
++ A binary search tree is either empty or has
++ a value which is an S, and a
++ right and left which are both BinaryTree(S)
++ Elements are ordered across the tree.
BinarySearchTree(S: OrderedSet): Exports == Implementation where
 Exports == BinaryTreeCategory(S) with
   binarySearchTree: List S -> %
       ++ binarySearchTree(l) \undocumented
(Continue reading)

Permalink | Reply |
headers
Gabriel Dos Reis | 2 Apr 2009 20:19
Picon
Favicon

Re: [open-axiom-devel] rep/per again

Bill Page <bill.page@...> writes:

| > | On Thu, Apr 2, 2009 at 12:06 AM, Gabriel Dos Reis wrote:
| > | > If you're not proposing to export the Rep, then your proposal is a bit
| > | > obscure to me.  Would you mind clarifying why the above does not
| > | > amount to exporting the Rep of SomeDomain?
| > | >
| > Bill Page wrote:
| > | Because it is not part of the 'with' clause and appears to the right
| > | of ==.
| >
| 
| On Thu, Apr 2, 2009 at 10:38 AM, Gabriel Dos Reis wrote:
| > But with your construct, in the capsule I would be able to tell what
| > Rep(SomeDomain) is.   That reveals the Rep of SomeDomain, and
| > effectively exports it.
| >
| 
| Let's take a real example from 'src/algebra/tree.spad.pamphlet':

I already addressed this in my previous mail.

[...]

| Note: This code is currently the same in both FriCAS and OpenAxiom.

OpenAxiom issues this warning:

   Warnings: 
      [1] OpenAxiom suggests removing assignment to Rep
(Continue reading)

Permalink | Reply |
headers
Ralf Hemmecke | 2 Apr 2009 22:27
Picon

Re: [open-axiom-devel] rep/per again

> | Note: This code is currently the same in both FriCAS and OpenAxiom.
> 
> OpenAxiom issues this warning:
> 
>    Warnings: 
>       [1] OpenAxiom suggests removing assignment to Rep 

Very nice.

> | Since BinarySearchTree is a particular class of BinaryTree for
> | consistency in BinarySearchTree I would expect to see:
> | 
> |  Implementation == BinaryTree(S) add
> |    Rep == List Tree S

> As I said, I would not.  I would not expect any definition of Rep at
> all.   The domain extension says BinaryTree(S) is the Rep of
> BinarySearchTree(S).

In fact, in add-inherited domains

D: C == A add
     Rep == X
     ...

one should not even be allowed to ever write anything else for X than 
just A. I think Open-Axiom is right to remove the necessity of the 
(redundant line "Rep == A").

And why would one want that in Rep==X, X must be the same as A? Because
(Continue reading)

Permalink | Reply |
headers
Bill Page | 6 Apr 2009 18:26
Gravatar

Re: [open-axiom-devel] Re: rep/per again

On Thu, Apr 2, 2009 at 4:27 PM, Ralf Hemmecke wrote:
>
>> | Note: This code is currently the same in both FriCAS and OpenAxiom.
>>
>> OpenAxiom issues this warning:
>>
>>    Warnings:
>>       [1] OpenAxiom suggests removing assignment to Rep
>
> Very nice.
>
>> | Since BinarySearchTree is a particular class of BinaryTree for
>> | consistency in BinarySearchTree I would expect to see:
>> |
>> |  Implementation == BinaryTree(S) add
>> |    Rep == List Tree S
>
>> As I said, I would not.  I would not expect any definition of Rep at
>> all.   The domain extension says BinaryTree(S) is the Rep of
>> BinarySearchTree(S).
>
> In fact, in add-inherited domains
>
> D: C == A add
>     Rep == X
>     ...
>
> one should not even be allowed to ever write anything else for X than
> just A. I think Open-Axiom is right to remove the necessity of the
> (redundant line "Rep == A").
(Continue reading)

Permalink | Reply |
headers
Ralf Hemmecke | 7 Apr 2009 11:04
Picon

Re: [open-axiom-devel] Re: rep/per again

> Having looked at this code in more detail I find I have doubts about
> Gaby's claim: "those domains can be profitably rewritten without
> having to know how FreeModule is implemented". It seems likely to me
> that any attempt to do so could result in a significant loss of
> performance in a very critical and central part of the panAxiom
> library.

If performance suffers then the compiler must improve. I don't see a 
reason why the compiler couldn't optimize away needless function wrappers.

> Of course we can retain the current notation in panAxiom that allows
> Rep to be explicitly specified, separate from 'add', but if we want a
> less idiosyncratic approach were Rep is tied to add-inheritance it
> seems to me we need to seriously consider the option I mentioned
> earlier of making the (default?) Rep X in
> 
>    A: C2 == add
>      Rep == X
> 
> equal to the Rep of C2 and not C2 itself. I think that before choosing
> either option for the treatment of add-inheritance and Rep, it would
> be a worthwhile project to attempt to convert the above add-chain to
> the 'Rep==C2' style of representation and to evaluate the impact that
> that might have on performance.

Bill, you think too much in terms of having all the sources available. 
But imagine that you had no chance in looking inside the domain you 
inherit from. You are definitely not told about the internal representation.

If you just get Rep(X) as you proposed, then what type would that have,
(Continue reading)

Permalink | Reply |
headers
Bill Page | 2 Apr 2009 21:31
Gravatar

Re: [open-axiom-devel] Re: rep/per again

On Thu, Apr 2, 2009 at 2:19 PM, Gabriel Dos Reis <gdr@...> wrote:
> Bill Page writes:
>
> | Since BinarySearchTree is a particular class of BinaryTree for
> | consistency in BinarySearchTree I would expect to see:
> |
> |  Implementation == BinaryTree(S) add
> |    Rep == List Tree S
>
> As I said, I would not.  I would not expect any definition of Rep
> at all.   The domain extension says BinaryTree(S) is the Rep of
> BinarySearchTree(S).
>

Sorry, then this is my confusion. As I said, I expected that the Rep
of BinarySearchTree should be the same as the Rep of the domain from
which it inherits - *not* the domain itself.

My (perhaps poor) understanding of add-inheritance

NewDomain(): with
    ... exports ...
  == OldDomain add
    ... body ...

was that all functions and constants defined in the OldDomain
(regardless of whether they are exported or not) are visible to code
in the body of the new domain. Is that true or not?

In the Axiom Book it says:
(Continue reading)

Permalink | Reply |
headers
Gabriel Dos Reis | 2 Apr 2009 21:58
Picon
Favicon

Re: [open-axiom-devel] rep/per again

Bill Page <bill.page <at> newsynthesis.org> writes:

| On Thu, Apr 2, 2009 at 2:19 PM, Gabriel Dos Reis <gdr <at> cs.tamu.edu> wrote:
| > Bill Page writes:
| >
| > | Since BinarySearchTree is a particular class of BinaryTree for
| > | consistency in BinarySearchTree I would expect to see:
| > |
| > | ═Implementation == BinaryTree(S) add
| > | ═ ═Rep == List Tree S
| >
| > As I said, I would not. ═I would not expect any definition of Rep
| > at all. ═ The domain extension says BinaryTree(S) is the Rep of
| > BinarySearchTree(S).
| >
| 
| Sorry, then this is my confusion.

confusion seems cleared then.

| As I said, I expected that the Rep
| of BinarySearchTree should be the same as the Rep of the domain from
| which it inherits - *not* the domain itself.

I think that is unnecessary leakage.  Indeed, if I understand your
description correctly, 'rep' would return a value of the Rep of old
domain, this achieve the effective effect of exporting Rep -- because,
you can now write functions to get access to that representation.

That breaks abstraction.
(Continue reading)

Permalink | Reply |

Gmane