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?
On Tue, Nov 8, 2011 at 1:45 PM, Gabriel Dos Reis <g...@cs.tamu.edu> wrote: > Bill Page <bill.p...@newsynthesis.org> writes: > > | Bill Page <bill.p...@newsynthesis.org> 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 fricas-de...@googlegroups.com. > To unsubscribe from this group, send email to > fricas-devel+unsubscr...@googlegroups.com. > 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 open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
