Re: [Axiom-developer] Unions in Spad

[Stephen Wilson]

Hi Ralf,

This is late in the night for me, so please forgive the terse
response.


Ralf Hemmecke <address@hidden> writes:

> =--- union-test.spad ----
> > )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
> 
> Stephen, have you ever thought about the difference between Rep and %?

Yes. 

> The type of [n] would be Rep, since there is no function
> 
>    bracket: Integer -> %

Perhaps you are thinking in terms of 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. 

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


Take care,
Steve