#88 cannot form Join

[Bill Page]

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?

[Bill Page]

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]

MonadCat

[Bill Page]

domain MySet

[Bill Page]

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]

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.