Bill Page <[email protected]> writes:
| In a domain and in categories referenced in a domain the notation %
| represents "this domain" (or self in some programming languages). So
| we commonly write for example
|
| with
| f: (%,%) -> %
|
| to indicate a function f which takes a pair of values in this domain
| and returns a value in this same domain - whatever domain we happten
| to be talking about in this context.
|
| But what if we are interested in the domain as a functor?
I am having trouble understanding why you think using the domain functor
would be a problem.
| Suppose I
| was writing an "endofunctor" domain constructor like 'Set' and I
| wanted to treat constructions like 'Set Set R', i.e. sets of sets as
| something special. E.g.
|
| MySet:(T:SetCategory):SetCategory == with
| join: MySet MySet T -> MySet T
This would not compile in OpenAxiom because of syntax errors, etc.
I suspect the colon before the open parenthesis is a typo. I removed
it, but then I could not make sense of the rest. The return type
"SetCategory" indicates that MySet is intended to be a functor, however
the body, i.e. the right hand side of the '==' is a category expression
not a domain expression. The OpenAxiom compiler rejects the construct
for that reason. I tried a variation of what you wrote
)abbrev domain MYSET MySet
MySet(T:SetCategory): SetCategory with
join: MySet MySet T -> MySet T
== add
Rep == Void
join x == per void()
that compiles just fine.
Whether one can use it is a different issue: that is a co-inductive
definition without a witness of it being inhabited.
-- Gaby
------------------------------------------------------------------------------
All the data continuously generated in your IT infrastructure
contains a definitive record of customers, application performance,
security threats, fraudulent activity, and more. Splunk takes this
data and makes sense of it. IT sense. And common sense.
http://p.sf.net/sfu/splunk-novd2d
_______________________________________________
open-axiom-devel mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
