Im not going to try and defend the idea, as I feel I can work with
simpler notions. But 1 and + would be considered value identifiers.
You might be right, but what I will certainly do in a near future is an
implementation of a domain whose elements are combinatorial species.
That domain will be a semiring, so I will use + and 1 to denote the
"elements" Plus
(http://www.risc.uni-linz.ac.at/people/hemmecke/AldorCombinat/combinatsu23.html#x37-550008.10)
and EmptySetSpecies
(http://www.risc.uni-linz.ac.at/people/hemmecke/AldorCombinat/combinatsu17.html#x31-380008.4.1).
As you see these identifiers actually denote not only domains but
functions that return domains. Would you like me not to use 1 just
because my elements would be domains?
Having the types as first class objects has the consequence that type
can appear in places where you expect an "element".
However, I need to explore the use tuples exclusively to lift types
otherwise hidden by sope into an enclosing context. I suspected that
type patterns would be generally useful but I like the simplicity of
Martins approach and will try to work with that.
Martin was just demonstrating ordinary use of a dependent type.
Ralf
_______________________________________________
Axiom-developer mailing list
[email protected]
http://lists.nongnu.org/mailman/listinfo/axiom-developer
