[TYPES] HOAS versus meta reasoning

[Dan Licata]

Hi Andrei,

On Nov17, Andrei Popescu wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> This "naive" hope driven style of inquiry becomes sharper, in my
> opinion, when we move from representing syntax to representing
> inference, and I think the latter is an equally important aspect of
> HOAS which unfortunately is not transparent in the name "HOAS". 

We've used the term "higher-order judgements" for this on the Twelf Wiki.

> Consider a typing system with a familiar rule for typing abstraction,
> like
> 
> Gamma, x : A |- Y : B
> ----------------------------
> Gamma |- Lam(x:A,Y) : A -> B
> 
> In idealized HOAS, one would represent it as something like
> 
> (All x. typeOf(x,A) => typeOf(Y x,B)) =>
> typeOf(Lam(A,Y), Arrow(A,B))     (*) 

Here is this example in Twelf:

http://twelf.plparty.org/wiki/Higher-order_judgements

> When and where is it sound? 
> 
> And, if so:
> 
> When and where can it be viewed as something like an inductive clause 
> (just like its object-level counterpart)?  
> 
> The answers in the style of the Miller-McDowell and Twelf approaches
> are instances of the following: consider a further meta-level layer
> and from there you can regard this clause (via its associated rule on
> sequents in the representation logic) as an inductive clause.

I won't speak for Miller-McDowell, but in LF, this clause is a generator
that helps populate the LF base type 'typeOf'.  So when you consider the
canonical LF terms of type 'typeOf(E,T)', one case will be that the term
has the form

  of-lam (\x.\dx.D(x,dx))

where

  \x.\dx.D(x,dx) 

is an LF function of type

  Pi x. typeOf(x,A) => typeOf(Y x,B)  

I think of LF as a fancy version of the ML datatype mechanism, one that
gives you two new ingredients: (1) a notion of binding and scope, and
(2) dependent types.

> However, isn't this shifting the burden of handling contexts from the
> contexts of the object logic to the ones of the representation logic?

If I understand you correctly, then yes, and that's a good thing!  By
representing the object language context as the LF context, you can inherit
properties like substitution from LF.  See this page for a little explanation:

http://twelf.plparty.org/wiki/Substitution


I hope that answers some of your questions,

-Dan