On Sun, Dec 4, 2011 at 12:17 PM, Martin Baker wrote: > 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? >
I reported this as a bug in OpenAxiom http://sourceforge.net/tracker/?func=detail&atid=984524&aid=3448475&group_id=203172 Recent changes in OpenAxiom have changed the error message. The original message "cannot form Join" is probably more indicative of what is going wrong. The "apparent user error" Cannot coerce #1 of mode Type to mode SetCategory suggests to me that perhaps the compiler is not passing all the information about the types of the arguments to MonadCat or perhaps that the type inference is somehow incomplete. I expect that the more recent message "The value NIL is not of type DATABASE." is likely due to unrelated changes that Gaby is currently making to the compiler. But that is just a guess. I wish I had enough time and skill to actually work on these sort of compiler internals. These are in short supply in all the Axiom projects. Although fixing this or explaining why should not work may not be a currently priority, I am fairly sure that the changes Gaby is making to the compiler will eventually resolve it one way or another. > 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? Yes, Type is the top of the category lattice but values like '3' and "text" are ... well, just values. T is necessarily a domain in the category Type. It does not make sense in Axiom to talk about values binding to categories. Axiom has a two-level type system consisting of categories and domains. In fact in Axiom values do not "bind" even to domains. Values have no type in and of themselves. Only variables, constants and formal parameters have types. > 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 > No, I don't think so. In MonadCat T is just some domain with an endofunctor M. A domain that satisfies MonadCat(T,M) is expected to be a monad, i.e. it must export operations that satisfy the monad axioms. In MySet(T:SetCategory) we so specify that T satisfies SetCategory. MonadCat(T,MySet) is a dependent type in this context. > 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 > 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 . > 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 > I think this happens (or should happen) now. > 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. > I do not see any reason to claim that SPAD is somehow less "powerful" than Haskell even as it stands now. To be sure both SPAD and Haskell (not to mention, Lisp, C and assembler language, etc. ) are formally universal. The concept of the "power" of a language is almost too vague to be useful. Even the idea of the "expressiveness" of a language is hard to quantify. How much "effort" it takes to write code in one language or another is highly subjective. To a large extent it comes down to a choice of style. 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.
