Re: [Axiom-developer] Unions in Spad

[Gabriel Dos Reis]

On Wed, 11 Jul 2007, Bill Page wrote:

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

My point is that the selectors are precisely the projectors -- and
the injectors are already there.  

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

I agree.  And I think that is what the current semantics does.

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

Agreed.  More strangely to me, it seems odd that Spad does not
have algebraic data types ans pattern matching (Boot does).

They support different styles of programming.

-- Gaby