Re: [Axiom-developer] Unions in Spad

[Ralf Hemmecke]

> > Stephen, have you ever thought about the difference between Rep and %?

> Yes. 

Good.

> > The type of [n] would be Rep, since there is no function
> >
> >    bracket: Integer -> %
>
> Perhaps you are thinking in terms of Aldor?

Yes, but that has nothing to do with Aldor.

>  In Spad, we have:
>
>    1) -> )sh Union(tag1: Integer, tag1: String)
>     Union(tag1: Integer,tag1: String) is a domain constructor.
>    ------------------------------- Operations --------------------------------
>
>     ?=? : (%,%) -> Boolean                ?case? : (%,tag1) -> Boolean
>     ?case? : (%,tag1) -> Boolean          coerce : % -> OutputForm
>     construct : Integer -> %              construct : String -> %
>     ?.? : (%,tag1) -> Integer             ?.? : (%,tag1) -> String

> Here, `bracket' is known as `construct', and as you can see, there are
> two such operations. 

OK. Let's assume that 'construct' exists (BTW my previous mail has 
already considered that case, but let's try to make it explicit.

> > so if you write
> >
> >    inj (n : Integer) : % == [n]
> >
> > as above, that should be a type error.
>
> On the contrary, it is a call to:
>    
>     construct : Integer -> %
>
> which is well typed.

Sorry, but I believe you are wrong. Rep and % are perhaps identical in 
their represenstation, but they export different functions. You know 
that, since you know Aldor. And if you want to have that treated 
differently in SPAD, then I am not on your side. I don't care what the 
current SPAD compiler or interpreter does. I'd rather like to look at 
the example from a specification point of view.

Since

  construct: Integer -> %

is exported by

  Union(tag1: Integer, tag1: String)

In the context of

> )abbrev domain BAR Bar
> > > Bar() : Exp == Impl where
> > >    Exp == with
> > >      inj : Integer -> %
> > >      inj : String -> %
> > >      prj : % -> Integer
> > >    Impl == add
> > >      Rep := Union(tag1: Integer, tag1: String)
> > >      inj (n : Integer) : % == [n]
> > >      inj (s : String) : % == [s]
> > >      prj p == (p::Rep).tag1

if there where a statement like

  import from Rep

there would then be

  construct: Integer -> Union(tag1: Integer, tag1: String)

in scope. Clearly,

  [n]

would be of type Union(tag1: Integer, tag1: String) and not of type %.
Type mismatch. That is why Aldor would require to write

  inj (n : Integer) : % == per [n]

Although that costs some typing. It's much clearer. Not only for the 
compiler but also for me. (Don't tell me that per is actually only a 
macro. I know that.)

And I hope some time SPAD also requires to write

  Rep == ...

because

  Rep := ...

introduces a variable Rep (not a constant). Would you think that

)abbrev domain BAR Bar
Bar() : Exp == Impl where
  Exp == with
    inj : Integer -> %
    inj : String -> %
    prj : % -> Integer
  Impl == add
    Rep := Union(tag1: Integer, tag1: String)
    inj (n : Integer) : % == [n]
    Rep := Union(tag1: String, tag1: Integer)
    inj (s : String) : % == [s]
    prj p == (p::Rep).tag1

should actually compile? On my machine (GOLD) it does. With some 
warnings, but that's all.

By the way let me give another example.

In Aldor I can write the following:

woodpecker:~>aldor -fx -laldor aaa.as
woodpecker:~>aaa
    inc f = 2
get inc f = 101

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

Foo: with {
  inj: Integer -> %;
  inc: % -> Integer;
  inc: % -> %;
  get: % -> Integer;
} == add {
  Rep == Integer;
  import from Rep;
  inj(z: Integer): % == per z;
  inc(x: %): Integer == rep x + 1;
  inc(x: %): % == per(rep x + 100);
  get(x: %): Integer == rep x;
}
main(): () == {
  z: Integer := 1;
  f: Foo := inj z;
  stdout << "    inc f = " << inc f << newline;
  stdout << "get inc f = " << get inc f << newline;
}
main();
---END aaa.as

Write the same program in SPAD and compile it.

Ralf