Bertfried,
On Sat, Dec 3, 2011 at 11:27 AM, you wrote:
>
>> )abbrev domain MYSET MySet
>> MySet(T:SetCategory): SetAggregate(T) with
>> finiteAggregate
>> join: MySet MySet T -> MySet T
>> == add
>> Rep == List T
>
> Why are the next two lines commented out?
>
In OpenAxiom (like Aldor) rep and per are built-in. In FriCAS one must
define them explicitly. The uncommenting these lines is needed when
attempting to compile this with FriCAS.
>> --rep(x:%):Rep == x pretend Rep
>> --per(x:Rep):% == x pretend %
>>
>> Rep2 := List List T
>> rep2(x:MySet MySet T):Rep2 == x pretend Rep2
>> per2(x:Rep2):MySet MySet T == x pretend MySet MySet T
>>
>> 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
>
>> Perhaps as you know the point of this exercise was to be able to write
>> 'MySet MySet T' (or equivalent) in the definition of MySet itself.
>
> Yes, I got that, and that was the reason why I tried to compile it.
I would like to write:
)abbrev category MONADC MonadCat
MonadCat(T:Type, M:T->T):Category == with
join: M M T -> M T
)abbrev domain MYSET MySet
MySet(T:SetCategory): MonadCat(T,MySet) with
finiteAggregate
== add
...
But this doesn't work even in OpenAxiom (yet).
> To define a monad,
> we need something which can operator on a (mathematical) category
> (say Set). Now sets itself may be structured, eg a set of elements,
> or a set of sets (take lists if you like).
Yes. As I currently understand that is what I intend by MonadCat above.
> So I wondered if one could have something like a `lazy type'. We want
> to have on the _category_ Set (List if you like) an endofunctor
> T : Set --> Set,
> which has as a codomain possibly a structured datatype (think
> of the power set functor) hence a set of sets (list of lists).
If I understand you correctly I think would could say that Axiom types
are always "lazy" in this sense.
> As the functor can be applied indefinitely often, we get data types
> of the form Set(Set(...(Set)...)). Clearly that is not a definable
> instance in a CAS.
This is not clear to me. I do not set any problem (in principle) with
such a type. What problems to you see?
> So I would like to see something as a type:
> lazyType = Type + T( lazyType )
> where the rhs is not evaluated (lazy). In terms of sets of elements
> of some type foo, we have foo, Set(foo), Set(Set(foo)), etc
> The monad multiplication operation will not look into the deeper
> nesting if always applied on the outer level (which is feasible due
> to associativity).
Yes. I don't think this is a problem. This is possible now. In fact
this is (more or less) done in the Axiom category ListAggregate now
for the specific case of List. The idea of MonadCat is to do this in
general for all monad-like types.
> So if the type checking would just see that there is
> at least on Set(bar) there, then the type of bar would not matter.
> I had the feeling that your code wanted to do this just for three
> levels:
> I, List(I), List(List(I))
No. Join requires the top two levels but th
Regards,
Bill Page.
--
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.
