unnatural space behavoir of the checker

[UlfNorell]

From mech...@botik.ru on September 07, 2013 13:49:50

This is on Agda of darcs August ~20 2013, MAlonzo, lib-0.7.

It concerns an unnatural space behavoir of the type checker.

This attached project is type-checked by

 agda -c $agdaLibOpt +RTS -K90m -M8000m -RTS  Main.agda

The space measurement concerns only the module ResidueI.Ring in ResidueI/Ring.agda, more precisely, the definition of r-mbCommutativeSemigroup in the end: r-mbCommutativeSemigroup : Maybe (CommutativeSemigroup {α} {ℓp} rUpSemigroup) r-mbCommutativeSemigroup with Magma.mbCommutative rMagma ... | just (yes comm) = just (record{ commutative = *comm }) ... | _ = nothing

All other modules need to be type-checked earlier, so that the checker would report for them "Skipping ...".

1. -M7000m is not sufficient to type-check ResidueI.Ring, -M8000m is sufficient, and takes long to type-check.
2. After commenting out *r-mbCommutativeSemigroup, it suffices -M700m (about 11 times ratio for such a small definition).

Can the checker be improved concerning such an effect?

As *r-mbCommutativeSemigroup is small, I expect the code can be changed so that -M900m will be sufficient.

How to change?

May be, some large definition bodies are inserted into *r-mbCommutativeSemigroup. May be, the word `abstract' will help. But the lengthy implementation segments that could be abstracted are not at the top scope level.

Can you give and advice - with respect to this concrete code?

Remark. To make this report smaller, many implementation segments in the real application are replaced with `postulate'.

Attachment: repSep2013.zip

Original issue: http://code.google.com/p/agda/issues/detail?id=897

[UlfNorell]

From nils.anders.danielsson on September 17, 2013 03:16:56

I suspect that you can make the code type-check much faster by avoiding the use of "with" in *r-mbCommutativeSemigroup.

Status: Fixed

[UlfNorell]

From mech...@botik.ru on September 17, 2013 06:08:48

Indeed, after changing this with' tocase' its type check takes ~11 times less memory (700 Mb instead of 8000).

But I need a general understanding: when to use with' and when to use case'. One needs to have a general notion of how to program in Agda on practice. In Haskell, I had not such cost problems.

Well, `with' is a language construct, and caseof is a library operator (implemented by a function). But this mere note does not explain the cost effect.

May be, with foo' inserts there the body of foo ? Butcase foo of \' also could insert various bodies, it depends on the checker implementation details.

Is this cost difference due to occasional checker implementation details or it is a fundamental feature which will preserve in further implementations?

Can you provide a simple program in which "with foo" takes about 10 times more space to type-check than "case foo of" ?

Also there are many places where I fail to replace with' withcase', the type check fails.

Can people advise, please?

[UlfNorell]

From nils.anders.danielsson on September 19, 2013 05:36:35

This discussion has moved to the Agda list.

[UlfNorell]

From andres.s...@gmail.com on November 11, 2013 06:36:40

Labels: Type-Enhancement