Bill Page <bill.p...@newsynthesis.org> 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':
|
| <<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
| insert_!: (S,%) -> %
| ++ insert!(x,b) inserts element x as leaves into binary search tree b.
| insertRoot_!: (S,%) -> %
| ++ insertRoot!(x,b) inserts element x as a root of binary search tree b.
| split: (S,%) -> Record(less: %, greater: %)
| ++ split(x,b) splits binary tree b into two trees, one with
| elements greater
| ++ than x, the other with elements less than x.
| Implementation == BinaryTree(S) add
| Rep := BinaryTree(S)
| binarySearchTree(u:List S) ==
| null u => empty()
| tree := binaryTree(first u)
| for x in rest u repeat insert_!(x,tree)
| tree
| insert_!(x,t) ==
| empty? t => binaryTree(x)
| x >= value t =>
| setright_!(t,insert_!(x,right t))
| t
| setleft_!(t,insert_!(x,left t))
| t
| split(x,t) ==
| empty? t => [empty(),empty()]
| x > value t =>
| a := split(x,right t)
| [node(left t, value t, a.less), a.greater]
| a := split(x,left t)
| [a.less, node(a.greater, value t, right t)]
| insertRoot_!(x,t) ==
| a := split(x,t)
| node(a.less, x, a.greater)
|
| @
|
| Apparently your analysis would require that 'BinaryTree(S)' is
| "effectively exported" but of course it is not.
And of course, that is not my reasoning. My reasoning, the semantics
implemented in OpenAxiom, is that BinaryTree(S) is the Rep of
BinarySearchTree(S). And it is never exported.
And the assignment
Rep := BinaryTree(S)
is redundant, and OpenAxiom will issue a warning
Warnings:
[1] OpenAxiom suggests removing assignment to Rep
and if you try to assign a different value, you should get an error.
| In my proposal one
| would write:
|
| Implementation == Rep BinaryTree(S) add
| binarySearchTree(u:List S) ==
| null u => empty()
| ...
In OpenAxiom, you just leave out the leading Rep, and you are just fine.
I confess I do not see the benefit of your proposed notation, since
the semantics you want it already there with less to write.
|
| I can see no reason why this might imply to someone that BinaryTree(S)
| is somehow "exported" when the example above does not.
I had assumed that you were somehow familiar with the OpenAxiom
semantics, and consequently you were proposing an enhancement which I
could not see. It turns out that, the proposal was a confusing
notation for something already implemented.
| --
|
| But there is an interesting problem in the example above.
| BinaryTree(S) is *both* add-inherited and specified as Rep. This is a
| mistake.
Yes. One that is warned about by OpenAxiom.
| We should not say that a BinarySearchTree is represented as a
| BinaryTree but rather that a BinarySearchTree is a particular class of
| BinaryTree, i.e one where the nodes of the tree are in a specific
| order. They share the same underlying representation but they are
| constructed by a slightly different set of methods.
|
| The Rep of BinaryTree(S) is 'List Tree S':
|
| <<domain BTREE BinaryTree>>=
| )abbrev domain BTREE BinaryTree
| ++ Description: \spadtype{BinaryTree(S)} is the domain of all
| ++ binary trees. A binary tree over \spad{S} is either empty or has
| ++ a \spadfun{value} which is an S and a \spadfun{right}
| ++ and \spadfun{left} which are both binary trees.
| BinaryTree(S: SetCategory): Exports == Implementation where
| Exports == BinaryTreeCategory(S) with
| binaryTree: S -> %
| ++ binaryTree(v) is an non-empty binary tree
| ++ with value v, and left and right empty.
| binaryTree: (%,S,%) -> %
| ++ binaryTree(l,v,r) creates a binary tree with
| ++ value v with left subtree l and right subtree r.
| Implementation == add
| Rep := List Tree S
| t1 = t2 == (t1::Rep) =$Rep (t2::Rep)
| ...
|
| Note: This code is currently the same in both FriCAS and OpenAxiom.
|
| 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
In fact, I do not expect this at all. It is just an invitation for
breaking abstraction barrier, and maintaince nightmarre.
I do not expect a Rep definition in an domain extension.
Currently the OpenAxiom library violates that principle only in the
cases where the representation are the same. I have no plan to
encourage that.
| Note: The 2nd line above is not required in OpenAxiom.
Exactly.
| But then we must change the implementation slightly.
|
| binarySearchTree(u:List S) ==
| tree := empty()
| for x in u repeat insert_!(x,tree)
| tree
| insert_!(x,t) ==
| empty? t => node(t,x,t)
| x >= value t =>
| setright_!(t,insert_!(x,right t))
| t
| setleft_!(t,insert_!(x,left t))
| t
I do not understand what you mean
|
| > | Similarly, the operations of OldDomain are not automatically
| > | exported in
| > |
| > | Foo(...): with
| > | ...
| > | == OldDomain add
| > | ... rep ... per ...
| > |
|
| That is my main point. The next paragraph in my email was misplaced. I
| am sorry for the resulting confusion.
|
| > | The result is exactly the same as if I had written:
| > |
| > | Foo(...): with
| > | ...
| > | == add
| > | Rep==SomeDomain
| > | ... rep ... per ...
| >
| > No, the result is not the same. In the second form, you'll have to
| > write bunch of functions (for Foo) that implement functions
| > implemented by OldDomain and exported by both.
| >
|
| I only meant to repeat here that the intended semantics of
|
| > # Foo(...): with
| > # ...
| > # == Rep(SomeDomain) add
| > # ... rep ... per ...
|
| is exactly the same as writing:
|
| > | Foo(...): with
| > | ...
| > | == add
| > | Rep==SomeDomain
| > | ... rep ... per ...
|
| Regards,
| Bill Page.
------------------------------------------------------------------------------
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
