# PLT Redex: mf-apply

::

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: http://summer-school.racket-lang.org/2017/

## Metafunctions vs. List Patterns

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

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 #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 (judgment-holds (free-variables (closure (λ (x : Int) x) ()) ())) ;; ==> #f 

WHAT HAPPENED??!

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

 1 2 3  .... (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) ...).

Right.

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):

 1 2 3  .... (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:

 1 2 3  .... (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):

 1 2 3 4 #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 #{:

 1 2 3 4 #lang mf-apply racket (require redex) (term #{f x ...}) 

as a metafunction application:

 1 2 3 4 #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).