On Wed, Apr 2, 2008 at 4:38 AM, Ralf Hemmecke wrote:
>
> 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.
> ...
> But why should there be a restriction that
> the index is of type NNI?
>
There is no such restriction. The index domain can be any domain.
> As a mathematician, I would be more happy to write
>
> Union(Foo(n, 42) for n in NNI)
>
> or whatever syntax would be best.
>
It is the introduction of formal variables in type expressions that I
wish to avoid.
> ...
>
> On 04/02/2008 05:52 AM, Bill Page wrote:
> > ...
> > 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 -> %
>
No 'zeroVector' is not a vector. [0,0,0] is a member of 'zeroVector(3)'.
> 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.)
>
What you have described is a different problem/example.
>
> > 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.
>
No. This is called a "signature" but I do not know what kind of
*domain* the expression '(n:NNI)' represents. The variable 'n' makes
this just an expression. Is
(n:NNI) == NNI ?
Does
(n:NNI) == (m:NNI) ?
I do not want signatures to contain such expressions - it is not
"algebraic"! I would prefer something that is a higher-order algebraic
operation.
>
> > 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)
>
That is a good question. In general what is the axiom/aldor category
associated with a Union?
(1) -> )show Union(Integer,String)
Union(Integer,String) is a domain constructor.
------------------------------- Operations --------------------------------
?=? : (%,%) -> Boolean autoCoerce : % -> Integer
autoCoerce : % -> String autoCoerce : Integer -> %
autoCoerce : String -> % ?case? : (%,Integer) -> Boolean
?case? : (%,String) -> Boolean coerce : % -> Integer
coerce : % -> OutputForm coerce : % -> String
> ? Would it export something like
>
> 0: %
>
> ? Certainly, it shouldn't. Rather it should only export the inclusion
> function that come from the categorial construction.
Yes certainly. The inclusions are normally represented by 'autoCoerce'
operations.
autoCoerce : String -> %
autoCoerce : Integer -> %
Or the 'construct' operations in a labelled Union:
(1) -> )show Union(A:Integer,B:String)
Union(A: Integer,B: String) is a domain constructor.
------------------------------- Operations --------------------------------
?=? : (%,%) -> Boolean ?case? : (%,A) -> Boolean
?case? : (%,B) -> Boolean coerce : % -> OutputForm
construct : Integer -> % construct : String -> %
?.? : (%,A) -> Integer ?.? : (%,B) -> String
I don't really know why these are treated so differently.
> 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 think the situation is a little different for built-in primitive
domains and domain constructors.
> 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.
>
Take a closer look at the changes the Gaby has made to Union/case
construct in OpenAxiom. I think that might be close to what you
suggest.
Regards,
Bill Page.
-------------------------------------------------------------------------
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
