Free variable types

By Edwin Westbrook, from TFP 2006, available from Aaron Stump’s website:

Higher-order abstract syntax (HOAS) has been shown to be useful in formal systems for reasoning about programming languages. How to recurse over HOAS representations, however, is a well-known problem. This is because, in most current systems, it is generally impossible to recurse on the body of a λ-abstraction without creating a fresh variable, which must itself be bound. This in turn makes it impossible, for instance, to extract first-order data from higher-order data. One previous approach to this problem has been to allow the creation of fresh variables that are not bound to pass to λ-abstractions as long as they can be shown not to escape their scope. Current systems cannot show these do not escape their scope without a runtime check. In this paper, we propose a novel type system that allows explicit reasoning about free variables. This type system can ensure these fresh variables do not escape their scopes without runtime checks. The usefulness of this approach is shown with a simple example.

0 Responses to “Free variable types”

  1. Leave a Comment

Leave a Reply

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

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

Google photo

You are commenting using your Google 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 )

Connecting to %s

%d bloggers like this: