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

#### 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 `#{`

:

as a metafunction application:

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:

- in the “Amb” tutorial: http://docs.racket-lang.org/redex/tutorial.html
- in the “Long Tutorial”: http://docs.racket-lang.org/redex/redex2015.html
- in the Redex reference manual: http://docs.racket-lang.org/redex/The_Redex_Reference.html
- on the PLT Redex website: https://redex.racket-lang.org/
- on GitHub: https://github.com/racket/redex

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:

(Show comments / Powered by Disqus)