The infinite union that you suggest looks interesting from a
mathematical point of view, but whether it is good from a computer
science point of view, might be a bit questionable.
Suppose instead of
DirectProduct: (NNI, Type) -> DirectProductCategory(...)
you have something like
Foo: (NNI, NNI) -> FooCategory(...)
Before you can apply Union on Foo, you have to construct a univariate
functor
Bar: NNI -> ...
that works like
Bar(n) == Foo(n, 42)
or
Bar(n) == Foo(42, n)
Well, that is OK, that there would be some need to transform something
into a univariate constructor before applying IndexedUnion (you have
simply called that "Union"). But why should there be a restriction that
the index is of type NNI?
As a mathematician, I would be more happy to write
Union(Foo(n, 42) for n in NNI)
or whatever syntax would be best.
In fact, I need something similar in Aldor-Combinat for multisorted species.
There I basically have a vector (A, B, C) of domains of a certain (fixed
and known) length and want to construct another vector (F A, F B, F C)
where F is a functor. Both vectors would be of the same type.
Of course, I can write this for vectors of length 1, 2, 3, etc. by hand,
but all this is of basically the same structure. So I would like to have
a programming construct that enables me to write such a construction
uniformly for vectors of length n, i.e. Vector(F(V.i) for i in 1..n).
Of course, that construction should not solely be a runtime construct. I
would like to see as much type information as possible checked at
compile time.
On 04/02/2008 05:52 AM, Bill Page wrote:
> Gaby, et al.
>
> I have been thinking about dependent types in Aldor quite a bit and as
> I mentioned elsewhere I do not really like this approach very much. In
> brief I think it is not "algebraic" enough for Axiom - we need to
> introduce variables in type expressions and other "non-algebraic"
> things like universal quantification rules, etc., etc.
>
> Consider the canonical example of a function that takes and a
> non-negative Integer 'n' and returns the zero "vector" of type
> 'DirectProduct(n,Integer)'
>
> zeroVector(n:NonNegativeInteger):DirectProduct(n,Integer)
>
> As far as I know it is impossible to write such a function in any
> version of Axiom as it stands today but this is possible in Aldor.
I think, no matter whether or not this is possible in Aldor, it looks
like a bad construction.
Suppose you implement the DirectProduct constructor with only vectors of
lenght n in mind. You would probably want your zero vector to have signature
0: %
and not
zeroVector: NNI -> %
since the latter implies that your implementation starts with
zeroVector(m: NNI): % == {
if not (m=n) then throw WrongLengthException;
...
}
(n comes from the domain definition
DirectProduct(n: NNI, T: Type): DirectProductCategory(n, T) == { ... }
where the above zeroVector would be implemented.)
> The issue is the nature of the domain on the right-hand side of the
> signature of zeroVector
>
> NonNegativeInteger -> DirectProduct(n,Integer)
>
> What is 'n' in this signature? The usual universal quantification
> suggests that we might like to write something like:
>
> Union(DirectProduct(0,Integer),DirectProduct(1,Integer), ... )
You certainly know that for your construction, the right signature for
your dependent type is
(n: NNI) -> DirectProduct(n, Integer)
and not just NNI.
> So suppose we introduced a new Union constructor that operates on
> other domain constructors. Given a domain constructor in one argument,
> e.g.
>
> DirectProductInteger(n:NonNegativeInteger):DirectProductCategory(n,Integer)
> == DirectProduct(n,Integer)
>
> Then
>
> Union(DirectProductInteger)
>
> would construct a domain representing the infinite union indexed
> (labeled) by objects of type NonNegativeInteger.
>
> Then 'zeroVector' could be written with this signature:
>
> zeroVector: NonNegativeInteger -> Union(DirectProductInteger)
>
> The need for variables disappears.
I don't know, whether my remarks above are clear, but suppose I really
use the signature
0: %
in my DirectProductInteger(n) domain, then the question is what is the
category of
Union(DirectProductInteger)
? Would it export something like
0: %
? Certainly, it shouldn't. Rather it should only export the inclusion
function that come from the categorial construction. If certain
operations can be lifted from the underlying domains to the union that
must be specified explicitly or through some (new) language construct
that is able to look into the category of DirectProductInteger and is
able to lift certain operations categorially.
I am not a language expert, but to me it sounds like that there should
be a construct that lets a programmer write something as general as
IndexedUnion.
Ralf
-------------------------------------------------------------------------
Check out the new SourceForge.net Marketplace.
It's the best place to buy or sell services for
just about anything Open Source.
http://ad.doubleclick.net/clk;164216239;13503038;w?http://sf.net/marketplace
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
