Switching to Typed Racket For the Rest of HtDP

Moving away from HtDP’s commented type declarations, ‘checked-’ functions, and custom predicates to make programs simpler, more reliable, and faster.

Published

Contents

Extending the Teaching Languages

Matthias Felleisen, a co-author of How to Design Programs, hosts On HtDP, a collection of essays and memos on the design rationale for the book. Under Teaching Languages (*SL), Not Racket, he advocates for instructors to extend the teaching languages as they please to ensure relevance to their audience1.

Making my way through HtDP alone, I am both instructor and audience and so am free to make such extensions for myself.

Thus far I’ve not been using the first such teaching language, Beginning Student Language (BSL), and have instead been using Racket, so that I can separate my exercise solutions from their tests, with the tests then importing the relevant functions. I just prefer this structure, figuring that once the tests pass and the function is deemed to be properly working, I would rather the program itself not be cluttered by these tests. I haven’t gone to the effort of creating my own extended teaching language with this additional feature, but aside from this I have only used features from BSL, so it’s effectively the same as having done so.

Consequently, I’ve had to create for myself a couple of functions already included in BSL, such as member? and the posn structure, and to run tests I’ve had to require the test-engine/racket-tests module and call (test), but that’s been about it, so there’s been very little trouble caused from having done this.

One additional change I am now exploring, from Chapter 10 onwards, is the use of Typed Racket over Racket, a gradually-typed sister language to the dynamically-typed base language, so that I can include static types.

Type-Checking in HtDP

In the second step of HtDP’s six-step function design recipe, Signature, Purpose Statement, Header, the programmer is to, among other things, comment a type declaration for the data that a function is to consume and produce:

#lang racket

(require test-engine/racket-tests)

; Number -> Number
; adds 1 to x
(define (f x)
  (add1 x))

(check-expect (f 0) 1)
(check-expect (f 1) 2)

(test)

HtDP then goes a step further with the creation of checked- functions, a function’s counterpart whose sole purpose is input validation through type-checking:

#lang racket

(require test-engine/racket-tests)

; Number -> Number
; adds 1 to x
(define (f x)
  (add1 x))

(check-expect (f 0) 1)
(check-expect (f 1) 2)

; Number -> Number
; adds 1 to x
(define (checked-f x)
  (cond
    [(number? x) (f x)]
    [else
      (error 'checked-f
             "expected Number")]))
 
(check-error
  (checked-f "a")
  "checked-f: expected Number")
(check-error
  (checked-f #t)
  "checked-f: expected Number")
(check-expect (checked-f 0) (f 0))
(check-expect (checked-f 1) (f 1))

(test)

But I don’t like having two functions to this end. I find it all too easy to use f instead of checked-f, which introduces the potential for errors. And so, I began to include the input validation within f:

#lang racket

(require test-engine/racket-tests)

; Number -> Number
; adds 1 to x
(define (f x)
  (cond
    [(number? x)
     (add1 x)]
    [else
      (error 'f
             "expected Number")]))

(check-error
  (f "a")
  "f: expected Number")
(check-error
  (f #t)
  "f: expected Number")
(check-expect (f 0) 1)
(check-expect (f 1) 2)

(test)

This way, with a single function, there isn’t such confusion while retaining the added benefit of input validation. However, if the function’s body contains a natural recursion, the input is again validated on every recursive call—unnecessarily so as it has already been validated. With HtDP’s heavy use of recursion, this can greatly increase the number of run-time evaluation steps.

Finally, I combined the two approaches: only performing input validation once, as in the original ‘checked-’ function, but as a single function, as in the above revision. An inner function gets called upon successful evaluation of the predicate, here number?: 

#lang racket

(require test-engine/racket-tests)

; Number -> Number
; adds 1 to x
(define (f x)
  (define (f-inner x)
    (add1 x))

  (cond
    [(number? x)
     (f-inner x)]
    [else
      (error 'f
             "expected Number")]))

(check-error
  (f "a")
  "f: expected Number")
(check-error
  (f #t)
  "f: expected Number")
(check-expect (f 0) 1)
(check-expect (f 1) 2)

(test)

I find this to be a satisfying solution to this problem, though a separate problem remains: having type declarations as comments—they are not there enforced and so can be misaligned with the actual implementation. For this I have no solution using the Racket base language, and so have opted instead for Typed Racket.

Type-Checking in Typed Racket

With Typed Racket the type declaration is now part of the code, solving this outstanding issue of potentially misaligned type declarations while also rendering the initial problems—that of having two functions serving the same purpose and then of recursively validating the function’s input—of no concern:

#lang typed/racket

(require typed/rackunit)

(: f (-> Number Number))
; adds 1 to x
(define (f x)
  (add1 x))

(check-equal? (f 0) 1)
(check-equal? (f 1) 2)

The programmer no longer needs to perform input validation in the function’s body or in its tests because it’s simply not allowed. The resulting code is simpler and more assuredly correct. Additionally, with type-checking done at compile-time instead of run-time, there are fewer run-time evaluation steps and so the code would also be faster.

To elucidate the improved simplicity of using Typed Racket, below I compare my solutions to HtDP’s Exercise 160 in both Racket (with the checked-f and f-inner approaches) and Typed Racket:

Version Functions Tests Lines (Code)
Racket: checked-f 7 28 142 (92)
Racket: f-inner 5 26 128 (86)
Typed Racket 3 9   45 (29)

There isn’t much change between the two Racket approaches, and there isn’t meant to be—the intent is more to simplify the interface. There is, however, a drastic change between the two Racket approaches and the Typed Racket approach. The primary savings here are from the deletion of ‘checked-’ functions, custom predicates, and their associated tests.

Exercise 160 (Racket: checked-f) 
#lang racket

(require test-engine/racket-tests)

; Any List -> Boolean
; determines if x is a member of l
(define (member? x l)
  (cond
    [(empty? l) #f]
    [(list? l)
     (or (equal? x (first l))
         (member? x (rest l)))]
    [else
      (error 'member?
             "expected Any List")]))

(check-error
  (member? 0 0)
  "member?: expected Any List")
(check-expect (member? 0 '()) #f)
(check-expect (member? 0 (cons "a" '())) #f)
(check-expect (member? 0 (cons "a" (cons 0 '()))) #t)

; A Son.L is one of: 
; -- empty
; -- (cons Number Son.L)
;
; Son is used when it
; applies to Son.L and Son.R

; Any -> Boolean
; determines if x is an element
; of Son.L
(define (Son.L? x)
  (cond
    [(empty? x) #t]
    [(list? x)
     (and (number? (first x))
          (Son.L? (rest x)))]
    [else #f]))

(check-expect (Son.L? 0) #f)
(check-expect (Son.L? '()) #t)
(check-expect (Son.L? (cons 0 '())) #t)
(check-expect (Son.L? (cons 0 0)) #f)
(check-expect (Son.L? (cons 0 (cons 0 '()))) #t)
(check-expect (Son.L? (cons 0 (cons 1 '()))) #t)

; Son.L Number -> Son.L
; create a set by adding number x
; to some given set s
(define (set+.L s x)
  (cons x s))

(check-expect (set+.L '() 0) (cons 0 '()))
(check-expect (set+.L (cons 0 '()) 0) (cons 0 (cons 0 '())))
(check-expect (set+.L (cons 0 '()) 1) (cons 1 (cons 0 '())))

; Son.L Number -> Son.L
; create a set by adding number x
; to some given set s
(define (checked-set+.L s x)
  (cond
    [(and (Son.L? s)
          (number? x))
     (set+.L s x)]
    [else
      (error 'checked-set+.L
             "expected Son.L Number")]))

(check-error
  (checked-set+.L 0 0)
  "checked-set+.L: expected Son.L Number")
(check-error
  (checked-set+.L '() "a")
  "checked-set+.L: expected Son.L Number")
(check-expect
  (checked-set+.L '() 0)
  (set+.L '() 0))

; A Son.R is one of: 
; -- empty
; -- (cons Number Son.R)
;
; Constraint: If s is a Son.R,
; no number occurs twice in s

; Any -> Boolean
; determines if x is an element
; of Son.R
(define (Son.R? x)
  (cond
    [(empty? x) #t]
    [(list? x)
     (and (number? (first x))
          (not (member? (first x) (rest x)))
          (Son.R? (rest x)))]
    [else #f]))

(check-expect (Son.R? 0) #f)
(check-expect (Son.R? '()) #t)
(check-expect (Son.R? (cons 0 '())) #t)
(check-expect (Son.R? (cons 0 0)) #f)
(check-expect (Son.R? (cons 0 (cons 0 '()))) #f)
(check-expect (Son.R? (cons 0 (cons 1 '()))) #t)

; Son.R Number -> Son.R
; create a set by adding number x
; to some given set s
(define (set+.R s x)
  (cond
    [(member? x s) s]
    [else
      (cons x s)]))

(check-expect (set+.R '() 0) (cons 0 '()))
(check-expect (set+.R (cons 0 '()) 0) (cons 0 '()))
(check-expect (set+.R (cons 0 '()) 1) (cons 1 (cons 0 '())))

; Son.R Number -> Son.R
; create a set by adding number x
; to some given set s
(define (checked-set+.R s x)
  (cond
    [(and (Son.R? s)
          (number? x))
     (set+.R s x)]
    [else
      (error 'checked-set+.R
             "expected Son.R Number")]))

(check-error
  (checked-set+.R 0 0)
  "checked-set+.R: expected Son.R Number")
(check-error
  (checked-set+.R '() "a")
  "checked-set+.R: expected Son.R Number")
(check-expect
  (checked-set+.R '() 0)
  (set+.R '() 0))

(test)
Exercise 160 (Racket: f-inner) 
#lang racket

(require test-engine/racket-tests)

; Any List -> Boolean
; determines if x is a member of l
(define (member? x l)
  (cond
    [(empty? l) #f]
    [(list? l)
     (or (equal? x (first l))
         (member? x (rest l)))]
    [else
      (error 'member?
             "expected Any List")]))

(check-error
  (member? 0 0)
  "member?: expected Any List")
(check-expect (member? 0 '()) #f)
(check-expect (member? 0 (cons "a" '())) #f)
(check-expect (member? 0 (cons "a" (cons 0 '()))) #t)

; A Son.L is one of: 
; -- empty
; -- (cons Number Son.L)
;
; Son is used when it
; applies to Son.L and Son.R

; Any -> Boolean
; determines if x is an element
; of Son.L
(define (Son.L? x)
  (cond
    [(empty? x) #t]
    [(list? x)
     (and (number? (first x))
          (Son.L? (rest x)))]
    [else #f]))

(check-expect (Son.L? 0) #f)
(check-expect (Son.L? '()) #t)
(check-expect (Son.L? (cons 0 '())) #t)
(check-expect (Son.L? (cons 0 0)) #f)
(check-expect (Son.L? (cons 0 (cons 0 '()))) #t)
(check-expect (Son.L? (cons 0 (cons 1 '()))) #t)

; Son.L Number -> Son.L
; create a set by adding number x
; to some given set s
(define (set+.L s x)
  (define (set+.L-inner s x)
    (cons x s))

  (cond
    [(and (Son.L? s)
          (number? x))
     (set+.L-inner s x)]
    [else
      (error 'set+.L
             "expected Son.L Number")]))

(check-error
  (set+.L 0 0)
  "set+.L: expected Son.L Number")
(check-error
  (set+.L '() "a")
  "set+.L: expected Son.L Number")
(check-expect (set+.L '() 0) (cons 0 '()))
(check-expect (set+.L (cons 0 '()) 0) (cons 0 (cons 0 '())))
(check-expect (set+.L (cons 0 '()) 1) (cons 1 (cons 0 '())))

; A Son.R is one of: 
; -- empty
; -- (cons Number Son.R)
;
; Constraint: If s is a Son.R,
; no number occurs twice in s

; Any -> Boolean
; determines if x is an element
; of Son.R
(define (Son.R? x)
  (cond
    [(empty? x) #t]
    [(list? x)
     (and (number? (first x))
          (not (member? (first x) (rest x)))
          (Son.R? (rest x)))]
    [else #f]))

(check-expect (Son.R? 0) #f)
(check-expect (Son.R? '()) #t)
(check-expect (Son.R? (cons 0 '())) #t)
(check-expect (Son.R? (cons 0 0)) #f)
(check-expect (Son.R? (cons 0 (cons 0 '()))) #f)
(check-expect (Son.R? (cons 0 (cons 1 '()))) #t)

; Son.R Number -> Son.R
; create a set by adding number x
; to some given set s
(define (set+.R s x)
  (define (set+.R-inner s x)
    (cond
      [(member? x s) s]
      [else
        (cons x s)]))

  (cond
    [(and (Son.R? s)
          (number? x))
     (set+.R-inner s x)]
    [else
      (error 'set+.R
             "expected Son.R Number")]))

(check-error
  (set+.R 0 0)
  "set+.R: expected Son.R Number")
(check-error
  (set+.R '() "a")
  "set+.R: expected Son.R Number")
(check-expect (set+.R '() 0) (cons 0 '()))
(check-expect (set+.R (cons 0 '()) 0) (cons 0 '()))
(check-expect (set+.R (cons 0 '()) 1) (cons 1 (cons 0 '())))

(test)
Exercise 160 (Typed Racket) 
#lang typed/racket

(require typed/rackunit)

(: member? (-> Any (Listof Any) Boolean))
; determines if x is a member of l
(define (member? x l)
  (cond
    [(empty? l) #f]
    [else
      (or (equal? x (first l))
          (member? x (rest l)))]))

(check-equal? (member? 0 '()) #f)
(check-equal? (member? 0 (cons "a" '())) #f)
(check-equal? (member? 0 (cons "a" (cons 0 '()))) #t)

(define-type Son.L (Listof Number))

(: set+.L (-> Son.L Number Son.L))
; create a set by adding number x
; to some given set s
(define (set+.L s x)
  (cons x s))

(check-equal? (set+.L '() 0) (cons 0 '()))
(check-equal? (set+.L (cons 0 '()) 0) (cons 0 (cons 0 '())))
(check-equal? (set+.L (cons 0 '()) 1) (cons 1 (cons 0 '())))

(define-type Son.R (Listof Number))

(: set+.R (-> Son.R Number Son.R))
; create a set by adding number x
; to some given set s
(define (set+.R s x)
  (cond
    [(member? x s) s]
    [else
      (cons x s)]))

(check-equal? (set+.R '() 0) (cons 0 '()))
(check-equal? (set+.R (cons 0 '()) 0) (cons 0 '()))
(check-equal? (set+.R (cons 0 '()) 1) (cons 1 (cons 0 '())))

A minor gripe is that it’s obvious enough that the last argument to -> in the type declaration is the return type, but I still find myself wanting it to be more obvious, perhaps through some kind of separation. Though I suppose that’s not how Racket works—functions use prefix notation, not infix notation, and -> is a type constructor with the types being its arguments.

One might argue that continuing to write such ‘checked-’ functions and custom predicates is valuable practice, but I’m now quite comfortable doing so and don’t believe I need any further development in this regard. My use of Typed Racket will undoubtedly make the learning curve steeper, but I believe it will prove beneficial in the long run as I use it to create better programs. Thanks to Typed Racket being gradually-typed, I still plan to use Racket’s dynamic typing for quick Read-Eval-Print Loop (REPL) evaluations, but for my programs I would prefer static typing.