axiom-developer
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] Unions in Spad


From: Stephen Wilson
Subject: Re: [Axiom-developer] Unions in Spad
Date: 08 Jul 2007 22:27:00 -0400
User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.4

"Bill Page" <address@hidden> writes:

> On 08 Jul 2007 17:51:54 -0400, Stephen Wilson wrote:
> > ...
> > But I think Aldor's treatment of selectors as elements of type
> > Enumeration is worth looking at and possibly worth making explicit in
> > Spad.  Spad seems to follow similar semantics conceptually but I cant
> > see the direct connection to the type system at this time.
> >
> 
> Gaby noted in another thread that Spad does in fact already implement
> Enumeration as a basic data type even though it is completely
> undocumented at the user level.

Oh, I know there exists an Enumeration type.  But not only is it not
documented, its also unused.  Perhaps it is used to interact with
Aldor compiled libraries?  I'll review the mailing list archives.

> But really I think the concept of "selectors" in both Union and Record
> is at best a legacy of earlier days in programming language design. 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.

Its been a while since I brushed up on Category Theory.  Yet another
todo item.  I thought that limit and co-limit were defined w.r.t an
index category.  How does this differ from the notion that an instance
of Enumeration type serves as the index into a record or union, and
how do the morphisms from the objects of the index category to the
objects of the category representing the elements of a union/record
differ from normal "selectors"?  Im probably missing some details, but
from my modest understanding of Category Theory, I feel the
categorical treatment is just a different vernacular to express the
same thing.  There are undoubtedly generalizations Im missing, but I
am curious how they might be expressed meaningfully in a programming
language.

Perhaps an example of how you envision this foundation working in
Spad?


Thanks so much for your feed-back!
Steve





reply via email to

[Prev in Thread] Current Thread [Next in Thread]