[Agda] Re: Issue 897 in agda: unnatural space behavoir of the
mechvel at botik.ru
Tue Sep 17 15:09:18 CEST 2013
On Tue, 2013-09-17 at 10:17 +0000, agda at googlecode.com wrote:
> Status: Fixed
> Comment #1 on issue 897 by nils.anders.danielsson: unnatural space behavoir
> of the checker
> 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
One needs to have a general notion of how to program in Agda on
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
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?
More information about the Agda