"Bill Page" <[EMAIL PROTECTED]> writes:

| On Fri, May 16, 2008 at 9:10 AM, Gabriel Dos Reis wrote:
| >
| > Well, my understanding of your proposal was that in
| >
| >    if cond then
| >        x := 1
| >    else
| >        x := 2.3
| >    ...
| > the compiler would assign type Integer to `x' in the `then' branch,
| > and type Float  in the `else' branch, and type Union(Integer,Float) at
| > the meet point.
| 
| No. I think *you* suggested that as an option in an earlier email.
| That was not my idea.

My other suggestion (which I repeatedly said I was not proposing as
actual semantics, but only to point that the design space is large)
was a `real' overload of variables.  Not unions.

| > And from there on, the compiler should figure out things by
| > itself (as the interpreter does, as you showed in your
| > messages).
| 
| I think the interpreter does something quite different. Are you
| referring to this example that I included earlier?

Yes.

| 
| (1) -> x:Union(Integer,Float)
|                                                   Type: Void
| 
| (2) -> if 0<1 then x:=1 else x:=2.3
| 
|   (2)  1
|                                                   Type: Union(Integer,...)
| 
| (3) -> x := x*x
| 
|   (3)  1
|                                                   Type: Union(Integer,...)
| 
| (4) -> if 1<0 then x:=1 else x:=2.3
| 
|   (4)  2.3
|                                                  Type: Union(Float,...)
| 
| (5) -> x := x*x
| 
|   (5)  5.29
|                                                  Type: Union(Float,...)
| 
| ---------
| 
| Note that the type Union is declared up front (1) - not deduced by the
| Interpreter at the meet point.

OK.  An additional point, which was the objection from Ralf, was how
to select `*'.  You showed (and the above stills shows) that nothing
was need.  And I explained that nothing was needed because the
interpreter does a small step reduction and always keeps the most
accurate type.  Unlike the compiler.  My objection is based on how the
coercions are inserted -- note in the above, no manual coercion is 
inserted -- and partly on my understanding that your proposal required
the compiler to do a time travel when it hits the meet point.

| 
| The only (slightly) surprising thing here is (3) and (5) where the
| interpreter automatically selects the right * operation even though no
| * is exported by the Union. It seems to me that this is the *same*
| magic that you described as happens in the compiler when we write:

No, it is not the same `magic'.  The interprter does not really keep
track of control flow -- it just follows it, and when it needs the
type of a value, it looks up the most accurate type which is always
stored along with the value in the interpreter environement.

The compiler on the other hand, does not keep the most accurate type.
So, what it does is to follow the control flow and constantly updating
the set of assumptions on a particular variable.

| 
|    if x case Integer then x:=x*x
|    else x:=x*x
| 
| It is just that the interpreter is able to divide these cases automatically.

It is more than it meets eyes.  The mechanism are completely
different.  Think that the interpreter stores a value along with its
type.  The compiler does not do that with variables.  Notice that, if
you design a domain that defines its own case operation without having
a corresponding autoCoerce, the compiler will reject the construct.

| > That, I think is not a minor modification.  The reason is
| > that in the `then' branch, the `x' has a specific type that does not
| > require coercion to obtain its value, whereas from the meet point, the
| > compiler has to `go back' to `fix up' the type of `x', and figured out
| > what to do business afterward.  Prompting the question from Ralf.
| >
| > If your proposal is: well, just manually declare x of type Union
| > before the `if', then there is nothing new; we already have that
| > in current Spad (and that is not going to change).
| 
| Yes, exactly!

OK, if you push that on the programmer, I have nothing to say and I
withdraw my observations.  But, if you push it on the compiler, I
would have to understand why and how it works :-)

| > In fact, it is completely orthogonal -- whether the `if'-branches
| > have their own scopes or not, that is going to work, just like
| > it works today.
| >
| 
| My point is only that *if* 'if'-branches acquire there own scopes,
| then manually declaring x to be of type Union is unavoidable (baring
| overloaded variable names). It is just a variant of the same solution
| applied to the 'for'-loop scope.

OK.

| > Bill Page writes:
| > | I do not agree that I am "manually
| > | inserting" the right coercion. Based on your explain below, it
| > | is clear that I could/should have written:
| > |
| > |      x case Integer => x*x
| >       ^^^^^^^^^^^^^^^^^^^^^^
| >
| > This is what I call manual insertion of right coercion -- not just
| > the fact that you wrote `::Integer' at the end of `x*x'.  Because
| > you're manually selecting which branch does what.  See the explanation
| > of `autoCoerce'. In contrast to what you did with the interpreter.
| 
| Well, in the compiler I am not really manually selecting anything
| since the same code occurs in both branches of the 'if' statement, but

The `case' constructs does that.  If you have an OpenAxiom compiler,
write a domain that defined its own `case' operator without defining
corresponding `autoCoerce' operator, and try the same thing.

| this has the effect of "dividing that cases", so that the compiler can
| apply it's usual coercion rules. I believe that this is also what is
| done automatically in the interpreter and it could also be automatic
| in the compiler.

The interpreter does something different:  It goes and ask the
object: `hey which branch are you in?'.  The compiler needs a target
and tries all possible coercisions that could work.

[...]

| > | I admit that it is helping the compiler a little more than one might
| > | like.
| >
| > It is more than helping the compiler: You're telling it what to do;
| > unlike the interpreter.
| 
| I did not tell it how to interpret
| 
|    x:=x*x
| 
| I just wrote this same expression in two different contexts.

Once you have manually exhausted the n-1 cases, the last is automatically
picked up by the inverse environement computation algorithm.  But, if you
have not gone through the n-1 cases, it would not work.  See the
example I posted earlier. 


| 
| > |
| > | > If you're going to manually insert the right coercions, you may just
| > | > as well declare the variable explicitly as being a Union.
| > | >
| > |
| > | I was suggesting exactly that: If you want x to be known outside the
| > | scope if the 'if' statement then you should be forced to explicitly
| > | declare it as a Union - just like the case you described with the
| > | 'for' loop:
| > |
| > |     x:Integer
| > |     for i in 1..10 repeat
| > |         x:=i
| > |     x
| >
| > OK, my understanding of your suggestion was different; see above.
| > But, if it is the case that the programmer -- not the compiler --
| > has to do the manual declaration as Union, and manual insertion
| > of coercion, I don't see anything wrong about it:  It is what we are
| > doing today.
| 
| No. Today there is a semantic error.

We must either test different compilers, or different examples.  Could
you remind me of which compiler and which example?

-- Gaby

-------------------------------------------------------------------------
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

Reply via email to