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

[Bill Page]

On 8/13/07, Ralf Hemmecke wrote:
> > The Spad compiler tries to treat category constructors, domain
> > constructors, package constructors, and function calls as uniformly as
> > possible.  What I mean by that is that it applies the principle:
> >
> >    When calling a function, collect candidates, filter them by
> >    applying the criteria that the arguments match the parameter types.
> >    And select the best match if possible.
>
> Oh, I hope that will change. The compiler should *never* have a choice
> left. Either after filtering there remains *exactly* one possibility or
> the compiler should complain.
>

I agree. Certainly that is what the Aldor compiler does.

> > And that irrespective of whether the arguments are value expressions
> > or domain expressions.
>
> > By "matching" here, I don't necessarily mean only `pattern matching'.
> > Rather I mean `coercible'.  For example an expression of type Integer
> > is coercible to Float because Float exports the following function
> >
> >      coerce : Integer -> %
>
> That is exactly what Aldor does *not* do. It never applies "coerce" if
> one doesn't explicitly call for it. At the moment I find Aldor much
> better in this respect. You should consider that some people might
> implement a function that is not a nice "coerce" (although their
> function carries this name).
>

I agree. I think Spad tries much to hard to do coercions. It does not
try as hard as the Axiom interpreter but still it is possible for Spad
to automatically do things that are quite unexpected for the
programmer and sometimes invisibly wrong. This is one more reason why
I prefer to write "Spad" code first in Aldor and then back port it to
Spad.

> Just suppose in the context where there is an integer that must be
> coerced into something of MyDomain. I have written a possible coercion
> function in MyDomain that could be used for that task by the SPAD
> compiler. But what I actually want was to call another function. I had
> just forgotten to write it into the source code. Then the compiler
> happily inserts "coerce" and I don't see (don't get a warning) that my
> code is actually not as I wanted it to be. Yes it means more typing, but
> that is not a big burden if you see from the code what is happening.
>
> > Similarly, an expression of type PositiveInteger is coercible to
> > Integer bcause PositiveInteger is a subdomain of Integer.  Similarly,
> > a domain expression of type C1 is coercible to C2 if C2 appears
> > in the list of named categories extended by C1.
> >
> > The exact rules are implemented by the function coerce() defined in
> > compiler.boot.  They are split into three categories:
> >
> >   (1) easy coercion -- ceorceEasy
> >   (2) subset coercion -- coerceSubset
> >   (3) hard coercion -- coerceHard

I think coercions from subdomain to domain and from subcategory to
category (presumably (2) above) are of a different kind than coercions
provided by the programmer. These are guaranteed to be correct by the
nature of what we mean by these subtypes. That is why we need the
concept of subdomain to be be "builtin" to the language instead of
pasted on externally via an exported coerce operation.

> Remember that in Axiom you can coerce anything to anything. Just write a
> function "coerce" with the corresponding types. So if I add a function
>
>    coerce: Float -> Integer
>
> probably a lot will go wrong and nobody will easily find the error if
> the compiler does not give an error or at least warn.
>
> I understand that the idea of automatic coercion is a good one at an
> interactive level, but at the library I don't want to have it.
>

I think what we need at the library level is support for coercions
that are a natural consequence of the way we define the types, e.g.
via subtypes. There are also several other similar types of coercions
that arise because of the universal categorical properties of types
like Cross, Record and Union. In the AUG these are referred to as
"courtesy conversions" but I think their presence is more a matter of
necessity than convenience.

> I am quite interested how other people feel about automatic coercion.
> (You should read Doye's thesis before you answer.
> http://portal.axiom-developer.org/refs/articles/doye-aldor-phd.pdf)
>
> If these coercion paths are always unique then I am certainly for it,
> but I somehow think that there is still a lot of research to be done on it.
>

I think that is especially true at the level of the Axiom interpreter.
Here the automatic coercions are one of the things that most violates
the "principle of least surprise" for new users. At the level of Spad
(and Aldor) programming however, I think these things can and should
be defined more carefully and in the most expressive manner possible
that is consistent with an underlying categorical semantics.

Regards,
Bill Page.