Syntax for free: representing syntax with binding using parametricity

Robert Atkey, from TLCA 2009, available from Robert Atkey’s website.

We show that, in a parametric model of polymorphism, the type ∀α.((α → α) → α) → (α → α → α) → α is isomorphic to closed de Bruijn terms. That is, the type of closed higher-order abstract syntax terms is isomorphic to a concrete representation. To demonstrate the proof we have constructed a model of parametric polymorphism inside the Coq proof assistant. The proof of the theorem requires parametricity over Kripke relations. We also investigate some variants of this representation.

Slides from the TLCA presentation are available here.

1 Response to “Syntax for free: representing syntax with binding using parametricity”

  1. 1 Samuel Gélineau October 6, 2009 at 7:12 pm

    As usual, here’s how to count variable occurrences with the technique introduced in this paper.

    -- first, define lambda calculus terms
    Term : Set → Set
    Term a = (lam : (a → a) → a)
           → (app : a → a → a)
           → a
    -- next, count the variable occurrences.
    countV : (∀ a → a → Term a) → Nat
    countV e = e Nat count-var
      count-lam = λ body → body 0
      count-app = λ e₁ e₂ → e₁ + e₂
      count-var = 1

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 )

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: