[Axiom-developer] "has" and "with" and bug

[Ralf Hemmecke]

> > > I'm saying that the parameter S of the default package
> > > Monad& -- generated for the default implementation of the
> > > category Monad -- is of the named category Monad.

Sorry, I am too lazy to go back where all began. But let me quote that 
piece of code here.

Monad(): Category == SetCategory with
      "*": (%,%) -> %
      "**": (%,PositiveInteger) -> %
      ...
    add
      import RepeatedSquaring(%)
      x:% ** n:PositiveInteger == expt(x,n)
      ...

RepeatedSquaring(S): Exports == Implementation where
   S: SetCategory with "*":(%,%)->%
   Exports == with
     expt: (S,PositiveInteger) -> S
   Implementation == add ...

First. % in RepeatedSquaring(%) can in general not be Monad.
Why? One should be able to pass the "add" part alone as an anonymous 
domain to a function.

AUG Chp. 8.10:

  An add expression also introduces a binding for the constant %, which
  is a reference to the domain formed by the add expression.

So let's do something in Aldor. "add" has to be replaced by "default", 
but this way it does not demonstrate what I wanted to show.

Let's compile and run the program below.

woodpecker:~/scratch>aldor -laldor -grun aaa.as
has with {foo: ()->()} = T
has with {bar: ()->()} = T
has with {rhx: ()->()} = T
has with {foo: ()->()} = T
has with {bar: ()->()} = T
has with {rhx: ()->()} = T
MDom has rhx? T

Ooops. I must say that is surprising. MDom exports foo, bar, ans, but 
not rhx.

So my preferred output would have been:
has with {foo: ()->()} = T
has with {bar: ()->()} = T
has with {rhx: ()->()} = T
has with {foo: ()->()} = T
has with {bar: ()->()} = T
has with {rhx: ()->()} = F
MDom has rhx? F

blahrhx()$Blah(%) should give T, because (I believe) the whole add part 
is passed to Blah and that is an anonymous domain with exports

                                                                 (*)
  foo: ()->()
  bar: ()->()
  rhx: ()->()
  ans: (...)->()

AUG Chp. 7.8:

  The type of the expression A add B is C with { x1: T1; ...; xn: Tn }
  where C is the type of A, and x1,...,xn are the symbols defined
  (using ==) in B, whose types are T1,...,Tn, respectively.

So that is another place where the Aldor compiler does not behave 
according to specification.

Also try to copy the add part of MDom and pass it as an anonymous domain 
argument to ans$MDom. That does not compile, since for some reason the 
compiler thinks that the type of that "add {...}" thing is Type instead 
of the category with exports given in (*).

In general, (as Bill already pointed out), "has" tests for "subcategory".

As a function "has" is of type

  has: (Type, Category) -> Boolean

where the first argument is actually restricted to domains/packages.
See AUG.pdf page 96 "Has expressions".

In Aldor you cannot say

  Monoid has with {1: %}

since Monoid is of type Category (though also of type Type).

----------------------------------------------------------------------
aldor -gloop
%1 >> #include "aldor"
%2 >> #include "aldorinterp"
%3 >> PrimitiveType
  () @ Category ==  with
        =: (%, %) -> Boolean
        ~=: (%, %) -> Boolean
        default ((a: %) ~= (b: %)): Boolean == ..
                                           Comp: 0 msec, Interp: 0 msec
%4 >> PrimitiveType has with {=:(%,%)->Boolean}
      ^
[L14 C1] #1 (Error) No meaning for identifier `PrimitiveType'.
%5 >> #quit
-----------------------------------------------------------------------------

Gaby, if you implement those stuff in SPAD, please don't apply some 
automatic coercion. This whole stuff is about type satisfaction.
I am sure you know about AUG.pdf Chp. 7.5 "Subtypes", Chp. 7.7 "Type 
satisfaction".

All the best

Ralf



---BEGIN aaa.as
#include "aldor"
#include "aldorio"

Blah(S: with {foo:()->()}): with {
    blahfoo: ()->Boolean;
    blahbar: ()->Boolean;
    blahrhx: ()->Boolean;
} == add {
  blahfoo(): Boolean == S has with {foo: ()->()};
  blahbar(): Boolean == S has with {bar: ()->()};
  blahrhx(): Boolean == S has with {rhx: ()->()};
}

MMM: Category == with {
  foo: () -> ();
  bar: () -> ();
}

MDom: MMM with {
  ans: (with {foo:()->(); bar:()->()}) -> ();
} == add {
  foo(): () == {
    stdout << "has with {foo: ()->()} = " << blahfoo()$Blah(%) << newline;
    stdout << "has with {bar: ()->()} = " << blahbar()$Blah(%) << newline;
    stdout << "has with {rhx: ()->()} = " << blahrhx()$Blah(%) << newline;
  }
  bar(): () == {}
  rhx(): () == {}
  ans(S: with {foo:()->(); bar: ()->()}): () == {
    stdout << "has with {foo: ()->()} = " << blahfoo()$Blah(S) << newline;
    stdout << "has with {bar: ()->()} = " << blahbar()$Blah(S) << newline;
    stdout << "has with {rhx: ()->()} = " << blahrhx()$Blah(S) << newline;
  }
}

main(): () == {
  foo()$MDom;
  ans(MDom)$MDom;
  stdout << "MDom has rhx? " << (MDom has with {rhx: ()->()}) << newline;
}
main();
---END aaa.as