[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Axiomdeveloper] "has" and "with"
From: 
Ralf Hemmecke 
Subject: 
Re: [Axiomdeveloper] "has" and "with" 
Date: 
Thu, 16 Aug 2007 12:17:33 +0200 
Useragent: 
Thunderbird 2.0.0.6 (X11/20070728) 
 > 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.

 Well, of course the answer should be "yes".
It is not clear to me why the answer should *of course" be "yes".
We have
RepeatedSquaring(S): Exports == Implementation where
S: SetCategory with
"*":(%,%)>%
Exports == with
expt: (S,PositiveInteger) > S
Implementation == add ...
and furthermore
Monad(): Category == SetCategory with
"*": (%,%) > %
...
add
import RepeatedSquaring(%)
x:% ** n:PositiveInteger == expt(x,n)
rightPower(a,n) == ...
leftPower(a,n) == ...
This should behave approximately like
BEGIN aaa.as
#include "aldor"
macro SetCategory == PrimitiveType;
RepeatedSquaring(S: SetCategory with {*: (%,%)>%}): with {
expt: (S, Integer) > S;
} == add {
expt(s: S, i: Integer): S == s;  dummy implementation
}
Monad(): Category == SetCategory with {
*: (%,%) > %;
default {
#if DoesntWork
import from RepeatedSquaring(%);
(x:%) ** (n:Integer): % == expt(x,n);
#else
(x:%) ** (n:Integer): % == expt(x,n)$RepeatedSquaring(%);
#endif
}
}
END aaa.as
woodpecker:~/scratch>aldor laldor aaa.as
woodpecker:~/scratch>aldor laldor DDoesntWork aaa.as
"aaa.as", line 14: (x:%) ** (n:Integer): % == expt(x,n);
...................................^
[L14 C36] #1 (Error) There are no suitable meanings for the operator `expt'.
Well. In fact, I would have liked that the Aldor compiler also works for
the second case. Clearly "expt: (%, Integer) > %" is in scope since it
was just imported via the import statement. I consider that a bug in the
Aldor compiler.
% 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).
The compiler should check whether the type of % exports SetCategory. Yes
it does, since Monad() exports it.
The compiler should check whether the type of % exports
*: (%,%)>%
. Yes it does, since Monad() exports it.
Now why I believe that the SPAD compiler returns "false" is the following.
SPAD does not have "default". Implementations of a category are
implemented by a private domain (therefore the "add" instead of
"default" in SPAD). Now if I take the definition of the AUG about what
the type of "add {...}" is, then, of course the % in RepeatedSquaring of
add
import RepeatedSquaring(%)
x:% ** n:PositiveInteger == expt(x,n)
rightPower(a,n) == ...
leftPower(a,n) == ...
(see naalgc.spad.pamphlet)
does *not* export
*: (%,%)>%
and therefore the instantiation of RepeatedSquaring(%) must fail.
Gaby, you have given in
http://lists.nongnu.org/archive/html/axiomdeveloper/200708/msg00412.html
how the "add" part in the Monad definition is translated to a private
domain. That looks perfectly fine to me.
Bill has already shown that a proper value for the argument of
RepeatedSquaring as in
http://wiki.axiomdeveloper.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. (And it has.) I don't see a
need for coercion at all.
Ralf
 Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure), (continued)
 Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure), Ralf Hemmecke, 2007/08/13
 [Axiomdeveloper] "has" and "with" and bug, Ralf Hemmecke, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with" and bug, William Sit, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with" and bug, Ralf Hemmecke, 2007/08/13
 [Axiomdeveloper] Re: "has" and "with" and bug, Gabriel Dos Reis, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure), Bill Page, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure), Ralf Hemmecke, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with" (was curious algebra failure), Gabriel Dos Reis, 2007/08/13
 Re: [Axiomdeveloper] "has" and "with",
Ralf Hemmecke <=
 Re: [Axiomdeveloper] "has" and "with", Gabriel Dos Reis, 2007/08/16
 Re: [Axiomdeveloper] "has" and "with", Ralf Hemmecke, 2007/08/16
 Re: [Axiomdeveloper] "has" and "with", Gabriel Dos Reis, 2007/08/16
 Re: [Axiomdeveloper] "has" and "with", Ralf Hemmecke, 2007/08/16
 Re: [Axiomdeveloper] "has" and "with", Gabriel Dos Reis, 2007/08/16
 Re: [Axiomdeveloper] "has" and "with", Ralf Hemmecke, 2007/08/16
 Re: [Axiomdeveloper] "has" and "with", Gabriel Dos Reis, 2007/08/16
 Re: [Axiomdeveloper] "has" and "with", Ralf Hemmecke, 2007/08/16
 Re: [Axiomdeveloper] "has" and "with", Gabriel Dos Reis, 2007/08/16
 Message not available
 Re: [Axiomdeveloper] "has" and "with", Gabriel Dos Reis, 2007/08/16