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
>        ...
>
> But this doesn't work even in OpenAxiom (yet).

Do you have any views on why this is and whether there is any prospect
of a change to SPAD to allow this?

Just to try to help my own understanding of the issue I have been
thinking about it and it seems to my non-expert eye that 'Type' in:
MonadCat(T:Type, M:T->T):Category == with
is too general(no type checking), in that if Type is the top if the
category lattice then T should bind with values like '3' and "text" as
well as types like Integer?
Would it help the compiler, as well as human readers of the program,
if we could specify a higher kinded type like this:
MonadCat(T:HigherType, M:T->T):Category == with

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

So this could be implemented with 'M' as say:
Integer -> Set Integer or Set Integer -> Set Set Integer ...
Ideally 'A' would only need to be defined in join.
I was thinking that the advantage of this would be that the compiler
would know that a functor could be applied to a type when they are
adjacent so
(A -> M A) A
would bind to M A

As I say, I'm just trying to get these issues clear in my mind and to
try to understand if SPAD will ever be as powerful as Haskell with
this type of construct.

Martin

-- 
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.

Reply via email to