strict evaluation. The main reason is that having strict semantics
lurking around when using e.g. the stdlib with a strict evaluation model.
Post by Ulf Norell
Both the type checker and the GHC backend are lazy by default. For the
it would be disastrous to be strict everywhere, since you'd end up
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.
On Wed, Mar 28, 2018 at 11:34 AM, Nils Anders Danielsson
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
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.
Agda mailing list
Agda mailing list