[Agda] strictness place

[Ulf Norell]

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>
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
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180328/fa1b5204/attachment.html>