[POPLmark] Lists of binders in HOAS

[David Walker]

Hi,

I started lurking here after being told there was considerable excitement on
the poplmark list....

Karl, I would love to see your solution for a collection of mutually
recursive multi-argument functions.  ie, encode the syntax, typing relation
and operational semantics of something like:


tp ::= unit | (tp,...,tp) -> tp

f ::= fun x (x:tp,...,x:tp):tp = e   (* recursive function *)

fs ::= f | f and fs                      (* mutually recursive *)

e ::= x | () | let fs in e | e e

I suppose you must already have something like this for your formalization
of the definition of standard ML.  If you could show me this little piece,
I'd be very interested.  The obvious difficulty here is that the scopes of
the function variables do not follow the syntactic structure of the
pseudo-BNF definition given above.  Therefore, to do a HOAS formalization,
it seems you have to lift introduction of the function variables above the
group of mutually recursive function definitions.  In addition, you may need
some trick to use the framework's definition of substitution to implement
the substitutions necessary for implementing the operational semantics of
function application. 

I hope your encoding is just as elegant as the HOAS encodings of
non-recursive functions.  Is the proof of adequacy also equally simple?
That would be great!

Thanks,
Dave

> -----Original Message-----
> From: poplmark-bounces at lists.seas.upenn.edu [mailto:poplmark-
> bounces at lists.seas.upenn.edu] On Behalf Of Karl Crary
> Sent: Monday, May 09, 2005 1:01 PM
> To: poplmark at lists.seas.upenn.edu
> Subject: [POPLmark] Lists of binders in HOAS
> 
> 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
> 
> _______________________________________________
> Poplmark mailing list
> Poplmark at lists.seas.upenn.edu
> http://lists.seas.upenn.edu/mailman/listinfo/poplmark