[TYPES] HOAS versus meta reasoning

[Karl Crary]

I see.  You should probably look at Licata, Harper, and Zeilberger's 
paper from the most latest LICS.  They show that you can sort (one might 
say tame) the HOAS issues by taking a view based in focusing (which 
arises from theorem proving).

The basic idea to focusing is to sort the connectives into positive and 
negative.  Positive connectives are eliminated via pattern matching, 
while negative connectives are introduced via pattern matching.  For 
example, sums are positive because they are eliminated using pattern 
matching, but functions are negative because they are introduced using 
pattern matching (on the argument).  Products can be taken either way, 
resulting in two different connectives. (Equivalently, you can view 
positive connectives as ones with a closed-scope elimination form and 
negative connectives as ones with an open-scope elimination form.)

They observe that the representational arrow used in HOAS is not the 
usual negative function space, but a *positive* function space.  The 
positivity of the function space ensures that the function is 
parametric, which higher-order representations depend on.  In essence, A 
-pos-> B refers to a B that is constructed using a new introduction form 
for A.  (Note that A must be atomic; otherwise positive functions would 
be creating new intro forms for connectives.)

Functions that analyze their arguments employ the usual negative 
function space.  Although most existing LF-based systems have (what we 
can now recognize as) negative functions only at a meta-level, there's 
no reason it must be so.  We can integrate positive and negative 
functions into the same system, and there's good reason to do so.

When you do so, the two function spaces can interact in interesting and 
surprising ways.  In short, some of the structural properties that one 
expects can fail when the two are combined.  (I suspect this is the sort 
of thing you are looking to tame.)  Licata, et al.'s framework shows 
exactly when/how this happens, and what you need to do to if you want to 
prevent it from happening.

Their framework also shows that the concern that is sometimes raised 
over negative instances arising in HOAS is really a red herring.  The 
problem, as I understand it, is as follows:  Suppose I take the 
higher-order representation of the lambda calculus:

lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.

and try to make it into a recursive definition.  Then I obtain something 
like:

mu X . (X -> X) + (X * X)

and this doesn't work the way it is supposed to, because of the negative 
occurrence of X.  Consequently, you cannot use HOAS in this manner.

Some people find this mysterious, but the mystery disappears when you 
consider which arrow is being used.  If I use the negative arrow this 
can be fine, but it has nothing to do with HOAS, which relies on the 
positive arrow.  If, on the other hand, I use the positive arrow, then 
this is ill-formed (even if we have recursive types), because the domain 
of a positive function has to be atomic, and therefore cannot be the 
type variable X.

    -- Karl Crary



Andrei Popescu wrote:
> Dear Andrew and Karl, 
>
> I thank you very much for your comments and references.  
>
> To answer Karl's question, I used the word "taming" because, as far as I see, the interaction between meta-reasoning (by which I understand reasoning about the object system) and HOAS is a wild issue.  Going back one level and (case-)analyzing the meta-logic inference itself in a meta-meta logic seems like an elegant, but extreme measure to take  -- for one thing, it breaks the ties with more conventional frameworks for developing mathematics, such as the ones of Coq, Isabelle/HOL or PVS, where a working mathematician feels immediately comfortable (thanks to the standard foundations), and where many libraries of theories are available. Staying in a conventional framework, on the other hand, requires compromises on the hassle-free (i.e., typing-context-free, substitution-free, bound-variables-free etc.) aspect of the representation.  I was not looking for taming any aspect in particular, 
> but for getting a picture of the recent progress within the above approaches and maybe others in between.  
>
> Regards, 
>  Andrei Popescu  
>
>
>