[Agda] Re: Issue 897 in agda: unnatural space behavoir of the checker

[Sergei Meshveliani]

On Tue, 2013-09-17 at 10:17 +0000, agda at googlecode.com wrote:
> Updates:
> 	Status: Fixed
> 
> Comment #1 on issue 897 by nils.anders.danielsson: unnatural space behavoir  
> of the checker
> http://code.google.com/p/agda/issues/detail?id=897
> 
> I suspect that you can make the code type-check much faster by
> avoiding the use of "with" in *r-mbCommutativeSemigroup.
> 

Indeed, after changing this `with' to `case' 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  case_of_  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 ?
But  `case 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' with `case',
the type check fails.

Can people advise, please?

Regards,

------
Sergei