[POPLmark] Lists of binders in HOAS

[Karl Crary]

My attention has been drawn to the following statement on page 6 of the 
Poplmark challenge: "However, our experience also suggests that it is 
often difficult to use HOAS to represent many problems.  For example, 
there are many languages with constructs that require lists of binders 
that do not have any obvious encoding into HOAS."

Of course, I can't refute this conclusively without knowing what you 
have in mind, but lists of binders are no problem at all in HOAS.  For 
example, to define a multi-argument lambda:

term : type.
bterm : type.  %% bound term

lam : bterm -> term.

bterm_none : term -> bterm.
bterm_another : (term -> bterm) -> bterm.

Then you encode \x,y.e as:

    lam (bterm_another ([x] bterm_another ([y] bterm_none (E x y)))).

As far as I know, this technique is quite robust.  So I'm curious, what 
did the challenge authors have in mind?

    -- Karl