[Agda] delaying computation to run time

[mechvel at scico.botik.ru]

On 2020-01-15 16:25, Nils Anders Danielsson wrote:
> 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"));


Does CAF abbreviate a Constant Applicative Form ?

Is  s  below a CAF ?
------------------------
size : Tree → ℕ
size leaf        = 1
size (node t t') = size t + size t'

example = perfect-tree-of-depth 50

s = size example
------------------------


I observe that under the above context the program
----------------------------------------
main : IO ⊤
main = putStrLn (toCostring (showℕ s))
----------------------------------------

is type-checked and compiled fast, and runs very long at the run time
(because (size example) loops about 2^50 steps when computed).

On the other hand, if we add to the program
-----------------------
lemma : (s + 1) ∸ s ≡ 1
lemma = refl
-----------------------

then it is type-checked very long. Probably it computes  s ...
Is `lemma' a CAF ?

Thanks,

------
Sergei





lemma : (s + 1) ∸ s ≡ 1
lemma = refl


main : IO ⊤
main = putStrLn (toCostring (showℕ n))
---------------------------------------