[Agda] strictness place

[Wolfram Kahl]

On Wed, Mar 28, 2018 at 11:34:56AM +0200, Nils Anders Danielsson wrote:
> 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.

(To be more precise, it uses lazy evaluation on a translation of
 the original code that eliminates most of the sharing a Haskell
 programmer would expect, see e.g.:

   https://github.com/agda/agda/issues/1895

 I hope I'll get back to working on that some time this summer...
)


Wolfram