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.
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), ... )
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.
It seems that something like this might "almost work" in OpenAxiom now. E.g.
(1) -> (DirectProduct(n,Integer) for n in 0..2)
Local variable or parameter used in type
We will attempt to interpret the code.
(1)
(DirectProduct(0,Integer),DirectProduct(1,Integer),DirectProduct(2,Integer))
Type: Tuple Domain
(2) -> Union(DirectProduct(n,Integer) for n in 0..)
Local variable or parameter used in type
We will attempt to interpret the code.
Interpret-Code mode is not supported for stream bodies.
(2) -> Union(DirectProduct(n,Integer) for n in 0..2)
Local variable or parameter used in type
We will attempt to interpret the code.
Local variable or parameter used in type
We will attempt to interpret the code.
((DirectProduct n Integer)for n in 0..2) is not a valid type.
(2) ->
0$DirectProduct(2,Integer)::Union(DirectProduct(0,Integer),DirectProduct(1,Integer),DirectProduct(2,Integer))
(2) [0,0]
Type: Union(DirectProduct(2,Integer),...)
(3) ->
-------
I know that you have already provided some generalization of the Union
construct in OpenAxiom. What is your opinion of the possibility of
extending Spad and OpenAxiom in this direction?
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
