Specifications

[zickgraf]

I wonder which of the following specifications should hold true for a category C and L := LazyCategory( C ):

1. IsEqualForObjects( DirectProduct( a / L, b / L ), DirectProduct( a, b ) / L ) for all objects a and b in C (of course, DirectProduct is just an example)
2. IsEqualForObjects( Source( morphism ), Source( EvaluatedCell( morphism ) ) / L ) for all morphisms morphism in L.
3. IsEqualForObjects( EvaluatedCell( Source( morphism ) ), Source( EvaluatedCell( morphism ) ) for all morphisms morphism in L.

From looking at the code I assume that 1. and 2. should not hold true, but I expect that 3. should be true.

[zickgraf]

I extend my question further:
4. IsEqualForObjects( EvaluatedCell( DirectProduct( a / L, b / L ) ), DirectProduct( a, b ) ) for all objects a and b in C

This is probably the most important one: if it should hold true it restricts the possible optimizations which we are allowed to make in L (e.g. the current optimization for FiberProduct would be invalid). If it need not hold true, it means that we cannot mix computations made with LazyCategories and computations made without LazyCategories.

[mohamed-barakat]

The answers are (generically): 1. false, 2. false, 3. true, 4. true

[mohamed-barakat]

I do not see the significance of 4. as IsEqualForObjects is called in the category underlying the lazy category.

[zickgraf]

Thanks for the quick response! Consider the following example (where I have replace DirectProduct by FiberProduct):

LoadPackage( "LazyCategories" );
LoadPackage( "FinSetsForCAP" );
M := FinSet( [ 1, 2 ] );
id := IdentityMorphism( M );
phi := MapOfFinSets( M, [ [ 1, 1 ], [ 2, 1 ] ], M );
L := LazyCategory( FinSets : show_evaluation := true );

IsEqualForObjects( EvaluatedCell( FiberProduct( phi / L, id / L ) ), FiberProduct( phi, id ) );

where the last line yields false, since the object in the lazy category has changed due to the optimization.

[mohamed-barakat]

Why is this bad?

[zickgraf]

It's not necessarily bad. It's unexpected if one thinks of LazyCategories as a completely transparent wrapper (in the sense that once I evaluate I get exactly the same result as if I had never lazified anything), that's why I asked for the specification.

If LazyCategories is not a completely transparent wrapper, you cannot mix computations from the lazy and the non-lazy world. And if such optimizations would be part of CompilerForCAP, there would be some additional implications:

1. Compiled and non-compiled code might produce different results.
2. If the compiler is enabled, every piece of code has to go through the compiler, even the code the user types in the command line.
3. If the compiler misses an optimization (for example because it is hidden in some user-provided function which is not resolved, or because there is some complicated for-loop the compiler cannot handle) it produces wrong results.
4. The compiler implicitly changes the notion of equality (e.g. it would distinguish between a morphism given by IdentityMorphism and a morphism which happens to be the identity by chance, exactly like LazyCategories does). And this changed notion of equality might not be apparent in the compiled code anymore.

Again, this is not necessarily bad, I'm just trying and to understand and write down my thoughts about the implications :-)