Bill Page <bill.p...@newsynthesis.org> writes: [...]
| > | Monad(A: SetCategory, M: SetCategory -> SetCategory): Category == with | > | unit: A -> M A | > | mult: M M A -> M A | > | | > | Yes that does compile. | > | > Great! | > | > | Is M compiled as a function or as a functor? | > | > In OpenAxiom, it is elaborated as a parameter with function type -- | > which is also what I read from your code. Also, remember that a | > category definition is barely type checked. You can smuggle in there | > just about anything and we have seen that in the past. | > | | So 'List' is not of type 'SetCategory->SetCategory', That is correct. A subsidiary question is whether it can be *coerced* to that type. See below. | but you are going to tell me that it *is* a function of type 'Type->Type', More precisely, the constructor List can be coerced to a function of type Type -> Type. Since the coercion does not incur any runtime computation, we just "pretend" that that function is also List. In addition, note that the type Type -> Type, mirrors more closely what you have in Haskell (which, if I understand correctly, sparked the debate; correct me if I am wrong). In Haskell you have * -> * where * is the kind (i.e. type) of all types. | 'Type' being the top of the category hierarchy with no exports. All | domains satisfy 'Type' by definition. It just so happens that the | actual type of 'List' is '(R:Type) -> Join(ListAggregate(R), ... )'. Yes, that is correct. The type of the contructor List (and in general, that of any constructor in AXIOM) is slightly more complicated than the types of most ordinary functions. It is a dependent type, i.e. the target type can mention (abstract) values of the parameters. To this date, no AXIOM flavour has a general support for dependent types. For constructors, howver, dependent types are important. So a special handling is done for them. Formal parameters are named #i where <i> is the position of the parameter in the parameter list, starting from 1. With that, the rest of elaboration (and type checking) is not as if in a conventional type system without dependent types. It works well almost all the time -- except when it does not, in which case you get some "surprises", but it is important to understand the current model (I am not justifying them, just explaining things.) | As written, 'List' is not an endofunctor but it can be considered as | such if we are willing to forget about what it exports. Well, the contructor List *is* an endofunctor -- you certainly can iterate it. An endofunctor is not required to be surjective, so it is OK if its range has more properties than its input, as long as the range is included in the input -- which is the case here. | > | If function what does M A mean in the signatures for unit and mult ? | > | > In OpenAxiom, M A is an expression designating a domain that satisfies | > SetCategory. Did you have a different expectation? | > | | This is my confusion. | | It did not occur to me that I could simply use a function where a | domain is expected. I find it difficult to keep in mind that the | difference between a function and functor is in only in how they are | evaluated, That is why they are called "constructors" :-) Constructors are very special -- the systems know about them in very intimate ways. Furthermore, formal systems also know about them -- you must, at least if you want to distinguish values from general expressions. | therefore I (incorrectly) assumed that a function and a | functor necessarily had different types. But what you are telling me | is that any expression that evaluates as a domain is acceptable here. That is correct. There are situations where the system needs to know whether something is a constructor or just a general function -- e.g. when to decide equality of types. | > | The code that does not compile is when we try to use it. | > | > In OpenAxiom, the category definition is just fine. It is just a | > category definition; there is no high hope there. | > However, the instantiation with arguments Integer and List is not type | > correct, because the functor List does not have the type expected by Monad. | > | | Yes. Thank you for the explanation. Therefore if I expected to pass | 'List' as an argument of Monad I must have: | | Monad(A: Type, M: Type -> Type): Category == with | unit: A -> M A | mult: M M A -> M A Yes, at least until the systems understand dependent types or at the very least dependent contravariant type coercions. | | > ... | > While looking at this, I realize there is a bug in the OpenAxiom | > compiler where a conversion of constructor to a general function type is | > not compiled correctly. Fixed. See example here: | > | > http://svn.open-axiom.org/viewvc/open-axiom/1.4.x/src/testsuite/compiler/ctor-mapping.spad?revision=2459&view=markup | > | > The handling in the interpreter is a completely different story. | > | > | > | 7) What type (if any) should be associated with a functor? | > | > | > | > Every functor in AXIOM has a type. You get it by executing | > | > | > | > )boot getConstructorSignature ctor | > | > | > | > where <ctor> is the name of the constructor you want, e.g. 'List, | > | > 'Integer, etc. | > | | > | In FriCAS I get with Complex for example: | > | | > | )boot getConstructorSignature 'Complex | > | | > | (|getConstructorSignature| '|Complex|) | > | Value = ((|Join| (|ComplexCategory| |#1|) | > | (CATEGORY |package| | > | (IF (|has| |#1| (|OpenMath|)) | > | (ATTRIBUTE (|OpenMath|)) | > | |noBranch|))) | > | (|CommutativeRing|)) | > | | > | -- | > | | > | How would I write that type in an argument list in SPAD? | > | > That expression is not closed -- it mentions the free variable #1. | > Assuming it is in scope, it is just | > | > ComplexCategory #1 with | > if #1 has OpenMath then OpenMath | > CommutativeRing | > | | No, I think that must be wrong. Properly prettyprinting the output | getConstructorSignature gives: | | ( | (|Join| (|ComplexCategory| |#1|) | (CATEGORY |package| | (IF (|has| |#1| (|OpenMath|)) | (ATTRIBUTE (|OpenMath|)) | |noBranch| | ) | ) | ) | (|CommutativeRing|) | ) | | CommutativeRing is the source in the type of Complex. The Target is | | ComplexCategory #1 with | if #1 has OpenMath then OpenMath | | So it's type must be written something like | | (R:CommutativeRing) -> ComplexCategory R with | if R has OpenMath then OpenMath You are right. Thank you; I was confused by the formatting. | If I wanted to write a domain that only took functors of this type in | a parameter, could I write the above expression in the parameter list? If the function does not have dependent types (like above), yes -- see examples in the library, e.g. defaults.spad.pamphlet and many other places. For types that are dependent, you have to wait till someone implement dependent contravariant type checking :-) Note that in general AXIOM compilers do not implement contravariant coercions for all functions -- keeping with the tradition that only "trivial" coercions are available in libraries. However, for constructors the situation is special because of the conditionals in exports. | > | Really this issue is: Can I pass a functor as a parameter? | > | > Yes. | > | > | If so, how can I write it's type? | > | > In Spad (library), in a way that respect type expectations. | > See the example in the OpenAxiom repo above. | > | | Thanks. That was quite helpful. I was able to compile and use the following: | | )abbrev package MONADL MonadList | MonadList(A:Type): MonadCat(A,List) == add | unit(x:A):List A == list(x) | join(x:List List A):List A == concat x | mult(x:List A,y:List A):List A == concat(x,y) | | See: http://axiom-wiki.newsynthesis.org/SandBoxMonads#msg20111109124013-0...@axiom-wiki.newsynthesis.org Great! -- 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
