Indeed, once you've queried the type of a domain, what do you do with it?

| > | We want to be able to write:
| > |
| > | DirectProduct(4,1..9)
| > |
| > | but this does not work because '1..9' is not a type - it is an object
| > | of 'Segment PositiveInteger'.
| >
| > If it worked, what would you have liked the mathematical meaning to
| > be, and why?
| >
|
| I would like the result to be a finite domain.

that says what property the result would have, but it does not tell me
what the meaning of the result is. I would like to underdstand
the mathematical meaning.

[...]

| > | Another example of this in Axiom that *does* work right now is:
| > |
| > | DirectProduct(4,OrderedVariableList [a,b,c])
| > |
| > | OrderedVariableList is a domain constructor that takes something of
| > | List Symbol as a parameter. In order to introduce '1..9' as a domain
| > | it would be possible to introduce new domain constructor like
| > |
| > | )abbrev domain INTS IntegerSegment
| > | IntegerSegment(S:Segment Integer): with Finite ...
| > |
| > | that takes something of 'Segment Integer' as a parameter. Do we want
| > | 'IntegerSegment' to also be a subdomain of Integer?. In any case,
| > | then we could write:
| >
| > I do not see obvious reasons why I would want IntegerSegment to be a
| > subdomain of Integer.
| >
|
| Well for example, maybe I would want to write:
|
| x:IntegerSegment 1..9
| y:=x + 1
|
| where the type of 'y' might be Union(IntegerSegment 1..9,"failed").

So, you are actually after a domain that constrains all operations on
the values of its objects to deliver a value in a specified bound. I
can be persuaded that IntegerSegment convays such meaning, but I'm not
sure the notation `1..9' is intuitive to me, given its other existing
meaning.

| > | DirectProduct(4,IntegerSegment 1..9)
| > |
| > | But somehow the distinction between '1..9' and 'IntegerSegment 1..9'
| > | and '[a,b,c]' and 'OrderedVariableList [a,b,c]' seems artificial.
| > |
| > | It occurs to me that one might like at least the Axiom interpreter to
| > | perform some kind of automatic coercion from 'x' in a domain like
| > | 'Segment Integer' into the *category* consisting of domains
| > | 'IntegerSegment(x)'.
| > |
| > | I think Gaby recently referred to this preference for things like
| > | '1..9' and [a,b,c] to also
| > | represent domains as a more "categorical" approach.
| >
| > In general, I would like OpenAxiom to take a more categorial approach
| > to almost everything -- in particular `cross'.
|
| Great. One should probably try to be more specific here about what one
| means by a "categorical approach". You could mean for example trying
| to provide mathematical semantics based on category theory. I have
| discussed before how one really should define 'cross' as a categorial
| limit in terms of the existence of the unique (universal) operation:
|
| product: (A:Type, A->X,A->Y) -> (A->%)
|
| See: http://wiki.axiom-developer.org/SandBoxLimitsAndColimits
|
| > However, I'm interested in some of you ideas here. Please, could you
| > elaborate, and if possible, give some use cases?
| >
|
| Do you mean use cases for operations like 'product' above or use cases
| of the domain 'Product' or use cases of the domain 'IntegerSegment'?
| :-)

I'm specifically after `1..9' that you would want to be a domain
and the various constructs you based on it.

-- Gaby