On 08/16/2007 02:18 PM, Gabriel Dos Reis wrote:
On Thu, 16 Aug 2007, Ralf Hemmecke wrote:
| % as the argument of RepeatedSquaring stands for a domain of type Monad().
| Such a domain obviously satisfies
|
| SetCategory with {*: (%,%)->%}
|
| since Monad() has these exports (and more in the Axiom library case).
Please be more precise about "satisfies". What does it mean?
That was written above. So let me repeat:
Monad() (in Axiom) exports the symbols
(*1*)
Monad
SetCategory
*: (%,%)->%
rightPower: (%,PositiveInteger) -> %
leftPower: (%,PositiveInteger) -> %
**: (%,PositiveInteger) -> %
The requirements of the argument of RepeatedSquaring are
(*2*)
SetCategory
*:(%,%)->%
Now "
Monad
satisfies
SetCategory with *:(%,%)->%
means that the (*1*) is a superset of (*2*).
Quote from AUG Section 7.7 "Type satisfaction" (p.83).
We say that a type S satisfies the type T if any value of type S
can be used in any context which requires a value of type T.
For example Integer is a value of type Monad (I hope). Integer (or any
other domain of type Monad) can be used in a place where (*2*) is
required. Why do I need coercion here? It's just a check that the
exports of a certain domain are a superset of the required exports.
I understand what it means it terms of "has".
That is SPAD compiler biased. ;-)
[...]
| Gaby, you have given in
|
| http://lists.nongnu.org/archive/html/axiom-developer/2007-08/msg00412.html
|
| how the "add" part in the Monad definition is translated to a private domain.
In fact, there is no nothing private about it. The rewrite is available
to user.
| That looks perfectly fine to me.
| Bill has already shown that a proper value for the argument of
| RepeatedSquaring as in
|
| http://wiki.axiom-developer.org/SandBoxMonad
|
| works fine.
|
| Gaby, you write there:
|
| Now the compiler goes on typecheking the defnition x ** n.
| It sees the use of expt() and find out that the only expt() in
| scope if the one from RepeatedSquare(S). Then it tries
| to instantiate that package -- just like a function call.
| From there, it applies the usual rules: Can I coerce S of
| type Monad to the expected argument type of RepeatedSquare()?
| They answer comes out as "no". Hence the error.
|
| Why would the compiler want to "coerce" if all that is needed is to check
| whether S of type Monad has at least the exports that are required by the
| argument type of RepeatedSquaring.
The compiler is doing that because it treats function calls -- either
to produce a value of a type -- uniformly. It seems to me that you're
arguing two non-uniform rules: one for value, and one for types. Is that
correct?
Hmmm, I would say, I don't completely understand all that, but I tend to
say "yes".
You cannot achieve that uniformity. Take
define Cat: Category == with;
define Foo(T: Cat): Category == with {};
DomI: Foo(Integer) == add;
DomS: Foo(String) == add;
b1: Boolean == DomI has Foo(Integer);
b2: Boolean == DomI has Foo(String);
b3: Boolean == DomS has Foo(Integer);
b4: Boolean == DomI has Foo(String);
If you treat domain constructors in the same way as basic values
(functions) then
Foo(Integer) = Foo(String) = with {}
So b1, ..., b4 should all be true, right? But I remember faintly that
you argued about a functional language with respect to the types and
that you would like to be able to distinguish
Foo(Integer) from Foo(String)
No? Where would be the uniformity here?
Ralf
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
http://lists.nongnu.org/mailman/listinfo/axiom-developer
