On Fri, Nov 11, 2011 at 1:37 AM, Gabriel Dos Reis wrote:
> Bill Page writes:
>
> | > IMList(): Monad(Integer,List) == add
> | > unit ( x:Integer ): List Integer == list x
> | > mult ( x: List List Integer ): List Integer = concat x
> |
> | Note especially the 2nd argument to Monad.
>
> In OpenAxiom, the second argument does not match the expected type.
>
That is clear. Hence my question concerning the type of 'List'.
> |
> | 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', but you are going
to tell me that it *is* a function of type 'Type->Type', '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), ... )'.
As written, 'List' is not an endofunctor but it can be considered as
such if we are willing to forget about what it exports.
> | 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, 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.
> | 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
> ...
> 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
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?
> | 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
Regards,
Bill Page.
------------------------------------------------------------------------------
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
