A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions

Brigitte Pientka, from POPL 2008, available from Brigitte Pientka’s website.

Higher-order abstract syntax (HOAS) is a simple, powerful technique for implementing object languages, since it directly supports common and tricky routines dealing with variables, such as capture-avoiding substitution and renaming. This is achieved by representing binders in the object-language via binders in the meta-language. However, enriching functional programming languages with direct support for HOAS has been a major challenge, because recursion over HOAS encodings requires one to traverse lambda-abstractions and necessitates programming with open objects.

We present a novel type-theoretic foundation based on contextual modal types which allows us to recursively analyze open terms via higher-order pattern matching. By design, variables occurring in open terms can never escape their scope. Using several examples, we demonstrate that our framework provides a name-safe foundation to operations typically found in nominal systems. In contrast to nominal systems however, we also support capture-avoiding substitution operations and even provide first-class substitutions to the programmer. The main contribution of this paper is a syntax-directed bi-directional type system where we distinguish between the data language and the computation language together with the progress and preservation proof for our language.

4 Responses to “A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions”


  1. 1 Samuel Gélineau October 4, 2009 at 10:27 pm

    I think that, to get a glimpse of each technique, it would be useful to implement a common example with each of the proposed techniques. What could be the hello-world of name binding? I suggest counting occurrences of a particular variable in open expressions of untyped lambda calculus. Here’s how to do it with the technique introduced in this paper (assuming HTML doesn’t destroy the indentation).

    -- first, define lambda calculus terms
    term : type
    lam : (term -> term) -> term
    app : term -> term -> term
    
    -- next, count the variable occurrences
    rec countV : Pi gamma. exp[gamma] -> exp[gamma] -> nat =
    Lambda {gamma} =>      -- Lambda abstracts over contexts
    fn var => fn exp =>  -- whereas fn abstracts over open terms
    case var of
      box(gamma. p[gamma]) =>  -- lowercase p matches a variable name
        case exp of
          box(gamma. lam \x. E[gamma,x:term]) =>
            countV                         -- recur
              {gamma,x:term}               -- on a larger context
              box(gamma,x:term. p[gamma])  -- weakening the var name
              box(gamma,x:term. E[gamma,x:term])
        | box(gamma. app E1[gamma] E2[gamma]) =>
            countV {gamma} var box(gamma. E1[gamma]) +
            countV {gamma} var box(gamma. E2[gamma])
        | box(gamma. q[gamma]) =>  -- a variable!
                                   -- is this the variable we want?
                                   -- let's check: open terms can
                                   -- be compared for equality
            if box(gamma. p[gamma]) = box(gamma. q[gamma])
            then 1
            else 0
    | box(gamma. E[gamma]) => error  -- var isn't even a variable
    
  2. 2 Name Binding Admin October 5, 2009 at 10:01 am

    That’s a nice idea, Samuel. Thanks for that, and sorry for the delay in approving your messages (I didn’t realise comment moderation was turned on).

    I’ve added a link to your blog on the “Blogroll” section.

    • 3 Samuel Gélineau October 5, 2009 at 1:53 pm

      Thanks!

      There’s no “edit” button on my side, so I can’t add the required “<pre>” tag around my code. As an administrator, do you have an easy way to do it, or should I just post a corrected version?

  3. 4 Name Binding Admin October 5, 2009 at 3:03 pm

    OK, done. There seems to be no way (in the “free version” of WordPress) to allow a user to edit their own comments.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s





%d bloggers like this: