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

Q&A

Functional programming?

Awesome!
Easy equational reasoning!

Dysfunctional programming?

Not awesome...

Programming with names and binders?

It's hard...

Nested data types?

Awesome!
Containers for free-variables!

Arithmetic with
de Bruijn indices

Not awesome...
(error prone)

Functors & Monads?

Awesome!
Safe and easy to rename and substitute!

Polymorphism?

Awesome!
Theorems for free!

Incoherent Type Class Instances?

Almost awesome!
(when it works)

Nested Abstract Syntax

Example

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
 

Customize


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

Traversable

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)

Foldable

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 =
  letC
    (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)

Discussion

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.

Thanks!