[Agda] strictness place

[Philipp Hausmann]

The JavaScript backend is the only exception here I guess, it uses 
strict evaluation. The main reason is that having strict semantics 
matches the JS evaluation model much more closely which simplified the 
backend implementation.

While this is permitted by Agdas semantics, I suspect most existing Agda 
code assumes laziness and there are probably some performance problems 
lurking around when using e.g. the stdlib with a strict evaluation model.

Philipp


On 03/28/2018 11:52 AM, Ulf Norell wrote:
> Both the type checker and the GHC backend are lazy by default. For the 
> type checker
> it would be disastrous to be strict everywhere, since you'd end up 
> evaluating expensive
> proof terms that you don't need to look at. For the run time it's 
> slightly better since many
> of those proof terms will get erased. It is not possible to compile an 
> Agda program with
> (the ghc flag) -XStrict since the GHC backend relies on laziness.
>
> You can manually control strictness using 
> Agda.Builtin.Strict.primForce. This forces
> evaluation of its argument both at compile time and at run time. There 
> is currently no way
> to declare strict constructors like in Haskell.
>
> / Ulf
>
>
>
>
> On Wed, Mar 28, 2018 at 11:34 AM, Nils Anders Danielsson 
> <nad at cse.gu.se <mailto:nad at cse.gu.se>> 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.
>
>         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
>
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180328/373dc868/attachment.html>