PLT Redex: mf-apply

:: PLT Redex, package, lang-extension, by Ben Greenman

The mf-apply keyword is for checked metafunction application in PLT Redex. In other words, (mf-apply f x) is just like (f x), but errors if f is not a previously-defined metafunction.

Also, consider applying to attend The Racket School of Semantics and Languages in Salt Lake City this summer:

Metafunctions vs. List Patterns

Have you used PLT Redex? Good! Maybe this has happened to you:

#lang racket
(require redex)

;; -----------------------------------------------------------------------------
;; 1. You define a language
(define-language STLC
  [V ::= integer boolean C]
  [C ::= (closure Λ ρ)]
  [Λ ::= (λ (x : τ) M)]
  [M ::= (M M) V Λ x]
  [τ ::= Int Bool (τ → τ)]
  [ρ ::= ((x V) ...)]
  [Γ ::= ((x τ) ...)]
  [x ::= variable-not-otherwise-mentioned]
  #:binding-forms (λ (x : τ) M #:refers-to x))

;; -----------------------------------------------------------------------------
;; 2. You define a few metafunctions
(define-metafunction STLC
  closure->lam : C -> Λ
  [(closure->lam (closure Λ ρ))

(define-metafunction STLC
  closure->env : C -> ρ
  [(closure->env (closure Λ ρ))

;; -----------------------------------------------------------------------------
;; 3. You try defining a judgment form . . .
(define-judgment-form STLC
  #:mode (free-variables I O)
  #:contract (free-variables M (x ...))
   --- FVS-Var
   (free-variables x (x))]
   (free-variables M_0 (x_0 ...))
   (free-variables M_1 (x_1 ...))
   --- FVS-App
   (free-variables (M_0 M_1) (x_0 ... x_1 ...))]
   (where (λ (x_0 τ) M) Λ)
   (free-variables M (x_1 ...))
   (where (x_2 ...) ,(set-remove (term (x_1 ...)) (term x_0)))
   --- FVS-Λ
   (free-variables Λ (x_2 ...))]
   --- FVS-Integer
   (free-variables integer_0 ())]
   --- FVS-Boolean
   (free-variables boolean_0 ())]
   (where Λ (closure->lam C))
   (free-variables Λ (x_0 ...))
   (where ((x_1 τ_1) ...) (closure-env C))
   (where (x_2 ...) ,(set-subtract (term (x_0 ...)) (term (x_1 ...))))
   --- FVS-Closure
   (free-variables C (x_2 ...))])

;; -----------------------------------------------------------------------------
;; 4. You test the judgment, and it mysteriously fails
  (free-variables (closure (λ (x : Int) x) ())
;; ==> #f


The problem is this line in the FVS-Closure rule:

   (where ((x_1 τ_1) ...) (closure-env C))

which checks that the list (closure-env C) (whose first element is the symbol closure-env and second element is the symbol C) matches the pattern ((x_1 τ_1) ...).


Of course you meant to apply the metafunction closure->env but made a typo. And since the syntax for metafunction application is the same as the syntax for building a list, Redex doesn’t report an error.

We can fix this code with the new mf-apply keyword (available on GitHub or in a snapshot build):

   (where ((x_1 τ_1) ...) (mf-apply closure-env C))

Running raco make now gives a compile-time error.

  term: expected a previously defined metafunction
    at: closure-env
    in: (mf-apply closure-env C)

But I still need to type mf-apply correctly!

Leif Andersen says:

I should point out that this has the issue of you still need to type mf-apply correctly. ;)

That is, if you accidentally write:

   (where ((x_1 τ_1) ...) (mf-applu closure-env C))

Then the code compiles, thinking you intend to match a list of three elements against the pattern.

Never fear, there are at least two solutions.

Solution 1: rename mf-apply

A simple fix is to rename the mf-apply keyword to something shorter (and harder to mis-type):

#lang racket
(require redex
         (rename-in redex
           [mf-apply MF]))

Solution 2: the mf-apply lang extension

A fancier solution is to install the mf-apply meta-language.

  $ raco pkg install mf-apply

This language updates the readtable to interpret S-expressions that begin with #{:

#lang mf-apply racket
(require redex)

(term #{f x ...})

as a metafunction application:

#lang mf-apply racket
(require redex)

(term (mf-apply f x ...))

You the programmer only needs to write the #{....} syntax.

Source code is on GitHub:

(It’s the simplest lang-extension I know of)

What is PLT Redex?

PLT Redex is a library for semantics engineering. One of my favorite Redex features is it implements capture-avoiding substitution and α-equivalence for any language with a #:binding-forms specification (such as STLC, above).

You can read more:

And if you act now, you can become a Redexan between July 10 and July 14 at the summer school in Salt Lake City, Utah: