#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

     
  • Bill Page

    Bill Page - 2011-12-02

    domain MySet

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

     
  • Gabriel Dos Reis

    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

     
  • Gabriel Dos Reis

    • status: open --> open-accepted
     
  • Gabriel Dos Reis

    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.

     

Log in to post a comment.

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks