Bill Page <[email protected]> writes: | I think the definition given here: | | http://en.wikibooks.org/wiki/Haskell/Category_theory | | will suffice for my purpose, especially when expressed in terms of | 'unit' and 'join'. Is that OK with you?
No. Because you are still asking me to second-guess what you meant. I am very willing to discuss the specifics of how this and that construct in Haskell is or is not available in SPAD, but you need to come forward with a specific example. Another reason is that that wiki uses terminology slightly different from what we use in Spad (e.g. they have a type class named Functor, but the equivalent of a type class in Spad would be a category, their Functor is unary but there is no such restriction in the terminology of Spad, etc.) What I am asking, for the purpose of making progress on this apparently recurrent and important issue, is that you put forward a specific program example in Haskell and say exactly what you want. I am just following through your previous statement "How can I implement Haskell monads in OpenAxiom". I want to see your Haskell monads, so that I can discuss how they relate to OpenAxiom notions. It isn't a trick question. It is just that there are so many things out there that one easily mistakes something for another thing. Hope that clears things a big. | | On Tue, Nov 8, 2011 at 1:53 PM, Gabriel Dos Reis <[email protected]> wrote: | > Bill Page <[email protected]> writes: | > | > | How can I implement Haskell monads in OpenAxiom (or any other Axiom | > | variant including Aldor)? How does or how could the monad construction | > | in Haskell fit into Axiom? | > | > OK. Show me your version of Haskell monad -- the reason I am asking is | > that there are many things people call "monad" (including in Haskell) | > and it would be not productive that I second guess what you meant. | > | > -- Gaby | > | > | | > | On Tue, Nov 8, 2011 at 1:45 PM, Gabriel Dos Reis <[email protected]> wrote: | > | > Bill Page <[email protected]> writes: | > | > | > | > | Bill Page <[email protected]> writes: | > | > | > ... | > | > | > | Second, we are trying to pass the functor M as a parameter. | > | > | > | Specifying this is a currently very awkward in both SPAD and Aldor. | > | > | > | What Ralph wrote involves passing a function which returns domain. In | > | > | > | Axiom and it's derivatives this is not the same thing as a domain | > | > | > | constructor (= functor). This is a rather deep issue in the | > | > | > | fundamental design of SPAD and Aldor where types are supposed to be | > | > | > | static and I am not sure if it was ever fully resolved. Maybe | > | > | > | OpenAxiom has made some progress here as well? | > | > | > | | > | > | | > | > | On Tue, Nov 8, 2011 at 10:44 AM, Gabriel Dos Reis wrote: | > | > | > | > | > | > I think this essentially goes back to a discussion we had recently. I | > | > | > am not sure I succeeded in getting my points trough:-) | > | > | > | > | > | | > | > | Yes, I have been listening. I think I understand this in the context | > | > | of the changes that you have made to OpenAxiom. | > | > | > | > Hmm, I am not sure I understand, but let's see. | > | > | > | > | > Yes, functors and category constructors are functions, but they are not | > | > | > ordinary functions. In general type constructor (in SPAD or any ML | > | > | > descendent, which includes Haskell) and data constructors are special | > | > | > functions. In terms of formal semantics, they are not reducible. | > | > | > This is a very important point. That allows the compiler to internally | > | > | > reason on some usage, including deciding equality when type checking an | > | > | > expression. | > | > | > | > | > | | > | > | Do you think we should be allowed to write something like the | > | > | following in the OpenAxiom compiler (SPAD)? | > | > | | > | > | (X:Domain):Domain+->List X | > | > | | > | > | i.e. define a function that takes a domain as an argument and returns | > | > | a domain? Could we use such a thing in a statically typed language? I | > | > | suppose not. | > | > | > | > In OpenAxiom, that depends on the context of usage. | > | > | > | > | > At the moment, all AXIOM variants do not allow you to pass a category as | > | > | > a parameter in a domain or category definition -- well, you can in | > | > | > OpenAxiom but the usage then is limited. As a consequence, | > | > | > you can't introduce a category as a parameter and a domain parameter | > | > | > depending on the category parameter and expect anything useful to come | > | > | > out. In your definition of MonadCat2, the compiler internally assumes | > | > | > that the parameter 'C' designates a domain -- not a category as you | > | > | > intended -- because its type is a category. You can check that by | > | > | > looking at the dual signature (or COSIG property of the DB) of MonadCat2. | > | > | > So, your attempt to call it with SetCategory for C is a type violation. | > | > | > | > | > | | > | > | It is not so clear to me that Aldor intended to duplicate this part of | > | > | the Axiom semantics. | > | > | > | > I am not sure I understand; could you elaborate? | > | > | > | > | > All AXIOM compilers assume that when they see a category form, the | > | > | > head is a category constructor, not an arbritrary function (or | > | > | > parameter) that may evaluate at runtime to a category. This allows the | > | > | > compiler to type check domains. The story is almost the same for | > | > | > domain forms in certain situations. See the roundabout hack in | > | > | > the implementation of Table (table.spad.pamphlet) just to conditionally | > | > | > select the representation domain (InnerTable.) OpenAxiom's compiler | > | > | > tried to improve on the situation, but only marginally at the moment. | > | > | > | > | > | | > | > | Yes, that is interesting. | > | > | | > | > | > But, whatever is done there is no way around the fact that a constructor | > | > | > is not an ordinary function -- being in Haskell or in Spad. | > | > | > | > | > | | > | > | Yet in Haskell we do have functors and monads ... | > | > | > | > Yes, but I am not seeing the implication. Could you elaborate? | > | > | > | > | One question being asked here is "what is required in Axiom (and/or | > | > | its descendants) to do something equivalent? | > | > | > | > Equivalent to what? I'm afraid I do not understand the description of the | > | > thing being claimed to be in Haskell -- to remove any misunderstanding I | > | > understand Haskell, but I do not understand the *claim* being made and what | > | > "equivalent" is being sought. | > | > | > | > Any clear elaboration of the original issue will help. | > | > | > | > -- Gaby | > | > | > | > -- | > | > 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. | > | > | > | > | > | ------------------------------------------------------------------------------ RSA(R) Conference 2012 Save $700 by Nov 18 Register now http://p.sf.net/sfu/rsa-sfdev2dev1 _______________________________________________ open-axiom-devel mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
