[Agda] evaluation in compilation

Nils Anders Danielsson nad at chalmers.se
Wed Oct 3 16:52:10 CEST 2012

On 2012-10-03 16:35, Serge D. Mechveliani wrote:
> Why do the developers talk of slowness, of call by name?
> Does this refer only to evaluation during compilation?

Call-by-name is (currently) used by the type-checker. The MAlonzo
backend uses whatever GHC uses. (If we wanted to we could add lots of
strictness annotations, but this is not done at the moment.)


More information about the Agda mailing list