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? | | -- | )abbrev category MONADC MonadCat2 | MonadCat2(C: Type, A : C, M: C -> C): Category == with | unit: A -> M A | mult: (M A, M A) -> M A | -- | | )show MonadCat2 | | MonadCat2(C: Type,A: t#1,M: (t#1 -> t#1)) is a category constructor | Abbreviation for MonadCat2 is MONADC | This constructor is exposed in this frame. | ------------------------------- Operations -------------------------------- | mult : (M(A),M(A)) -> M(A) unit : A -> M(A) | | | In principle would could instantiate MonadCat2 as follows: | | MonadCat2(SetCategory, Integer, (X:SetCategory):SetCategory+->List X) | | but we can not write this in FriCAS, so try to use Type instead. | | -- | )abbrev domain MONDIL MonadIntegerList | MonadIntegerList(): MonadCat2(Type, Integer, (X:Type):Type+->List X) == add | unit(x:Integer):List Integer == list(x) | mult(x:List Integer,y:List Integer):List Integer == concat(x,y) | -- | | Notice here that I explicitly attempted to construct a function which | returns a domain: | | (X:SetCategory):SetCategory +-> List X | | 'List' is the domain constructor (functor), but both FriCAS and Aldor | complain in various ways. Maybe someone else can find a variant that | does compile? Bill -- I think this essentially goes back to a discussion we had recently. I am not sure I succeeded in getting my points trough:-) 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. 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. 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. 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. -- 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
