Re: [Axiom-developer] Unions in Spad

[Bill Page]

On 11 Jul 2007 08:08:27 -0500, Gabriel Dos Reis wrote:
> ...
> "Bill Page" <address@hidden> writes:
> | It
> | makes much for sense to me to define Union and Record as co-limit and
> | limit in the sense of category theory. Then Union selectors are just
> | injections operations and Record selectors are projection operations
> | which are exported like any other function from these types. There is
> | no need for any lower level language construct.
>
> Well, if we are to be following that reasoning, there is no need for Spad
> -- we just need lambda calculus.
> We should be discussing what is useful, convenient; not the bare
> minimum that is necessary.

That is not what I am arguing. I want Record and Union domains just as
they exist now in Spad but with a simple and rigorous object-oriented
semantics consistent with other Axiom domains. We do not need to talk
about selectors and enumerations in order to define these concepts. It
is enough that these domains export projection and product
(respectively, injection and sum) operations that satisfy certain
(categorical) axioms, in the same way that other domains in Axiom do.

Here are some some toy notions...

We can recover the usual notation for records by defining '.' as left
associative application. Given the value of some 'a' of type 'A' we
can define an instance 'r' of some Record having a "field" named 'x'
that takes values from 'A'. But 'x' is actually the name of one of the
projection functions exported by the record.

 a:A
 r:Record(x:A, ...) := [a, ... ]
 x$Record(x:A, ... )  : % -> A
 x(r) = r.x =  a

Eg.

p1:Record(Age:Integer,Name:String) := [25, "Peter"]
p1.Age = 25
Name(p1) = "Peter"

And we can do something similar (bug categorically dual) for unions:

Given the value of some 'b' of type 'B' we can define an instance 'u'
of some Union having a "field" named 'y' with values from 'B'. But 'y'
is actually the name of one of the injection functions exported by the
Union. Evaluating y of b yields a member of the Union.

 b:B
 u:Union(y:B, ...) := y(b) = b.y
 y$Union(y:B, ... ) : B -> %
 case y : % -> Boolean

'case' classifies the sub-object (injective map) 'y' over the Union.
'/y' denotes the inverse of 'y' defined over this sub-object of u. For
convenience '.' is omitted in the expression 'u./y'.

 if u.case(y) then u/y = b

Eg.

d1:Union(inches:Float,feet:Float) := (2.5).feet
d2:Union(inches:Float,feet:Float) := inches(30.0)
if d1 case feet then d1/feet = 2.5
try d1 := feet(d2/inches / 12.0)

It seems to me these primitive domains would be quite easy to provide in Spad.

Another issue. It seems strange to me that Spad does not have any
primitives for exception handling, e.g. 'try'.

Regards.
Bill Page.