[Agda] delaying computation to run time

[Nils Anders Danielsson]

On 2020-01-15 13:58, mechvel at scico.botik.ru wrote:
> e is introduced because without inputting it, the example would be computed at the type
> check time, which will be very expensive (gBasis-ext is expensive to compute).
> Will it?

Agda does not normalise all "CAFs". Here is a simple example:

   module Example where

   open import Agda.Builtin.Nat

   data Tree : Set where
     leaf : Tree
     node : Tree → Tree → Tree

   perfect-tree-of-depth : Nat → Tree
   perfect-tree-of-depth zero    = leaf
   perfect-tree-of-depth (suc n) = node t t
     where
     t = perfect-tree-of-depth n

   example : Tree
   example = perfect-tree-of-depth 1_000_000_000

The GHC and JS backends compile example to the following two pieces of
Haskell/JavaScript code:

   d18 = coe d8 (coe (1000000000 :: Integer))

   exports["example"] = exports["perfect-tree-of-depth"](agdaRTS.primIntegerFromString("1000000000"));

-- 
/NAD