Re: [Axiom-developer] "has" and "with" (was curious algebra failure)

[Gabriel Dos Reis]

On Mon, 13 Aug 2007, Ralf Hemmecke wrote:

| >     1.  When a function is called, the compiler/interpreter determines
| >         whether the arguments used to call the function are coercible
| >         to the type of the formal parameters of the function, when it
| >         was declared.
| > 
| >        What that means concretely is that when we declare a function
| >        like
| > 
| >          foo: Double -> Double
| > 
| > 
| >        and we attempt foo(4), the compiler/interperter does not start
| >        looking whether the value 4 "has" sin, cos, and many operations that
| >        hold for Doubles.  Rather, it determins whether the value
| >        4 can be converted the type Double, if yes, it applies that
| >        conversion and generate call to foo() with the result of the
| >        of the conversion as argument.
| > 
| >        That looks intuitive enough.  And I suspect we all agree.
| 
| In Aldor that is different. When the compiler sees 4 that is just something of
| type Literal. If it sees foo(4) and foo: Double->Double is the only foo in
| scope, the compiler tries to match the type of 4 with Double. The only thing
| it is allowed to do is to call a function that converts 4 to Double, i.e. a
| function
| 
|   Literal -> Double
| 
| Now in Aldor there are several functions of this kind.
| 
|   float:   Literal -> %
|   integer: Literal -> %
|   string:  Liteal -> %
| 
| Double might actually export and implement the first two of them.
| And the rules are simple for the compiler.
| 
| If a literal looks like a string, i.e. of the form "...", then apply "string".
| If a literal looks like a float, then apply "float".
| If a literal looks like an integer, then apply "integer".

maybe the use of the literal 4 was a distraction from the main topic.  

What I way saying is that when the compiler sees a call to foo
with an expression of type integer, and foo is the only one in scope...

[...]

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

| But that should be found out by
| taking the exports of S (which happens to be Monad). Then the compiler should
| check whether Monad exports SetCategory and *:(%,%)->% (which is what S in
| RepeatedSquaring requires). If that is fulfilled then everything is fine. No
| coercion necessary.

That is a another model of translation; I'm sure it is uniform in the sense
that it treats value expression and domain expression in the same way.


Please, note I'm not being argumentative.  I'm trying to understand
all perspective -- that is why I would like to understand the "obviousness"
of each point of view.  I underdstand the coercion well enough and  I believe
I can prove that that system is sound.

-- Gaby