Re: [Axiom-developer] "has" and "with"

[Ralf Hemmecke]

On 08/16/2007 02:18 PM, Gabriel Dos Reis wrote:
> On Thu, 16 Aug 2007, Ralf Hemmecke wrote:
>
> | % as the argument of RepeatedSquaring stands for a domain of type Monad().
> | Such a domain obviously satisfies
> | 
> |   SetCategory with {*: (%,%)->%}
> | 
> | since Monad() has these exports (and more in the Axiom library case).
>
> Please be more precise about "satisfies".  What does it mean?

That was written above. So let me repeat:

Monad() (in Axiom) exports the symbols

(*1*)

  Monad
  SetCategory
  *: (%,%)->%
  rightPower: (%,PositiveInteger) -> %
  leftPower: (%,PositiveInteger) -> %
  **: (%,PositiveInteger) -> %

The requirements of the argument of RepeatedSquaring are

(*2*)

   SetCategory
   *:(%,%)->%

Now "

  Monad
  satisfies
  SetCategory with *:(%,%)->%

means that the (*1*) is a superset of (*2*).

Quote from AUG Section 7.7 "Type satisfaction" (p.83).

  We say that a type S satisfies the type T if any value of type S
  can be used in any context which requires a value of type T.

For example Integer is a value of type Monad (I hope). Integer (or any 
other domain of type Monad) can be used in a place where (*2*) is 
required. Why do I need coercion here? It's just a check that the 
exports of a certain domain are a superset of the required exports.

> I understand what it means it terms of "has".

That is SPAD compiler biased. ;-)

> [...]
>
> | Gaby, you have given in
> | 
> | http://lists.nongnu.org/archive/html/axiom-developer/2007-08/msg00412.html
> | 
> | how the "add" part in the Monad definition is translated to a private domain.
>
> In fact, there is no nothing private about it.  The rewrite is available
> to user.
>
> | That looks perfectly fine to me.
> | Bill has already shown that a proper value for the argument of
> | RepeatedSquaring as in
> | 
> | http://wiki.axiom-developer.org/SandBoxMonad
> | 
> | works fine.
> | 
> | Gaby, you write there:
> | 
> |        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.
> | 
> | Why would the compiler want to "coerce" if all that is needed is to check
> | whether S of type Monad has at least the exports that are required by the
> | argument type of RepeatedSquaring. 
>
> The compiler is doing that because it treats function calls -- either
> to produce a value of a type -- uniformly.  It seems to me that you're 
> arguing two non-uniform rules: one for value, and one for types.  Is that
> correct? 

Hmmm, I would say, I don't completely understand all that, but I tend to 
say "yes".

You cannot achieve that uniformity. Take

define Cat: Category == with;
define Foo(T: Cat): Category == with {};
DomI: Foo(Integer) == add;
DomS: Foo(String)  == add;
b1: Boolean == DomI has Foo(Integer);
b2: Boolean == DomI has Foo(String);
b3: Boolean == DomS has Foo(Integer);
b4: Boolean == DomI has Foo(String);

If you treat domain constructors in the same way as basic values 
(functions) then

  Foo(Integer) = Foo(String) = with {}

So b1, ..., b4 should all be true, right? But I remember faintly that 
you argued about a functional language with respect to the types and 
that you would like to be able to distinguish

  Foo(Integer) from Foo(String)

No? Where would be the uniformity here?

Ralf