[Agda] strictness place

[Nils Anders Danielsson]

On 2018-03-28 10:54, Sergei Meshveliani wrote:
> can you, please explain, what is the relation between laziness and
> strictness in Agda?

Agda is a language in which every program is productive (in the absence
of bugs, when the termination checker has not been turned off, etc.).
This gives quite a bit of freedom to those implementing compiler
backends for Agda, and different backends take different approaches.

I think you are mainly using the GHC backend. This backend uses lazy
evaluation.

> Is Agda ready to take the option "do everything strict in type checking
> and in the executable code" ? what will be a real effect?

It would be easy to make all *inductive* constructors strict in the GHC
backend. This might be beneficial for code written in a certain way, but
it could also hurt performance for code that includes proof terms that
are not erased.

I guess it would also be possible to make more function applications
strict. However, if you make, say, if_then_else_ strict, then you could
incur a substantial performance penalty.

-- 
/NAD