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
--
You received this message because you are subscribed to the Google Groups
"FriCAS - computer algebra system" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/fricas-devel?hl=en.
