Gaby,
On Mon, Nov 21, 2011 at 8:52 AM, you wrote:
> Bill Page <bill.p...@newsynthesis.org> writes:
> ...
> | 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.
Yes. I am sorry that my example was so sloppy and I appreciate your
effort to understood my intention. Thank you.
> 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.
>
Yes, thank you for giving this example. Maybe it is interesting that
this example does not compile in FriCAS.
> Whether one can use it is a different issue: that is a co-inductive
> definition without a witness of it being inhabited.
>
Here is some more realistic example code that does compile and run:
)abbrev domain MYSET MySet
MySet(T:SetCategory): SetAggregate(T) with
finiteAggregate
join: MySet % -> MySet T
== add
Rep == List T
--rep(x:%):Rep == x pretend Rep
--per(x:Rep):% == x pretend %
Rep2 := List List T
rep2(x:MySet(%)):Rep2 == x pretend Rep2
per2(x:Rep2):MySet(%) == x pretend MySet(%)
coerce(x:%):OutputForm == brace [i::OutputForm for i in rep x]
x = y == rep(x) = rep(y)
construct(x) == per removeDuplicates(x)$Rep
parts(x:%):List T == rep x
join x == construct concat rep2 x
--
(1) -> m1:MySet(Integer) := construct([1,2,3])$MySet(Integer)
(1) {1,2,3}
Type: MySet Integer
(2) -> m2:MySet(Integer) := construct([4,5,6])$MySet(Integer)
(2) {4,5,6}
Type: MySet Integer
(3) -> m12:=construct([m1,m2])$MySet(MySet Integer)
(3) {{1,2,3},{4,5,6}}
Type: MySet MySet Integer
(4) -> join m12
(4) {1,2,3,4,5,6}
Type: MySet Integer
--
Could you elaborate a little on what you mean by:
"that is a co-inductive definition without a witness of it being inhabited"
Does this have something to do with the need to for a type coercion
such as 'rep2' above?
Regards,
Bill Page.
------------------------------------------------------------------------------
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
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
