Interleaving typechecking and evaluation [Re: [Agda] Recursive Sets / refine vs. load]

[Wolfram Kahl]

On Fri, Mar 30, 2012 at 03:08:42PM +0200, Andreas Abel wrote:
>  [ long calculation ]
> Hoorray, type checked!
> 
> And we did not peek into boxes during evaluation.
> 
> Sharing seems essential.

That sentence caught my attention, so I looked at the calculation more
carefully, but couldn't figure it out: What does ``sharing'' refer to here?


Unrelated to that question, the key step in that calculation
appears, to me, to be the rec-expansion that would be happening
on a not-yet-fully-typechecked term (but with fully type-checked
path from rec to the rec-bound variable occurrence).
Does this assume that the termination checking could/would be done
on such terms, too?


Wolfram