On Wed, May 14, 2008 at 7:54 PM, Waldek Hebisch <[EMAIL PROTECTED]> wrote: > > 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.
Yes and No. No, because for exported operations, a different environment is modified, e.g. different rules are used. See the definition of of put() and get(). The fact that the same code is used is not fundamental semantics -- just an implementation convenience. If they wanted the code to be legal they would have attached differentiator (e.g. predicates); but they explicitly took steps to check that the modes were the same, with an error in case of violation. > 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). Well the difference is fundamental, because for exported operations, what counts is the modemap and they do consistently use different rules. Note also that conditional definition of local functions is not supported at all (see other past threads about duplicate definitions generated by the compiler). > > > > > | 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. Well, `does not work well with implicit declarations; is vague. I gave a rule that works 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. Yes, that there is no problem there: the condition covers both branches. In fact Spad is not the only language doing that. If I recal correctly, that feature goes back to Algol 68. C++ has it too. > So many constructs can not create new scope. I'm sorry that does not follow. > For consistency, it is reasonable to have very short > list of constructs which create new scope. I'm not sure `very short list' follow from is a necessary or sufficient condition for `consistency'. They are orthogonal. And in fact, we don't have many constructs that introduces new scopes. > > 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. Many people believe that the two-level languages of Axiom is a strength: one for library development, and one for interpreter. Large scale programming (libraries) tend to impose different requirements than small scale programming (interactive uses). There are different ways to achieve that: One can make the language separate but close (as all Axiom flavours currently do), or one can make the interactive language a subset of the library language (as many Haskell implementations do). Both approaches have their pros and cons. > > > > 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... I would like to see a mode detailed an elaboration of that rule, along with how overload resolution should proceed. Note: this is not a suggestion that the rule will not work, rather, I would like to see the rule elaborated so that I can compare where it leads to simpler language for interactive users and library users. > > 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... Probably. But, they also decided that a variable and a local function must have at most one mode. > > > > | 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. For sure, they wanted small functions (many design aspects support that). However, I don't how the second sentence follows.. (there are clearly many functions in the algebra that violate the `simple function definition' principle.) > > > > 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. yes, otherwise, I would not sent out messages to collect different views. There are two issues at play: abstract semantics and implementation details. I always try to focuse on the former, and give the second weight only if the consequences are two high from an implementation point of view. I do not consider sharing the same code for exported and non-export definitions essential (the current compilers already use different rules in many places). ------------------------------------------------------------------------- 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
