Hi Ralf,
This is late in the night for me, so please forgive the terse
response.
Ralf Hemmecke <[EMAIL PROTECTED]> 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
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
http://lists.nongnu.org/mailman/listinfo/axiom-developer
