[Agda] strictness place

[Sergei Meshveliani]

Dear Agda developers,

can you, please explain, what is the relation between laziness and
strictness in Agda?

Which is the default? Which is favorite?
Have they equal rights?

Where strictness can appear? Does the type checker process strictness?
Does the compiler process strictness?

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

(As I recall, Haskell needs to define `strict' separately for each
particular constructor or function application, so that `lazy' and
`strict' have not equal rights).

Is it true that Agda only transmits strictness annotations to the
Haskell code, and then GHC processes these annotation according to the
Haskell rules?

So far, I am not going to use strictness explicitly.
But sometimes I say "Agda has lazy evaluation", and some people object
as "no, it also has a strict back-end ...".
So that I need to have an idea.
Probably, it needs to be "Agda has lazy evaluation as default and
favorite" (?)

Thanks,

------
Sergei

[Nils Anders Danielsson]

Post by Sergei Meshveliani
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.

Post by Sergei Meshveliani
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.

[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

Post by Nils Anders Danielsson

Post by Sergei Meshveliani
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

Post by Sergei Meshveliani
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
https://lists.chalmers.se/mailman/listinfo/agda

[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

Post by 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
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
https://lists.chalmers.se/mailman/listinfo/agda
<https://lists.chalmers.se/mailman/listinfo/agda>
_______________________________________________
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Wolfram Kahl]

Post by Nils Anders Danielsson

Post by Sergei Meshveliani
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