A universe of binding and computation

Daniel Licata and Robert Harper, from ICFP 2009, available from Harper’s website.

In this paper, we construct a logical framework supporting datatypes that mix binding and computation, implemented as a universe in the dependently typed programming language Agda 2. We represent binding pronominally, using well-scoped de Bruijn indices, so types can be used to reason about the scoping of variables. We equip our universe with datatype-generic implementations of weakening, substitution, exchange, contraction, and subordination-based strengthening, so that programmers are provided these operations for free for each language they define.

In our mixed, pronominal setting, weakening and substitution hold only under some conditions on types, but we show that these conditions can be discharged automatically in many cases. Finally, we program a variety of standard difficult test cases from the literature, such as normalization-by-evaluation for the untyped lambda-calculus, demonstrating that we can express detailed invariants about variable usage in a program’s type while still writing clean and clear code.

A video of Daniel Licata’s presentation at ICFP is available here.

1 Response to “A universe of binding and computation”

  1. 1 Samuel Gélineau October 7, 2009 at 1:46 am

    As usual, here’s how to count variable occurrences using the paper’s approach.

    -- first, define lambda calculus terms.
    -- this is a bit tedious since fragments need to be added
    -- in a couple of different places.
     module DefinedAtoms where
    +  termA : Atom
    +  world termA = True
    +  eq termA termA = True
    +  eq-refl termA = _
    +  certify-eq {termA} {termA} c = Refl
     module Sig where
    +  term = D⁺ termA
    +  lam : InΣ (termA ⇐ termC ⇒ term)  -- (termC ⇒ term) -> termA
    +  app : InΣ (termA ⇐ term ⊗ term)   -- term ⊗ term    -> termA
    +  premises termA = typeof lam :: typeof app :: []
    +  certify-premises lamm = i0        -- 0th constructor
    +  certify-premises appp = iS i0     -- (suc 0)th constructor
    -- next, count the variable occurrences.
    -- "∀⇛" quantifies over all contexts Γ.
    -- "⊃" is a computational arrow, while
    -- "⇒" is a syntactic arrow, which augments the context.
    -- thus the term we are examining has context (Γ ,, termC).
    -- the "□" in the result type means that we return
    -- closed nats, even though the context is Γ.
    cnt : ∀⇛ (termC ⇒ term) ⊃  □ nat
    cnt Γ (▹ i0)     = succ · (zero · _)  -- one for first var
    cnt Γ (▹ (iS _)) = zero · _           -- zero for others
    cnt Γ (app · (e1 , e2)) = cnt Γ e1 + cnt Ψ e2
    cnt Γ (lam · e)  = cnt (Γ ,, termC)         -- augment context
                           (exchange2 term Γ e) -- while keeping var
                                                -- in first position
    -- if we want, we can now turn the closed nats into ordinary
    -- Nat values, defined outside of the framework.
    nat-to-Nat : ⊡ nat → Nat
    nat-to-Nat (zero · _) = 0
    nat-to-Nat (succ · n) = 1 + nat-to-Nat n
    nat-to-Nat (▹ x)      = impossible x
    -- special case when the context is ([] ,, termC), of size one.
    countV : ⊡ (termC ⇒ term) → Nat
    countV e = nat-to-Nat (cnt [] e)

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: