Martin,
On Mon, Dec 5, 2011 at 4:47 AM, you wrote:
>> > Another idea that occurred to me would be to have an equivalent to the
>> > Haskell typeclass. Like a higher order (non-concrete) category, say a
>> > category where all the function parameters and returns are only
>> > specified in terms of types (not values). So the equivalent to the
>> > Haskell typeclass might be:
>> >
>> > )abbrev hcategory MONADC MonadCat
>> > MonadCat(M):Category == with
>> > join: M M A -> M A
>>
> On Monday 05 Dec 2011 02:07:45 Bill Page wrote:
>> Except for omitting the type of M, I do not see much difference from
>> what I wrote above.
>>
>> > So this could be implemented with 'M' as say:
>> > Integer -> Set Integer or Set Integer -> Set Set Integer ...
>>
>> I don't think this makes sense. M must be an endofunctor, i.e.
>> something like 'Set' itself.
>>
>> > Ideally 'A' would only need to be defined in join.
>>
>> As I described T above, A must be the formal parameter of the monad
>> MySet as the endofunctor M .
>
> This is a difference between what I wrote (which seem to me to be the
> Haskell way of doing it) and your code. Because-
>
> M=Set A=PI gives:
> join: Set Set PI -> Set PI
>
> M=Set A=Set PI gives:
> join: Set Set Set PI -> Set Set PI
>
> M=Set A=Set Set PI gives:
> join: Set Set Set Set PI -> Set Set Set PI
>
> So the same category represents all these, but not if A is a parameter
> of the whole monad, this seems to me quite a fundamental aspect of
> monads which your code does not support?
>
Your comments have made me look more carefully at what I wrote in my
reply and you are right, there was something wrong with my original
code:
> On Saturday 03 Dec 2011 21:42:20 Bill Page wrote:
>> 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
>> ...
It does not make sense for me to write M:T->T.
T is a *domain* but M is supposed to be an endofunctor from some
*category* to the same category.
We really want
)abbrev category MONADC MonadCat
MonadCat(T:Type, M:Type->Type):Category == with
join: M M T -> M T
This is equivalent in this context to what actual appears in my
OpenAxiom bug report.
)abbrev category MONADC MonadCat
MonadCat(A : Type, M: Type -> Type): Category == with
if A has SetCategory then SetCategory
fmap: (A->A, %) -> %
unit: A -> %
join: M % -> %
mult: (%, %) -> %
--
Just replace % by 'M T'. And the error message is the same.
Oddly, this variant:
MonadCat(A : SetCategory, M: SetCategory -> SetCategory): Category == with
join: M M A -> M A
gives a different result:
>> System error:
Control stack exhausted (no more space for function call frames).
This is probably due to heavily nested or infinitely recursive function
calls, or a tail call that SBCL cannot or has not optimized away.
PROCEED WITH CAUTION.
--
But contrary to what you say, there is no problem (in principle) to write:
MonadCat(PI,Set) to get
join: Set Set PI -> Set PI
MonadCat(PI,Set Set) to get
join: Set Set Set PI -> Set Set PI
etc.
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.
