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