#88 cannot form Join

1.5.0
open-accepted
compiler (16)
5
2011-12-05
2011-12-02
Bill Page
No

This category:

)abbrev category MONADC MonadCat
MonadCat(A : Type, M: Type -> Type): Category == with
if A has SetCategory then SetCategory
fmap: (A->A, %) -> %
unit: A -> %
join: M % -> %
mult: (%, %) -> %
--

Compiles OK. But using it here:

)abbrev domain MYSET MySet
MySet(T:SetCategory): Join(MonadCat(T,MySet),SetAggregate(T)) with
finiteAggregate
--join: MySet MySet T -> MySet T
== add
Rep == List T
--rep(x:%):Rep == x pretend Rep
--per(x:Rep):% == x pretend %

Rep2 := List List T
rep2(x:MySet MySet T):Rep2 == x pretend Rep2
per2(x:Rep2):MySet MySet T == x pretend MySet MySet T

coerce(x:%):OutputForm == brace [i::OutputForm for i in rep x]
x = y == rep(x) = rep(y)
construct(x) == per removeDuplicates(x)$Rep
parts(x:%):List T == rep x
join x == construct concat rep2 x
--

results in:

Compiling OpenAxiom source code from file
/var/zope2/var/LatexWiki/4350417341717496175-25px002.spad using
Spad compiler.
MYSET abbreviates domain MySet
------------------------------------------------------------------------
initializing NRLIB MYSET for MySet
compiling into NRLIB MYSET
Semantic Errors:
[1] cannot form Join of: ((MonadCat T$ MySet) (SetAggregate T$) (CATEGORY package (ATTRIBUTE finiteAggregate)))

****** comp fails at level 4 with expression: ******
(|Join| (|MonadCat| T$ |MySet|) (|SetAggregate| T$)
(CATEGORY |package| (ATTRIBUTE |finiteAggregate|)))
****** level 4 ******
$x:= (MySet #1)
$m := Type

>> Apparent user error:
Cannot coerce #1 of mode Type to mode SetCategory

--

Is it really user error?

Discussion

  • Bill Page
    Bill Page
    2011-12-02

    • milestone: --> 1.5.0
     
  • Bill Page
    Bill Page
    2011-12-02

    With Revision: 2514 I get a different error:

    (1) -> )co myset.spad
    Compiling OpenAxiom source code from file
    /export/disk1/wspage/myset.spad using Spad compiler.
    MYSET abbreviates domain MySet
    ------------------------------------------------------------------------
    initializing NRLIB MYSET for MySet
    compiling into NRLIB MYSET
    STYLE-WARNING: redefining BOOT::|MonadCat;| in DEFUN

    >> System error:
    The value NIL is not of type DATABASE.

     
  • Bill Page
    Bill Page
    2011-12-02

    MonadCat

     
    Attachments
  • Bill Page
    Bill Page
    2011-12-02

    domain MySet

     
    Attachments
  • Bill Page
    Bill Page
    2011-12-05

    The original error message
    Semantic Errors:
    [1] cannot form Join of: ((MonadCat T$ MySet) (SetAggregate T$) (CATEGORY package ( ATTRIBUTE finiteAggregate)))
    ...

    was generated by OpenAxiom 1.4.x revision: 2461 with the example code.

    This variant

    MonadCat(A : SetCategory, M: SetCategory -> SetCategory): Category == with
    join: M M A -> M A

    gives a different result: with the same revision

    >> System error:
    Control stack exhausted (no more space for function call frames).
    This is probably due to heavily nested or infinitely recursive function
    calls, or a tail call that SBCL cannot or has not optimized away.

    PROCEED WITH CAUTION.

    and the database error in the more recent revision of trunk.

     
  • I cannot reporduce th "NIL DATABASE" error with 1.4.x. I have not tried trunk yet but I would be surprised if there is a difference.

    As for the "apparent user error", this is related to the dependent contravariant coercion I mentioned in this mail

    http://sourceforge.net/mailarchive/message.php?msg_id=28388586

     
    • status: open --> open-accepted
     
  • Looking closer at the definition of MySet, there is one construct that I cannot make sense (and I suspect that is what is also tripping the compiler) . It is

    MonadCat(T,MySet)

    at the point where MySet is used, we do no even know yet what its type is! So,
    type checking its uses as argument to MonadCat is not well defined.