Gabriel Dos Reis wrote:
> Waldek Hebisch <[EMAIL PROTECTED]> writes:
>
> | Gabriel Dos Reis wrote:
> | >
> | > The definition of the function recip$NormalizationPackage elicites
> | > a `semantic error' from the compiler because the local variable
> | > `hesrg' is defined in the two branches of an if-statement with two
> | > differen types. That looks like a bug to me. Opinion?
> | >
> | > recip(p:P,ts:TS): Record(num:P, den:P) ==
> | > -- ASSUME p is invertible w.r.t. ts
> | > -- ASSUME mvar(p) is algebraic w.r.t. ts
> | > v := mvar(p)
> | > ts_v := select(ts,v)::P
> | > if mdeg(p) < mdeg(ts_v)
> | > then
> | > hesrg: Record (gcd : P, coef2 : P) :=
> halfExtendedSubResultantGcd2(ts_v,p)$P
> | > d: P := hesrg.gcd; n: P := hesrg.coef2
> | > else
> | > hesrg: Record (gcd : P, coef1 : P) :=
> halfExtendedSubResultantGcd1(p,ts_v)$P
> | > d: P := hesrg.gcd; n: P := hesrg.coef1
> | > g := gcd(n,d)
> | > (n, d) := ((n exquo g)::P, (d exquo g)::P)
> | > remn, remd: Record(rnum:R,polnum:P,den:R)
> | > remn := remainder(n,ts); remd := remainder(d,ts)
> | > cn := remn.rnum; pn := remn.polnum; dn := remn.den
> | > cd := remd.rnum; pd := remd.polnum; dp := remd.den
> | > k: K := (cn / cd) * (dp / dn)
> | > pn := removeZero(pn,ts)
> | > pd := removeZero(pd,ts)
> | > [numer(k) * pn, denom(k) * pd]$Record(num:P, den:P)
> | >
> | >
> |
> | I belive that Axiom creators considered this function legal,
> | so generating error message would be a bug.
>
> Hmm, could you give me hints at to why they considered the function legal?
Note that the same code handles conditional definitions
and normal 'if' statements. I think that this is not an
accident, but that Axiom creators wanted to have the same
semantics for both. For conditional definitions clearly we
want (predicated) union of modes. There is a difference:
the function above defines variables, but IMHO here this
difference is not essential (see below).
> | OTOH I am not
> | sure if I want this function to be legal. The function
> | captures important pattern where in in both branches of
> | conditional computation is almost the same, but one has to use
> | different types. One can use different variable names
> | in both branches, but it also makes sense to use the same
> | name to stress similarity.
>
> The are two separate but losely related issues:
> (1) What should be the content of the meet of both branches?
> (2) Should if-statement have their own scopes?
>
> In the current semantics, branches of if-statements do not have their
> own scopes, so the meet environment of an if-statement is the union
> of environment of both branches. And this is where the error comes
> in: One cannot declared the same variable in the same environment
> with different modes.
> One way is to say that each branch has its own scope, of the
> if-statement would be OK, but will have a completely different meaning
> from the one intended -- and the functions would be an error because
> hesrg will not be visible after the meet point.
I think that _if_ you require explicit declarations, than
giving each 'if' branch explict scope is natural. But,
as Stephen Watt pointed out, such tight scope does not
work well with implicit declarations. More precisely,
treating 'if' branch as new scope may work. But
Spad is an imperative expression oriented language,
which means that variables may be created in the middle
of expressions and conditionals may be part of
expression. So many constructs can not create new scope.
For consistency, it is reasonable to have very short
list of constructs which create new scope.
Note: personally I do not like namespace pollution and I would
like to have compiler mode (switch) which disables
implicit declarations. But I would like to have single
language and tight rules may be too hard for interactive
users.
> Another way is saying that the meet contains common variables (with
> coherent modes); in that case he program will be an error because at
> the meet point, the variable will have two modes (a bit like today).
> This option can have its benefit, but I'm not sure it is one that I'm
> comfortable with.
>
Different modes for variable may cause problems. But in the function
above variable is assigned only once and is unused outside of 'if'
statement. So formally there is no problem with overloading:
we may have two different modes, each with its own condition.
Of course, in general deciding which mode to use may be tricky, but
here is trivial, since the variable is unused after meet...
Note: I am _not_ comfortable with the argument above -- I prefer
to have very clear and simple semantics for core constructs
and to make illegal problematic things. But I supect that
Axiom creators may have use such arguments...
> | So I see some benefits of original design.
>
> The original design produces an error on the construct.
> The only reason we don't usually see it is that there is a bug in the
> compiler (all Axiom flavours) where the compiler fails not to produce
> a .o -- when it actually says so.
>
> | But making
> | this function illegal would make Spad closer to conventional
> | languages which has its own advantages.
>
>
> >From my perspective, it is less a desire to be close to conventional
> languages, than having a clear well-though of semantics that support
> modularity. I tend to have a preference for localization because,
> localization plays well with modularization.
>
1) My impression is that original design expected (and wanted) small
functions. Then only modularity above function level plays role,
and extra scopes inside functions play little role.
> When you say making the function illegal, do you think it is because
> you think the declaration from both branches should be exported to the
> enclosing scope?
>
As you noted, there are at least two ways to make it illegal. ATM
I do not have strong opinion about this function -- when choosing
rules I prefer to look at other consequences and in this case
just accept what to rules will say.
--
Waldek Hebisch
[EMAIL PROTECTED]
-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
