[Agda] how does BUILTIN work - practical programming in Agda

[Nils Anders Danielsson]

On 2011-12-04 20:13, Silvio Frischknecht wrote:
> 2) While using haskell types to compute fibonacci numbers I also
> stumbled over the lake of a seq function. Is there a portable way to
> force eager evaluation?

Agda compilers are free to choose whatever evaluation order they like,
as long as they don't change the meaning of the program. The JavaScript
and Epic backends currently use strict evaluation (for inductive types),
whereas the MAlonzo backend uses lazy evaluation (modulo whatever
strictness optimisations GHC applies).

If you're using a "strict" backend, then you should remember that
functions like if_then_else_ compute all arguments strictly.

> Because I got a stack overflow when using big numbers. Which i fixed
> by also importing seq from haskell, which is again not portable.

Introducing seq in this way also has another disadvantage: the
type-checker does not reduce seq a b to b.

I guess it would be easy to add a seq primitive which does reduce.
However, this might be error-prone: the type-checker may decide to
reduce an occurrence of seq, thus turning strict code non-strict.

> 3) when compiling agda is it correct to specify -i darcsdir/src?
> Because that would mean that Everything.agda is outside.

 From README.txt:

   Note that all library sources are located under src or ffi. The
   modules README, README.* and Everything are not really part of the
   library, so these modules are located in the top-level directory
   instead.

-- 
/NAD