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

[Andreas Abel]

Hello Wolfram,

On 30.03.12 3:50 PM, Wolfram Kahl wrote:
> On Fri, Mar 30, 2012 at 03:08:42PM +0200, Andreas Abel wrote:
>> 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?

In this case, I used 'let' to express sharing, but one could use a dag 
structure.  The thing is, you do not want to duplicate an expression 
that is only half type-checked, otherwise you duplicate the effort of 
type-checking.

> 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?

If one uses type-based termination, then the problem of termination 
checking is mostly subsumed into type checking.  However, if one infers 
the termination order, I guess unfolding of recursion needs to be 
blocked until the termination has been guaranteed.  Currently, we don't 
do this, during type checking Agda believes everything is terminating, 
only then she checks termination.

Cheers,
Andreas


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/