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

[Ralf Hemmecke]

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

There is no guessing. If none of float, integer, string with an 
appropriate type is in scope, then throw an error.


>    2.  When one defines a category with default implementation, like 
>        Monad, the compiler extracts the "purely categorial" part of
>        Monad, e.g. the exports; then it implicitly creates a package
>        Monad& with an implicit parameter S of type Monad.  E.g., it is
>        as if the code was written:
>
>        )abbrev package MONAD- Monad&
>        Monad&(S: Monad): Public == Private where
>          Public ==> with
>            "**" : (S, PositiveInteger) -> S
>  
>          Private ==> add
>            import RepeatedSquare(S)
>            x ** n == expt(x, n)

Again, that is not the case for "default" in Aldor.

If you define yet another function inside "default {...}", then this 
belongs to the exports of the category although it is not declared as a 
signature.

define Foo: Category == with {
  default { foo(): () == {} }
}

exports

  foo: () -> ()

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

Ralf