[Agda] about serialization

[Ulf Norell]

Your code turns into (roughly)

module M1 where
  M11.f : (p : ℕ) → ℕ → ℕ
  M11.f p x = p + x

module M2 where
  f = M1.M11.f 2
  g : ℕ → ℕ
  g x =  f (suc x)

No normalisation takes place.

/ Ulf

On Thu, Mar 30, 2017 at 10:20 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> Dear Agda developers,
>
> consider the modules  M1.agda and M2.agda  of
>
> ---------------------------------------
> module M1 where
> open import Data.Nat using (ℕ; _+_)
>
> module M11 (p : ℕ)
>   where
>   f : ℕ → ℕ
>   f x =  p + x
>
> ----------------------------------------
> module M2 where
> open import Data.Nat using (ℕ; suc)
> open import M1       using (module M11)
>
> open M11 2 using (f)
>
> g : ℕ → ℕ
> g x =  f (suc x)
> -----------------------------------------
>
> And suppose that  M1  is type-checked earlier.
>
> 1) Then, how eager is the type checker in processing the definition
>    for  g ?
>
> Probably, it substitutes 2 into the body of  M11, and into  f,
> and it becomes
>        f x = 2 + x.
>
> Then it normalizes everything, and f  becomes  f x = suc (suc x).
>
> Then it substitutes the obtained definition for f into the definition
> for  g,  and normalizes this to
> g x = suc (suc (suc x)).
>
> Right?
>
> Or may be, it delays the above operations for where  g  is used?
>
> 2) If we comment out the last two lines for  g,
>    then will the type checker do the above substitution into M11 and
> normalization for the definition of  f ?
>
> Thanks,
>
> ------
> Sergei
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170331/3130d831/attachment.html>