Section 3.1 gives confusing prose on define-metafunction vs define-relation

[csgordon]

trafficstars

I'm following along typing everything, and hit a minor snag.

Section 3.1 gives two alternative definitions of unique and suggests they are equivalent:

(define-metafunction REDEX
      unique : any ... -> boolean
      [(unique any_!_1 ...) #t]
      [(unique _ ...) #f])

There is a kind of short-hand for defining predicates (metafunctions that produce either true or false), called, confusingly enough, define-relation:

(define-relation REDEX
  unique ⊆ any × ...
  [(unique any_!_1 ...)])

The text suggests the two are interchangable, but the define-metafunction form seems to break things. I tried to evaluate the PCF typing judgment using the define-metafunction form of unique, but got the following error:

define-judgment-form: expected judgment form name in: unique

The error goes away if I switch to the define-relation form, and the tutorial code itself uses the relation form in shared.rkt (line 128)

I ran into this on Racket (DrRacket) 6.5, but checked on 6.2.1 as well.

[leafac]

I can confirm the issue. It happened exactly the same to me. I believe a suitable solution is just to remove the part mentioning unique as a meta-function. I don't think it would do any harm, as ext was already introduced as an example of meta-function, so the reader should know define-metafunction by that point.

[frenchy64]

I also ran into this issue.