[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiom-developer] "has" and "with"
From: |
Gabriel Dos Reis |
Subject: |
Re: [Axiom-developer] "has" and "with" |
Date: |
Thu, 16 Aug 2007 10:48:03 -0500 (CDT) |
On Thu, 16 Aug 2007, Ralf Hemmecke wrote:
| > Whether those those two categories are equal in the sense that
| > "=" returns true is entirely a matter semantics attached to
| > the "with"-construct. There is no predefined choice.
|
| Yes, I understand and agree. I don't even remember that I have seen clearly
| that I have seen a statement in the AUG that says that
|
| with {}
|
| and
|
| with {}
|
| would necessarily two identical or non-identical things. Maybe that should be
| considered a bug in the documentation.
|
| And that Foo(Integer) is different from Foo(String) but equal to Foo(Integer)
| you can only assure if the language restricted to types is functional.
Hmm; I'm lost. Could you elaborate on the last paragraph?
| We all know that one could define
|
| define Bar(i: Integer): Category == with;
|
| and here I am no longer sure whether Bar(0) is really treated differently (by
| the current aldor compiler) from Bar(1) in a "has" construct. I'd like to have
| the same behaviour as for type-valued arguments, but maybe there is some good
| reason why the Aldor compiler behaves different for non-type-valued arguments.
| There must be some examples on this list, I just don't know how I can find
| them now.
In any cas,e it would be nice to have those examples, and the logical
inference rules that go with them put somewhere for future reference.
[...]
| > | So my guess was that they should be treated in the same way.
|
| > Well, ne need rules to define equality on objects we manipulate
| > in programs. Every definition has its consequences -- pros and cons.
|
| Good. Where should these pros and cons go to? Any suggestion for a
| documentation. MathAction?
I believe MathAction is a good place to start.
(But, I tend to leave on emails...)
| > In the field of type theory, the notion of equality on types (and modules)
| > is a fertile area of research that has been going on for ages.
| > Search for "manifest types" and "generative types". Youcan replace
| > "type" by "modules".
|
| Thank you. I'll do my homework.
|
| > My point of view is this: I believe the idea of treating category,
| > domain, and packages instantiation as function call is a good uniform rule.
| > I also believe that we should further uniformity by
| > having only one set of rules for function calls -- e.g. we don't
| > have one rule for values, one for types, and one for whatever.
|
| If that can be done, I am all for it.
|
| > Notice that, in that view, the notion of value equality is not involved.
|
| Hmmm, but doesn't that mean that whether baz(0) is equal or not equal to
| baz(1) has nothing to do with the implementation of "=" in Integer? That
| sounds a bit strange to me. What are contexts (examples) where =$Integer would
| not be needed?
Well, there are two things here:
* evaluating the expressions "baz(0)", "baz(1)", "baz(x)" where x is
a variable
* evaluating the expression "baz(0) = "baz(1)"
what I'm saying is that in the evaluation of the function calls baz(1),
baz(0), baz(x), I don't see where the definition of =$Integer is involved.
Nor, am I sure it should be involved -- utimately we would like
=$Integer to be a function itself that can be called...
-- Gaby
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), (continued)
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
- Re: [Axiom-developer] "has" and "with", Ralf Hemmecke, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Gabriel Dos Reis, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Ralf Hemmecke, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Gabriel Dos Reis, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Ralf Hemmecke, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Gabriel Dos Reis, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Ralf Hemmecke, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Gabriel Dos Reis, 2007/08/16
- Re: [Axiom-developer] "has" and "with", Ralf Hemmecke, 2007/08/16
- Re: [Axiom-developer] "has" and "with",
Gabriel Dos Reis <=
- Message not available
- Re: [Axiom-developer] "has" and "with", Gabriel Dos Reis, 2007/08/16
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), William Sit, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Bill Page, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
- Re: [Axiom-developer] "has" and "with" (was curious algebra failure), Ralf Hemmecke, 2007/08/13
- Re: [Aldor-l] [Axiom-developer] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
- Re: [Aldor-l] [Axiom-developer] "has" and "with" (was curious algebra failure), Ralf Hemmecke, 2007/08/13
- RE: [Aldor-l] [Axiom-developer] "has" and "with" (was curious algebrafailure), Weiss, Juergen, 2007/08/13