3 Formal Functions

3.1 Motivation

Pattern matching usually goes together with algebraic types. Racket’s structures and lists could be used as constructors for algebraic data types, but they use have some drawbacks.

Suppose we wish to define a rewriting system for Peano axioms. We start with definition of types for numerals, successor, sum and product:

(struct N (x) #:transparent)
(struct 1+ (x) #:transparent)
(struct Sum (x y) #:transparent)
(struct Prod (x y) #:transparent)

Next we define rewriting rules:

(define calculate
  (replace-all-repeated
   (N 0) --> 0
   (N n) --> (1+ (N (- n 1)))

   (Sum x 0) --> x
   (Sum x (1+ y)) --> (1+ (Sum x y))

   (Prod _ 0) --> 0
   (Prod x (1+ y)) --> (Sum x (Prod x y))))

> (calculate (Sum (N 2) (N 3)))
(Sum (N 2) (N 3))

However, this clear definition doesn’t work, because the rewriting process can’t get into the structures and change their parts. One solution is to add rules for penetrating into the structures:

(define calculate2
  (replace-repeated
   (N 0) --> 0
   (N n) --> (1+ (N (- n 1)))

   (Sum x 0) --> x
   (Sum x (1+ y)) --> (1+ (Sum x y))

   (Prod _ 0) --> 0
   (Prod x (1+ y)) --> (Sum x (Prod x y))

   (1+ x) --> (1+ (calculate2 x))
   (Sum x y) --> (Sum (calculate2 x) (calculate2 y))
   (Prod x y) --> (Prod (calculate2 x) (calculate2 y))))

> (calculate2 (Sum (N 2) (N 3)))
(1+ (1+ (1+ (1+ (1+ 0)))))
> (calculate2 (Prod (N 2) (N 3)))
(1+ (1+ (1+ (1+ (1+ (1+ 0))))))

Now it works! But heavy and tautological lines which end up the rewriting system look cumbersome. They describe programming, not Peano axioms.

Moreover, we need explicit recursion, therefore we have lost the ability to make anonymous rewriting system. Finally, use of structures fixes the number of their fields, so it is impossible to write a pattern like (Sum x __) and to have any number of arguments, which is reasonable when dealing with sums.

Another approach is to use lists and interpret their car-s as tags.

(define calculate3
  (replace-all-repeated
   `(N 0) --> 0
   `(N ,n) --> `(1+ (N ,(- n 1)))

   `(Sum ,x 0) --> x
   `(Sum ,x (1+ ,y)) --> `(1+ (Sum ,x ,y))

   `(Prod ,_ 0) --> 0
   `(Prod ,x (1+ ,y)) --> `(Sum ,x (Prod ,x ,y))))

> (calculate3 '(Sum (N 2) (N 3)))
'(1+ (1+ (1+ (1+ (1+ 0)))))
> (calculate3 '(Prod (N 2) (N 3)))
'(1+ (1+ (1+ (1+ (1+ (1+ 0))))))

Looks much better, but a bit prickly because of quotes and commas. It may become even worse-looking if we use blanks _ and ___ a lot. Using explicit list constructor does not help either, it makes patterns more difficult to read and write: (list 'Sum x (list '1+ y)).

The package provides an abstraction named formal function which work as a taged list constructor in expression position and as a structure constructor in patterns. With use of formal functions we may write clear definition of rewriting system for Peano’s numerals without a single redundant word or symbol:

(define-formal N 1+ Sum Prod)
(define calculate4
  (replace-all-repeated
   (N 0) --> 0
   (N n) --> (1+ (N (- n 1)))

   (Sum x 0) --> x
   (Sum x (1+ y)) --> (1+ (Sum x y))

   (Prod _ 0) --> 0
   (Prod x (1+ y)) --> (Sum x (Prod x y))))

> (calculate4 (Sum (N 2) (N 3)))
'(1+ (1+ (1+ (1+ (1+ 0)))))
> (calculate4 (Prod (N 2) (N 3)))
'(1+ (1+ (1+ (1+ (1+ (1+ 0))))))

Besides, formal functions could be usefull in general. For example in exploring functional programming:

> (define-formal f g h)
> (map f '(a b c))
'((f a) (f b) (f c))
> (foldl g 'x0 '(a b c))
'(g c (g b (g a x0)))
> (foldr g 'x0 '(a b c))
'(g a (g b (g c x0)))
> ((compose f g h) 'x 'y)
'(f (g (h x y)))

Examples "peano.rkt" and "logics.rkt" demonstrate the use of formal functions. Rules using structures are shown in "turing.rkt".

3.2 Declaring Formal Functions

(define-formal id ...)

Declares identifiers id ... to represent formal functions. Produces bindings for id? symbols, which work as type predicates.

Examples:
> (define-formal f)
> (f 1)
'(f 1)
> (f 'a 'b)
'(f a b)
> (f? (f 2 3))
#t
> (f? '(f 2 3))
#t

(formal? v) → boolean?
v : any/c

Returns #t if v is a formal function, #f otherwise.

(n/f-list? v) → boolean?
v : any/c
(n/f-pair? v) → boolean?
v : any/c

Return #t if v is a list (pair), but not a formal function.

Examples:

> (define-formal f)
> (formal? f)
#f
> (list? (f 2 3))
#t
> (n/f-list? (f 2 3))
#f
> (n/f-list? '(x 2 3))
#t

In the last case x was not declared as a formal function, so it is treated as a regular list.

← prev up next →

1	Motivation
2	Replacement Forms
3	Formal Functions
4	Utilities
	Bibliography