Names For Free

Polymorphic Views of Names and Binders

Nicolas Pouillard
IT University of Copenhagen

(joint work with)
Jean-Philippe Bernardy
Chalmers University of Technology and University of Gothenburg

2013-09-23, Haskell Symposium, Boston


Functional programming?

Easy equational reasoning!

Dysfunctional programming?

Not awesome...

Programming with names and binders?

It's hard...

Nested data types?

Containers for free-variables!

Arithmetic with
de Bruijn indices

Not awesome...
(error prone)

Functors & Monads?

Safe and easy to rename and substitute!


Theorems for free!

Incoherent Type Class Instances?

Almost awesome!
(when it works)

Nested Abstract Syntax


data Tm a where
  Var  a  Tm a
  App  Tm a  Tm a  Tm a
  Lam  Tm (Succ a)  Tm a

-- λ f → λ x → f x
apN  Tm Zero
apN = Lam $
        Lam $
          Var (Old $ New ()) `App` Var (New ())

Library Types

type Succ a = a ▹ () -- ≅ Maybe a

data a ▹ v = Old a | New v -- ≅ Either a v

mapOld   a b v. (a  b)  (a ▹ v)  (b ▹ v)
mapNew   a v w. (v  w)  (a ▹ v)  (a ▹ w)

Our proposal

Building terms (step 1)

Example: λ f → λ x → f x

-- Baseline: Nested Abstract Syntax
apN  Tm Zero
apN = Lam $   {- Tm (Succ Zero)        -}
        Lam $ {- Tm (Succ (Succ Zero)) -}
          Var (Old $ New ()) `App` Var (New ())
-- More readable and safe!
apTm_  Tm Zero
apTm_ = lam $ λ f 
          lam $ λ x 
            Var (Old (New f)) `App` Var (New x)
-- HOAS style using a smart-constructor: `lam`
lam   a. ( v. v  Tm (a ▹ v))  Tm a
lam f = Lam (f ())

Building terms (step 2)

Example: λ f → λ x → f x

-- Baseline: step 1
apTm_  Tm Zero
apTm_ = lam $ λ f 
          lam $ λ x 
            Var (Old (New f)) `App` Var (New x)
-- No counting anymore using the `var` smart-constructor
apTm = lam $ λ f 
         lam $ λ x 
           var f `App` var x
-- Hiding away the Old/New injections
var   a v. (v ∈ a)  v  Tm a
var = Var . inj
  -- where inj ∷ ∀ a v. v ∈ a → v → a
  --       inj ≈ (Old)ⁿ . New

Matching terms

Decide if a given term is of the form:
λ x → M x (where x fresh-for M)

Piece of cake!

canEta  Tm Zero  Bool
canEta (Lam e) = unpack e $ λ x t  case t of
  App e1 (Var y)  y `isOccurrenceOf` x &&
                   x `freshFor` e1
  _  False
canEta _ = False

Type Isomorphisms

∀ v. v → f (a ▹ v)

f (a ▹ ())

∃ v. (v, f (a ▹ v))

Thanks to parametricity! Proved in Agda!

Core Library Interface

-- Used in place of your Var constructor
var      f a v. (v ∈ a, Monad f)  v  f a

-- Builds an abstraction and provides you with a _fresh_ name
mkAbs    f a. ( v. v  f (a ▹ v))  f (Succ a)

-- Concretises an abstraction with your given name/value
atVar    f a v. Functor f  f (Succ a)  v  f (a ▹ v)

-- Builds an abstraction with your given name
pack     f a v. Functor f  v  f (a ▹ v)  f (Succ a)

-- Opens an abstraction and provides you with a name and a body
unpack   f a r. f (Succ a)  ( v. v  f (a ▹ v)  r)  r

-- Weakens a Term (Functor)
wk       f a b. (Functor f, a ⊆ b)  f a  f b

-- Test occurrences across different scopes
isOccurrenceOf   a v. (Eq a, v ∈ a)  a  v  Bool


lam   a. ( v. v  Tm (a ▹ v))  Tm a
lam f = Lam (mkAbs f) -- Same as: Lam (f ())

lamP   v a. v  Tm (a ▹ v)  Tm a
lamP x t = Lam (pack x t)

Term structure

Renaming and functors

instance Functor Tm where
  {- ... -}

rename0   a. Eq a  (a, a)  a  a
rename0 (x,y) z | z == x    = y
                | otherwise = z

rename   f a. (Functor f, Eq a)  (a, a)  f a  f a
rename = fmap . rename0

swap0   a. Eq a  (a, a)  a  a
swap0 (x,y) z | z == y    = x
              | z == x    = y
              | otherwise = z

swap   f a. (Functor f, Eq a)  (a, a)  f a  f a
swap = fmap . swap0

wk   f a b. (Functor f, a ⊆ b)  f a  f b
wk = fmap injMany

Substitution and monads

instance Monad Tm where
--return ∷ ∀ a. a → Tm a
  return = Var
--(>>=) ∷ ∀ a b. Tm a → (a → Tm b) → Tm b
  Var x   >>= θ = θ x
  Lam s   >>= θ = Lam (s >>>= θ)
  App t u >>= θ = App (t >>= θ) (u >>= θ)
liftSubst   f v a b. (Functor f, Monad f) 
                         v  (a  f b)  (a ▹ v)  f (b ▹ v)
liftSubst _ θ (Old x) = fmap Old (θ x)
liftSubst _ θ (New x) = return (New x)

(>>>=)   f a b. (Functor f, Monad f) 
                    f (Succ a)  (a  f b)  f (Succ b)
s >>>= θ = unpack s $ λ x t 
             pack x (t >>= liftSubst x θ)

substituteOut   f v a. Monad f 
                           v  f a  f (a ▹ v)  f a
substituteOut x t u = u >>= λ y  case y of
     New _  t
     Old x  return x


instance Traversable Tm where
--traverse ∷ ∀ f a b. Applicative f ⇒ (a → f b)
--                                  → Tm a → f (Tm b)
  traverse f (Var x)   = Var <$> f x
  traverse f (App t u) =
    App <$> traverse f t <*> traverse f u
  traverse f (Lam t)   =
    unpack t $ λ x b 
      lamP x <$> traverse (bitraverse f pure) b

bitraverse   f a a' b b'.
              Functor f  (a      f a')
                         (b      f b')
                         (a ▹ b  f (a' ▹ b'))
bitraverse f _ (Old x) = Old <$> f x
bitraverse _ g (New x) = New <$> g x

closed   f a b. Traversable f  f a  Maybe (f b)
closed = traverse (const Nothing)


instance Foldable Tm where
--foldMap ∷ ∀ a m. Monoid m ⇒ (a → m) → Tm a → m
  foldMap = foldMapDefault

--toList ∷ ∀ t a. Foldable t ⇒ t a → [a]
--elem   ∷ ∀ t a. (Foldable t, Eq a) ⇒ a → t a → Bool

freeVars   a t. Foldable t  t a  [a]
freeVars = toList

freshFor   a v t. (Eq a, v ∈ a, Foldable t) 
                    v  t a  Bool
x `freshFor` t = not (inj x `elem` t)

Bigger examples

Continuation Passing Style

data TmC a where
  HaltC  Value a  TmC a
  AppC   Value a  Value a  TmC a
  LetC   Value a  TmC (Succ a)  TmC a

data Value a where
  LamC   TmC (Succ a)  Value a
{- ... -}

cps   a. Tm a  ( v. v  TmC (a ▹ v))  TmC a
cps (Var x)     k = untag <$> k x
cps (App e1 e2) k =
  cps e1 $ λ x1 
  cps (wk e2) $ λ x2 
  varC x1 `AppC` (varC x2 `PairC`
                  lamC (λ x  wk $ k x))
cps (Lam e)    k =
    (lamC $ λp 
       letC (fstC p) $ λ x1 
       letC (sndC p) $ λ x2 
       cps (wk $ e `atVar` x1) $ λr 
       varC x2 `AppC` varC r) k

Closure Conversion

data LC a where
  VarLC    a  LC a
  AppLC    LC a  LC a  LC a
  Closure  ( vx venv. vx  venv 
               LC (Zero ▹ venv ▹ vx)) 
            LC a  LC a
  Tuple    [LC a]  LC a
  Index    LC a  Int  LC a
  LetOpen  LC a  ( vf venv. vf  venv 
                     LC (a ▹ vf ▹ venv))  LC a

{- ... -}

cc   a. Eq a  Tm a  LC a
cc (Var x) = VarLC x
cc t0@(Lam b) =
  let yn = nub $ freeVars t0
  in Closure (λ x env  cc (b `atVar` x) >>=
                   liftSubst x (idxFrom yn env))
             (Tuple $ map VarLC yn)
cc (App e1 e2) =
  LetOpen (cc e1)
          (λ f x  var f $$ wk (cc e2) $$ var x)

Normalization by hereditary substitution

data No a where
  LamNo   v. v  No (a ▹ v)  No a
  Neutr  a  [No a]  No a

instance Monad No where
  return x = Neutr x []

  LamNo x t  >>= θ = LamNo x (t >>= liftSubst x θ)
  Neutr f ts >>= θ = foldl app (θ f) ((>>= θ) <$> ts)

{- ... -}

app   a. No a  No a  No a
app (LamNo x t)  u = substituteOut x u t
app (Neutr f ts) u = Neutr f (ts++[u])

norm   a. Tm a  No a
norm (Var x)   = return x
norm (App t u) = app (norm t) (norm u)
norm (Lam b)   = unpack b $ λ x t  LamNo x (norm t)


Known Extensions

  • Binding many variables at time  ∀ v. (n → v) → tm (a ▹ v)

  • Delayed substitutions (generalized de Bruijn indices)  tm (tm a ▹ v)

  • Using a type class constraint
     ∀ v. v → f (a ▹ v)
     ∀ v. Binder v ⇒ v → f (a ▹ v)
    where Binder () is the only instance.

Future work

  • Integrate as a language extension?
  • Improve performances
  • Provide a bound-extras package extending E. Kmett's bound.