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

[Gabriel Dos Reis]

Ralf Hemmecke <address@hidden> writes:

| > | Isn't the problem whether 'Monad has SetCategory with "*":(%,%)->%' ?
| 
| > If the question is formulated in terms of "has", then I think the answer
| > is unambiguously "yes".
| 
| Gaby, if you are going to implement "yes", then we should keep in mind 
| that the Aldor compiler currently does not allow categories as the first 
| argument of "has" and the AUG.pdf p.96 "Has expressions" is clear about 
| this.


Hi,

  Thanks for all who are looking tinto this with me.
I just woke up, going through mails.  I'll be trying to answer
what I believe the easy parts first, then get into the deeper ones at
the end.  Please bear with me.

  
Ralf --

  For the moment, I'm not implementing any new functionality.  I'm
just trying to collect the rules as used at the moment, checking with
all of you here to see whether they match your understanding as well.

[...]

| > It seems to me that the compiler asks the question in terms of coercible,
| > instead of "has".
| 
| Oh, that would surprise me even in SPAD. Where should the "coerce" 
| function come from?

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.

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

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 attached to this message the gzipped trace of coerceEasy,
coerceSubset and coerceHard when compiling "**" for Monad&.
All three functions are called with two arguments

  a. a triplet for the current expression,
  b. the target mode.

A triplet for an expression e is:

     (i) the expression e
    (ii) the assumed mode m of e
   (iii) the environment in which e is assumed to have mode m

-- Gaby

coerce-trace.txt.gz
Description: GNU Zip compressed data