"Bill Page" <[EMAIL PROTECTED]> writes:
[...]
| But this notwithstanding, let me at least try to answer your question
| about why I think universal quantification might lead to something
| "not algebraic". This is still only "half baked", but I did not mean
| to say that there was something necessarily non-algebraic about
| universally quantified types. But to be "algebraic" in the (admittedly
| still unclear) sense in which I meant it, I think that universal
| quantification must enter the language only in a "constructive"
| manner.
What is nonconstructive about
forall(T: Type)
identity(T x) == x
which can be used as
identity 4.4 -- T deduced to Float
identity "string" -- T deduced to String
?
I'm trying to understand, so take the questions as a way to
help me fill in lot of blanks I have at the moment regarding your
comments.
| This means (for example) that if I write:
|
| MyDomain(a:MyCatA(x:X)): MyCatB(y:Y)
|
| where the name 'y' does not appear in any expression in the argument
| list of MyDomain and 'x' does not appear in any expression of the
| category to which MyDomain belongs, then it is correct to interpret
| 'y' as universally quantified and 'x' as existentially qualified only
| in the following sense:
|
| MyDomain(a:Meet(MyCatA(x) for x in X) ): Join(MyCatB(y) for y in Y)
That is possibly one way of doing things.
There are at many ways to interprert the above, amoung which
forall(X: Type, x: X, Y: Type, y:Y) .
MyDomain(a: MyCat x): MyCatB y
forall(X: Type, x: X) . exist(Y: Type, y:Y) .
MyDomain(a: MyCat x): MyCatB y
forall(X: Type) . exist(x: X) . forall(Y: Type) . exist(y: Y) .
MyDomain(a: MyCat x): MyCatB y
forall(X: Type, x: X) .
MyDomain(a: MyCat x): exist(Y: Type, y: Y) . MyCatB y
forall(X: Type, x: X) .
MyDomain(a: MyCat x): forall(Y: Type) . exist(y: Y) . MyCatB y
...
some of them may be equivalent (I don't know). But at least there are
many possible interpretation for
MyDomain(a:MyCatA(x:X)): MyCatB(y:Y)
could you explain why that particular one, you chosed?
|
| In other words this domain must satisfy all such categories
| 'MyCatB(y:Y)' for all y in Y. Similarly the parameter 'a' of MyDomain
| is a domain that satisfies at least one of the categories
| 'MyCatA(x:X)' for some x in X. This can be extended to more complex
| dependencies in a mostly obvious manner. The significance of these
| rules is that we know exactly how to write 'MyDomain', i.e. which
| operations to expect from domain 'a' and when operations we must
| export.
|
| It is not clear to me if what you are proposing would always fit these
| restrictions.
so it is strange before you actually know what it is? Hmm. :-/
|
| 'Meet' is the built-in category constructor dual to 'Join' that was
| also briefly discussed at the workshop.In Axiom (but not Aldor!)
| 'Type' is just the top of the category lattice where all categories
| "meet" and which exports no operations.
|
| > ...
| >>
| >> I took that fact that this approach of passing symbols that are
| >> evaluated as names of exported functions "almost works" as evidence
| >> that some changes were made to Spad that were intended to make this
| >> possible. (Why else evaluate the function names?).
| >
| > I suspect the right question is why category expressions are evaluated at
| > compile time. The answer is to get the list of exported operations.
| >
|
| The answer to that question is obvious.
In that case, the answer to the following question
| But why does it evaluate the function names?
is obvious: because it evaluated the category expression Associative "*".
| I.e. Given
|
| MyCat(f:Symbol):Category == with
| f:X->Y
|
| Why is 'f' in 'f:X->Y' replaced with "*" when I write:
|
| MyCat("*")
Because the category expression MyCat "*" is evaluated. Evaluating a
category expression means (among other things) replacing parameters by
their arguments. Just like when you evaluate a
function call, you expect that the actual arguments to be substituted
for the parameters.
| Wouldn't it be enough to treat 'f' in this context as a constant
| unrelated to the parameter 'f'?
Why should the 'f' in signature declaration in
MyCat(f:Symbol):Category == with
f:X->Y
should be unrelated to the f in the parameter list?
| Or do you think that this is just an accident of the design of the compiler?
I don't have enough evidence to select `accident' over `logical
consequence of the design'.
| >> It seems to me that
| >> the bug that prevents its full use in the "monoid problem" is not a
| >> fundamental design problem but rather something much more technical. I
| >> would greatly appreciate any suggestions you have about how to
| >> approach debugging this problem.
| >
| > My immediate question is how do you use it in practice? A monoid
| > operation comes with a neutral element. How do you use it?
|
| )abbrev category ID Identity
| ++ m(u,a)=a and m(a,u)=a
| Identity(u:Symbol,m:Symbol):Category == Commutative(m) with
| u: () -> % ++ unit
|
| -------
|
| In other words Identity implies the operation is commutative and has a
| unit. E.g.
|
| Identity("*","1")
|
| and
|
| Identity("+","0")
OK, thanks. Unlike others, I would refrain from making any premature
judgment (which would likely be unimprintable) and wait to see more of
this tested on the algebras. In particular, I would highly encourage
you to test this scheme on a modified version of the AXIOM algebras
(pick anyone you are comfortable with). I find it very effective to
test ideas on concrete problems to filter out which ones scale, which
don't, and what amendments are necessary.
| > Something I found very effective at testing proposals I've seen so far
| > is to construct all the usual algebraic structures up to Lie algebras
| > and use them in usual algorithms. That is a good test. Can you
| > test that?
| >
|
| Someday soon. :-)
I hope it is very soon :-)
-- Gaby
-------------------------------------------------------------------------
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
http://moblin-contest.org/redirect.php?banner_id=100&url=/
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
