## Type equivalence of domains in FriCAS and Aldor As a result of the recent message thread about "iterators and cartesian product" in the Axiom library I have been thinking again about type equivalence. For example consider the following domains in FriCAS: fricas (1) -> P:=Product(Stream Integer,
Type: Typefricas Q:=Stream Product(Integer,
Type: TypeOn reflection (pun intended) it seems that Thus we should have: P = Q Side Note: Perhaps with an extension of the domain I understand that neither Spad nor Aldor actually evaluate type expressions like P and Q above so it does not make sense to ask for "value" equality of these two domains. But perhaps EQUAL in the Lisp sense (ref: http://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node74.html) could apply? Therefore I would propose the following definition of type-equivalence of domains: - Def
- Two domains P and Q are equivalent if and only if both domains satisfy
exactly the same set of categories: (P has x) = (Q has x) for all Category
expressions x
*and*neither P nor Q has any explicit exports that are not provided by some named category.
Note (by Waldek): such equivalence is usually called structural equivalence. Spad normally uses "name equivalence": two types are equivalent if and only if they have the same constructor and corresponding arguments are equivalent. It seems that in principle it should be possible to give an efficient decision procedure for this test if it is not already implemented somewhere in the Spad and Aldor compilers. I would like to understand this better from the point of view of the compiler and iterpreter design. Obviously it makes sense to require that two equivalent domains must
provide the same set of exported operations (the same interface)
having the same names and same signatures. But as I understand the
intention of the semantics of categories in both Spad and Aldor this
is not enough. We want categories to represent abstract concepts
usually with a well-defined mathematical meaning. That is the reason
for explicitly referring to satisfaction of categories in the
definition above. Further since domains can also explicitly include
exported operations in the With this definition it is easy to show that the current definitions
of fricas )sh P fricas )sh Q As a minimum it would probably be necessary to introduce two new categories: StreamCat?(S) and ProductCat?(X,Y). Then it would seem that would be necessary add code along the lines of: Product(A: SetCategory,B: SetCategory): ProductCat(A,B) with if A has StreamCat(S) and B has StreamCat(S) then StreamCat(S) And: Stream(S:Type): StreamCat(S) with if S has ProductCat(A,B) then ProductCat(A,B) for some set of allowed domains A, B and S, including for example
Of course we also need the implementations of the associate operations. With these changes we would be able to satisfy the definition of the type-equivalence of P and Q above. I would like to know if other developers think this more algebraic approach to the design of the FriCAS library domains makes sense. Comments and criticisms are invited.
Hi Bill, I unfortunately couldn't make it to the Aldor workshop and I haven't touched the language in a few years, but I do have a comment. Your questions have definite answers in category theory and
since Aldor is http://atlas.bu.edu/~youssef/papers/math/aldor/aldor.pdf I still think that this is a good way to look for flaws in the language - implement category theory and see what goes wrong. Best regards, Saul Youssef
Def: Two domains P and Q are equivalent if and only if both domains satisfy exactly the same set of categories: (P has x) = (Q has x) for all Category expressions x Let's see: Cat: Category == with { coerce: Integer -> %; coerce: % -> Integer; bar: (%, %) -> %; } P: Cat == add { Rep == Integer; import from Rep coerce(x: Integer): % == per x; coerce(x: %): Integer == rep x; bar(x: %, y: %): % == per(rep x + rep y); } ----------------------------------^ Q: Cat == add { Rep == Integer; import from Rep coerce(x: Integer): % == per x; coerce(x: %): Integer == rep x; bar(x: %, y: %): % == per(rep x - rep y); } ----------------------------------^ You are saying that P and Q are equivalent.
No. I should have explicitly written "type-equivalent" as I did elsewhere in that message. I would only want to say that their types are equivalent - that they necessarily represent the same kind of things. Something like: "they are both monoids". I would also say that without giving more information about the use of
the category Regards, Bill Page.
Although it's trivial to see, I thought it might be good to explicitly say that this property can only be checked at runtime--due to Aldor's "extend". If P and Q are type equivalent in the above sense, linking the code with a further library extending only P by another named category breaks type equivalence. In a nutshell, you want each anonymous category to be different from any category. My feeling about Aldor is different: Important exports with well-defined semantics should be defined in named categories. Unimportant exports, syntactic sugar and the like (so all the exports which do not represent some general mechanism and do not contribute to the essence of a domain) may go into unnamed categories. Using such an intuition, unnamed categories and their current semantics for type satisfaction really fit the concept. Still, you could define type equivalence by just checking the named categories and ignoring the unnamed categories. Currently, lots of domains do not stick to this intuition, but that's a different story. As a mininum it would probably be necessary to introduce two new cateogies: StreamCat?(S) and ProductCat?(X,Y). Then it would seem that would be necessary add code along the lines of The code seems to somehow model a distributive law you described above. That's ok for me, but I cannot see how this relates to type equivalence. Assume, I give you a binary operator "type-equivalent?" taking two Aldor entities and computing whether or not they are type-equivalent in the sense you presented in your last mail. What problem can you solve with it? Kind regards, Christian |