7.7

5.2 A Syntax Extension

Part 2 of 3 in the Tutorial: From Models to Interpreters.

    5.2.1 The Extended Syntax

      5.2.1.1 Preliminaries

      5.2.1.2 Application & Sequence “Currying”

      5.2.1.3 Multi-clause Abstractions

      5.2.1.4 Local Bindings

      5.2.1.5 The New Parser

      5.2.1.6 The New Printer

      5.2.1.7 Putting It Back Together

    5.2.2 Examples

      5.2.2.1 Numbers

      5.2.2.2 Booleans

      5.2.2.3 Lists

    5.2.3 Closing Remarks

 #lang algebraic/model/ext package: algebraic

In The Core Calculus , we built an s-expression interpreter as a small-step term evaluator based loosely on the λ-calculus. To help encode complex terms as runnable s-expressions, we used a manual term rewriting technique. This time, we’re going to simplify the surface syntax dramatically by building that technique and one more into the parse and print functions.

Syntax

t ⩴ ⋯ | tt | t;⋯;t | φ

p

t

p

t

  | μ

p

t

p

t

p ⩴ ⋯ | pp | p;⋯;p

Evaluation Semantics

t1 t2tn   ↝   t1 (t2tn)

t1;t2;⋯;tn   ↝   t1;(t2;⋯;tn)

p1 p2pn   ↝   p1 (p2pn)

p1;p2;⋯;pn   ↝   p1;(p2;⋯;pn)

n ≥ 2

φ

p1

t1

p2

t2

pn

tn

 

 

φp1.t1

p2

t2

pn

tn

μ

p1

t1

p2

t2

pn

tn

 

 

μp1.t1

p2

t2

pn

tn

φ

p1

t1

 

 

φp1.t1

μ

p1

t1

 

 

μp1.t1

Special Forms

fix = φf.(φx.f φy.(x x) y) (φx.f φy.(x x) y)

let ≈ μ

(p t)

body

p.body) t

(p t;cs)

body

let (p t) let cs body

letrec ≈ μ

(p t)

body

let (p fix φp.body) t

(p t;cs)

body

letrec (p t) letrec cs body

Example Programs

add = φ

a

Zero

a

a

Succ b

Succ add a b

mul = φ

a

Zero

Zero

a

Succ b

add a mul a b

not = φ

False

True

_

False

and = μ(a b).φ

False

False

_

b

 a

or = μ(a b).φ

False

b

x

x

 a

xor = μ(a b).φ

False

b

x

and (not b) x

 a

list = μ

x

Cons(x;Nil)

x

xs

Cons(x;list xs)

reverse = φxs.letrec imagerev φ

Nil

a

a

Cons(y;ys)

a

rev ys Cons(y;a)

image rev xs Nil

5.2.1 The Extended Syntax

The point of this extension is to make The Core Calculus easier to use. With a more forgiving syntax, we can write more substantial programs. To get there, we’ll implement two simple rewriting tricks. First, we’ll eliminate some parentheses by generalizing the abstraction, application, and sequence forms to any number of clauses or sub-terms. Then, we’ll get rid of boilerplate by pre-defining let, letrec, and fix in the parser. Our new parse and print functions will map between the new surface syntax and the existing AST, so we can re-use the core interpret function without modification.

5.2.1.1 Preliminaries

We’ll be re-using a good chunk of the core interpreter, so it makes sense to import those things up front. It’s a lot of stuff to keep track of, so we’ll just import all of algebraic/model/core except the forms that would clobber Racket’s default behavior. We should also exclude the names we’ll be re-defining.

  (require (except-in algebraic/model/core
                      #%app #%datum #%module-begin #%top-interaction
                      parse show algebraic))

5.2.1.2 Application & Sequence “Currying”

t ⩴ ⋯ | tt | t;⋯;t

p ⩴ ⋯ | pp | p;⋯;p

In The Core Calculus, applications and sequences have exactly two sub-terms and all sub-terms must be parenthesized. This design keeps the core language small and easy to implement, but it also makes core programs hard to read and write.

t1 t2tn   ↝   t1 (t2tn)

t1;t2;⋯;tn   ↝   t1;(t2;⋯;tn)

n ≥ 2

p1 p2pn   ↝   p1 (p2pn)

p1;p2;⋯;pn   ↝   p1;(p2;⋯;pn)

An extended application or sequence (term or pattern) with more than two sub-terms (or sub-patterns) becomes an equivalent series of core applications or sequences. If we view these rewrites as premise-less inference rules, or tautologies, they’re easy to transcribe into the clauses of a recursive function.

  (define (parse t)
    (define term
      (function
        ...
        [('$ t1 t2 . ts) (TSeq (term t1) (term `($ ,t2 ,@ts)))]
        [('$ t1) (term t1)]
        [(t1 t2 . ts) (TApp (term t1) (term `(,t2 ,@ts)))]
        [(t1) (term t1)]
        ...))
    (define patt
      (function
        ...
        [('$ p1 p2 . ps) (PSeq (patt p1) (patt `($ ,p2 ,@ps)))]
        [('$ p1) (patt p1)]
        [(p1 p2 . ps) (PApp (patt p1) (patt `(  ,p2 ,@ps)))]
        [(p1) (patt p1)]
        ...))
    (term t))

This formulation has a subtle yet significant quirk. In curried languages, function application is usually left associative. To get an idea why, consider a two-argument λ-abstraction:

λxy.f x y

Currying transforms this two-argument function into an equivalent series of single-argument functions:

λxy.f x y

Now imagine f is bound to a similarly curried two-argument λ-abstraction. When f is applied to x, it produces another λ-abstraction which, when applied to y, completes the series and evaluates the original body of f. Because each application produces the next left-hand side of the series, we have less parentheses with left-associative applications.

In Haskell, the expression f x y parses as if it was written (f x) y but 1::2::[] parses as 1::(2::[]). Haskell makes this distinction because left-associative applications are the backbone of the popular point-free style but list construction is usually right associative.

The curry and compose functions can be helpful, and define has a currying shorthand notation as well, but they are much less satisfying to use than what Haskell offers. The compose-app and fancy-app packages can be helpful in that regard.

In Racket, function application is list construction and therefore also right associative, so the same expression (f x y) parses as if it were written (f . (x . (y . ()))).

When Racket encounters a function application, it evaluates the entire argument list before invoking the function. If we want to resolve the head position of the list with a series of unary functions, we must express that desire in the code or load an extension to do it for us; Racket won’t do it automatically. Since our interpreter is helping us design an extension for Racket and not Haskell, our programs will contain less parentheses if extended applications also associate to the right.

5.2.1.3 Multi-clause Abstractions

t ⩴ ⋯ | φ

p

t

p

t

  | μ

p

t

p

t

Extended abstractions with multiple clauses are more compact and easier to read than their core counterparts. Each row of an extended function or macro corresponds to a core abstraction clause.

A row [p | t] can be read:

If the argument matches p, then evaluate t with the variables of p in context.

If an extended abstraction has more than one clause, the clauses will be tried in order from top to bottom until a match succeeds.

We need to transform an extended abstraction into The Core Calculus constructs that behave the same way: a uniform sequence of core abstraction clauses.

φ

p1

t1

p2

t2

pn

tn

 

 

φp1.t1

p2

t2

pn

tn

n ≥ 2

μ

p1

t1

p2

t2

pn

tn

 

 

μp1.t1

p2

t2

pn

tn

φ

p1

t1

 

 

φp1.t1

μ

p1

t1

 

 

μp1.t1

Once again, we can implement these rewrites as tautologies.

  (define (parse t)
    (define term
      (function
        ...
        [('fun [p . t]) (term `(φ ,p ,@t))]
        [('mac [p . t]) (term `(μ ,p ,@t))]
        [('fun c . cs) (TSeq (term `(fun ,c)) (term `(fun ,@cs)))]
        [('mac c . cs) (TSeq (term `(mac ,c)) (term `(mac ,@cs)))]
        ...))
    (define patt ...)
    (term t))

On the surface, a fun or mac is a non-empty list of pattern-term pairs. A fun with only one clause becomes a function clause, and a fun with more than one clause becomes a sequence of function clauses. If t is a list, its outer parentheses can be dropped.

5.2.1.4 Local Bindings

In The Core Calculus, we developed a technique for encoding example programs in terms our interpreter could evaluate. Starting with an ideal pseudo-syntax that included hypothetical let and letrec forms, we manually rewrote the ideal forms into terms in the surface syntax. We need these forms to define pretty much everything else, so hard wiring them into our parser is an obvious win.

fix is a straight-forward function expression.

fix = φf.(φx.f φy.(x x) y) (φx.f φy.(x x) y)

The remaining transformations for let and letrec cannot be expressed with functions and macros directly, but we can take advantage of the extended syntax to explain what goes wrong and how we’ll handle it.

let ≈ μ

(p t)

body

p.body) t

(p t;cs)

body

let (p t) let cs body

This definition of let behaves like Racket’s let* and not like let, though the latter can also be approximated in the calculus.

A let form behaves like a macro that takes one or more pattern-term clauses and produces a nested series of function applications which evaluates and deconstructs one term at a time.

We can’t just define let with a macro because it would try to use a Term (p) as the Patt of a function abstraction (φp.body). To avoid this wrinkle, our parser will rewrite the surface syntax and then re-apply itself to the result.

letrec ≈ μ

(p t)

body

let (p fix φp.body) t

(p t;cs)

body

letrec (p t) letrec cs body

The letrec form is similar to the let form, except it also fixes the ts for simple recursive definitions.

  (define (parse t)
    (define term
      (function
        ...
        ['fix (term '(φ f (φ x f φ y (x x) y) (φ x f φ y (x x) y)))]
        [('let () . body) (term body)]
        [('let ([p . t] . cs) . body) (term `((φ ,p let ,cs ,@body) ,@t))]
        [('letrec () . body) (term body)]
        [('letrec ([p . t] . cs) . body)
         (term `((φ ,p letrec ,cs ,@body) fix φ ,p ,@t))]
        ...))
    (define patt ...)
    (term t))

This binds the names let, letrec, and fix globally.

5.2.1.5 The New Parser

Together, the new clauses form the basis of our syntax extension. We’ll round out our new parse function by folding in clauses for the remaining core constructs.

  (define (parse t)
    (define term
      (function
        ['fix (term '(φ f (φ x f φ y (x x) y) (φ x f φ y (x x) y)))]
        [('fun [p . t]) (term `(φ ,p ,@t))]
        [('mac [p . t]) (term `(μ ,p ,@t))]
        [('fun c . cs) (TSeq (term `(fun ,c)) (term `(fun ,@cs)))]
        [('mac c . cs) (TSeq (term `(mac ,c)) (term `(mac ,@cs)))]
        [('let () . body) (term body)]
        [('let ([p . t] . cs) . body) (term `((φ ,p let ,cs ,@body) ,@t))]
        [('letrec () . body) (term body)]
        [('letrec ([p . t] . cs) . body)
         (term `((φ ,p letrec ,cs ,@body) fix φ ,p ,@t))]
        [('φ p1 . t2) (values-> TFun (α-rename (patt p1) (term t2)))]
        [('μ p1 . t2) (values-> TMac (α-rename (patt p1) (term t2)))]
        [('$ t1 t2 . ts) (TSeq (term t1) (term `($ ,t2 ,@ts)))]
        [('$ t1) (term t1)]
        [(t1 t2 . ts) (TApp (term t1) (term `(,t2 ,@ts)))]
        [(t1) (term t1)]
        [x #:if (con-name? x) (TCon x)]
        [x #:if (var-name? x) (TVar x)]
        [' TUni]))
    (define patt
      (function
        [('$ p1 p2 . ps) (PSeq (patt p1) (patt `($ ,p2 ,@ps)))]
        [('$ p1) (patt p1)]
        [(p1 p2 . ps) (PApp (patt p1) (patt `(  ,p2 ,@ps)))]
        [(p1) (patt p1)]
        [x #:if (con-name? x) (PCon x)]
        [x #:if (var-name? x) (PVar x)]
        ['_ PWil]
        [' PUni]))
    (term t))

5.2.1.6 The New Printer

The extended printer is a little more interesting than its predecessor. To print extended applications and sequences, we’ll need to transform the abstract syntax back into ordinary lists.

  (define app->list
    (function
      [(TApp t1 t2) (cons (show t1) (app->list t2))]
      [(PApp p1 p2) (cons (show p1) (app->list p2))]
      [a (list (show a))]))
   
  (define seq->list
    (function
      [(TSeq t1 t2) (cons (show t1) (seq->list t2))]
      [(PSeq p1 p2) (cons (show p1) (seq->list p2))]
      [a (list (show a))]))

The app->list function takes a two-argument instance of TApp (or PApp) and conses the left sub-term (or sub-pattern) onto the result of recursively applying itself to the right sub-term (or sub-pattern).

The seq->list function does the same thing for TSeqs and PSeqs.

These two functions are the workhorses of the new printer. For the most part, it has the same structure as the old printer. With two extra clauses for the extended abstractions, it’ll look like this:

  (define (show a)
    (define term
      (function
        [(TSeq (TFun _ _) _) ...]
        [(TSeq (TMac _ _) _) ...]
        [(TSeq _ _) ...]
        [(TApp _ _) ...]
        [(TFun p1 t2) ...]
        [(TMac p1 t2) ...]
        [(TVar x1) (α-restore x1)]
        [(TCon δ1) δ1]
        [TUni ']))
    (define patt
      (function
        [(PSeq _ _) ...]
        [(PApp _ _) ...]
        [(PVar x1) (α-restore x1)]
        [(PCon δ1) δ1]
        [PWil '_]
        [PUni ']))
    (term a))

Applications are the simplest non-trivial case. To show a series of TApps (or PApps), we just need to list out the left-hand sides and that’s exactly what app->list does. Sequences get similar treatment, except we also prepend a $ to the list.

  (define (show a)
    (define term
      (function
        ...
        [(TSeq _ _) #:as t `($ ,@(seq->list t))]
        [(TApp _ _) #:as t (app->list t)]
        ...))
    (define patt
      (function
        ...
        [(PSeq _ _) #:as p `($ ,@(seq->list p))]
        [(PApp _ _) #:as p (app->list p)]
        ...))
    (term a))

Here, we bind the whole term to an alias (#:as t or p) and then pass it to the helper which does most of the work.

The simple abstractions (φ, μ) are slightly more involved. If the body term is an application, we can drop the outer parentheses.

  (define (show a)
    (define term
      (function
        ...
        [(TFun p1 t2) `(φ ,(patt p1) ,@(app->list t2))]
        [(TMac p1 t2) `(μ ,(patt p1) ,@(app->list t2))]
        ...))
    (define patt ...)
    (term a))

And finally, we’ll transform sequences of abstractions into lists of extended abstraction clauses with the symbol fun or mac prepended.

  (define (show a)
    (define term
      (function
        ...
        [(TSeq (TFun _ _) _) #:as t `(fun ,@(fun->list t))]
        [(TSeq (TMac _ _) _) #:as t `(mac ,@(mac->list t))]
        ...))
    (define patt ...)
    (define fun->list
      (function
        [(TFun p1 t2) `([,(patt p1) ,@(app->list t2)])]
        [(TSeq t1 t2) (append (fun->list t1) (fun->list t2))]))
    (define mac->list
      (function
        [(TMac p1 t2) `([,(patt p1) ,@(app->list t2)])]
        [(TSeq t1 t2) (append (mac->list t1) (mac->list t2))]))
    (term a))

The fun->list and mac->list helpers do pretty much the same thing as app->list or seq->list but for sequences of abstraction clauses. They both need the patt combinator, so we’ll just leave them inside the show function.

The full extended parser:

  (define (show a)
    (define term
      (function
        [(TSeq (TFun _ _) _) #:as t `(fun ,@(fun->list t))]
        [(TSeq (TMac _ _) _) #:as t `(mac ,@(mac->list t))]
        [(TSeq _ _) #:as t `($ ,@(seq->list t))]
        [(TApp _ _) #:as t (app->list t)]
        [(TFun p1 t2) `(φ ,(patt p1) ,@(app->list t2))]
        [(TMac p1 t2) `(μ ,(patt p1) ,@(app->list t2))]
        [(TVar x1) (α-restore x1)]
        [(TCon δ1) δ1]
        [TUni ']))
    (define patt
      (function
        [(PSeq _ _) #:as p `($ ,@(seq->list p))]
        [(PApp _ _) #:as p (app->list p)]
        [(PVar x1) (α-restore x1)]
        [(PCon δ1) δ1]
        [PWil '_]
        [PUni ']))
    (define fun->list
      (function
        [(TFun p1 t2) `([,(patt p1) ,@(app->list t2)])]
        [(TSeq t1 t2) (append (fun->list t1) (fun->list t2))]))
    (define mac->list
      (function
        [(TMac p1 t2) `([,(patt p1) ,@(app->list t2)])]
        [(TSeq t1 t2) (append (mac->list t1) (mac->list t2))]))
    (term a))

5.2.1.7 Putting It Back Together

The extended interpreter is nearly finished. Before we can use it, it needs two more things.

First, we need to combine our new parse and show functions with the core interpret function in a new algebraic form.

  (define-syntax algebraic (μ t (show (interpret (parse 't)))))

Second, we need a reader sub-module enabling #lang algebraic/model/ext as a module language with the default s-expression reader.

  (module reader syntax/module-reader
    algebraic/model/ext)

And that completes the extended interpreter. Let’s kick the tires.

5.2.2 Examples

The extended syntax may be more compact and easier to read than the core syntax, but is it any easier to write?

5.2.2.1 Numbers

add = φ

a

Zero

a

a

Succ b

Succ add a b

mul = φ

a

Zero

Zero

a

Succ b

add a mul a b

This may look a little jarring at first. Where did all the inner parentheses go? With right-associative applications, the pattern (a Succ b) is equivalent to (a (Succ b)) and the term (Succ add a b) is equivalent to (Succ (add a b)).

It’s pretty easy to accept that (add a b) is the argument to Succ because there’s only one argument in the argument list. But what about the corresponding term for mul? If applications were left associative, the term (add a mul a b) would have to be re-written as (add a (mul a b)).

Succ took only one argument, but add takes two. The parser knows that the second argument to add is (mul a b) and not mul or (mul a) because the tail of the argument list is the final argument. All arguments with sub-terms except the last must be parenthesized.

Let’s slow down a little and figure out what’s really going on. Say we are evaluating the term:

add Zero mul Zero Zero

Before the “add” function takes control, its argument list (Zero mul Zero Zero) is evaluated in the following manner:

  1. Zero is already a value—a constructor. Evaluation continues down the rest of the argument list:

    (mul Zero Zero)

  2. The name “mul” reduces to an anonymous function. The argument list is now:

    ((φ mul ...) Zero Zero)

  3. The trailing Zeros are already values. Every element of the argument list is now known to be a value. Evaluation continues back up the argument list, which hasn’t changed:

    ((φ mul ...) Zero Zero)

  4. ((φ mul ...) Zero Zero) reduces to Zero. Evaluation continues back up the argument list:

    (Zero Zero)

  5. The argument list (Zero Zero) is now fully evaluated.

This leaves (add Zero Zero) as the next step of the computation.

To state the obvious, the tail of a list is also a list, and a list with a function at its head is a function application. As evaluation focuses down the tail of the argument list, any argument (except the last) that is a function will be applied to the remaining arguments.

Note that extended sequences do not have this property. Every term with sub-terms in a sequence must be parenthesized.

Encoding Peano arithmetic in the extended calculus is as easy as 1 + 2 = 3

> (letrec ([add fun [(a Zero) a] [(a Succ b) Succ add a b]])
    add (Succ Zero) Succ Succ Zero)

'(Succ Succ Succ Zero)

or 2 × 3 = 6.

> (letrec ([add fun [(a Zero)    a] [(a Succ b)  Succ add a b]]
           [mul fun [(a Zero) Zero] [(a Succ b) add a mul a b]])
    mul (Succ Succ Zero) (Succ Succ Succ Zero))

'(Succ Succ Succ Succ Succ Succ Zero)

These definitions are a lot more realistic. They almost look like real algebraic programs.

5.2.2.2 Booleans

not = φ

False

True

_

False

and = μ(a b).φ

False

False

_

b

 a

or = μ(a b).φ

False

b

x

x

 a

xor = μ(a b).φ

False

b

x

and (not b) x

 a

There isn’t much to say about Booleans in the extended model.

> (letrec ([not fun [False True] [_ False]]
           [and μ (a b) (fun [False False] [_ b])             a]
           [or  μ (a b) (fun [False     b] [x x])             a]
           [xor μ (a b) (fun [False     b] [x and (not b) x]) a])
    or (not True) and (xor True True) True)

'False

The extended surface syntax is definitely easier to read, if only because the definitions come first and aren’t nested.

5.2.2.3 Lists

list = μ

x

Cons(x;Nil)

x

xs

Cons(x;list xs)

The extended notation visually folds our “list” function definition on top of itself. When we align patterns and terms vertically like this, the structural similarities and differences across clauses stand out.

> (letrec ([list mac [(x  ) Cons $ x       Nil]
                     [(x xs) Cons $ x (list xs)]])
    list (Succ Zero) (Succ Succ Zero) (Succ Succ Succ Zero) )

'(Cons

  ($

   (Succ Zero)

   (Cons ($ (Succ Succ Zero) (Cons ($ (Succ Succ Succ Zero) Nil))))))

If we recall the original result:

> ((φ fix
       ((φ list
          (list ((Succ Zero)
                 ((Succ (Succ Zero))
                  ((Succ (Succ (Succ Zero)))
                   )))))
        (fix (φ list ($ (μ (x ) (Cons ($ x Nil)))
                        (μ (x xs) (Cons ($ x (list xs)))))))))
     (φ f
       ((φ x (f (φ y ((x x) y))))
        (φ x (f (φ y ((x x) y)))))))

'(Cons

  ($

   (Succ Zero)

   (Cons ($ (Succ (Succ Zero)) (Cons ($ (Succ (Succ (Succ Zero))) Nil))))))

We’re 6 parentheses lighter. That’s not bad, but not quite as dramatic as what we squeezed out of our code. Can we do better with our data, too? The next tutorial, Exposing the Host, will address this question.

reverse = φxs.letrec imagerev φ

Nil

a

a

Cons(y;ys)

a

rev ys Cons(y;a)

image rev xs Nil

> (letrec ([list mac [(x ) Cons $ x Nil] [(x xs) Cons $ x (list xs)]]
           [reverse φ xs
                    letrec ([rev fun
                                 [(Nil a) a]
                                 [((Cons ($ y ys)) a) rev ys Cons $ y a]])
                    rev xs Nil])
    reverse list (Succ Zero) (Succ Succ Zero) (Succ Succ Succ Zero) )

'(Cons

  ($

   (Succ Succ Succ Zero)

   (Cons ($ (Succ Succ Zero) (Cons ($ (Succ Zero) Nil))))))

Our model of the “reverse” function looks nice, but this time even the code is resisting simplification. It should be clear by now that we have more work to do.

5.2.3 Closing Remarks

The nice thing about syntax extensions is they require less work. The extended interpreter is half the size of the core and there’s still plenty of room to explore the minutiae of our design. In the next tutorial, we’ll start borrowing features from the host platform (i.e. Racket) to make the code faster and the data easier to read.