On this page:
3.1 Expression Test Forms
3.2 Top-Level Test Forms
typecheck-fail/  toplvl
typecheck-fail/  definitions
3.3 Other Debugging Forms

3 Rackunit-Style Test Forms for Turnstile

 (require rackunit/turnstile)
  package: rackunit-macrotypes-lib

This section describes rackunit-style test forms that are used primarily for testing the type checking of Turnstile-created languages.

This section will use the following Turnstile-defined, simply typed language to demonstrate the testing forms:

; types
(define-base-types Int Bool)
(define-type-constructor  #:arity = 2)
; rule for Int and Bool literals
(define-typed-syntax #%datum
  [(_ . n:integer) 
   [ 'n   Int]]
  [(_ . b:boolean) 
   [ 'b   Bool]]
  [(_ . x) 
   [#:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]])
; single-arity λ
(define-typed-syntax λ
  [(_ [x:id (~datum :) τ_in:type] e) 
   [[x  x- : τ_in.norm]  e  e-  τ_out]
   [ (#%plain-lambda (x-) e-)  ( τ_in.norm τ_out)]]
  [(_ x:id e)  (~→ τ_in τ_out) 
   [[x  x- : τ_in]  e  e-  τ_out]
   [ (#%plain-lambda (x-) e-)]])
; single-arity function application
(define-typed-syntax (#%app e_fn e_arg) 
  [ e_fn  e_fn-  (~→ τ_in τ_out)]
  [ e_arg  e_arg-  τ_in]
  [ (#%plain-app e_fn- e_arg-)  τ_out])
; add1 primop
(define-primop add1 : ( Int Int))
; top-level define
(define-syntax define
    [(_ f [x:id (~datum :) τ_in] : τ_out e)
     #'(define-typed-variable f (λ x e)  ( τ_in τ_out))]))

3.1 Expression Test Forms


(check-type e tag τ)

(check-type e tag τ -> val)
(check-type e tag τ  val)
The test succeeds if expression e’s "type" and τ are equal according to typecheck?.

The expression e’s "type" is determined by tag, which must be an identifier and is used as a symbol key for a syntax property lookup on e’s expanded form. The supplied tag will be most commonly be :.

During type checking, τ is set as e’s "expected type". Thus, a rule’s "check" (⇐) variant, if defined, will be invoked to type check e.

If an optional val argument is specified, the test additionally evaluates e at run time and checks that the result is equal to val according to check-equal? (from rackunit).

> (check-type Int :: #%type)
> (check-type add1 : ( Int Int))
; pass
> (check-type (add1 2) : Int)
; type check fail
> (check-type (add1 2) : Bool)

eval:11.0: check-type: Expression (add1 2) [loc 11:0] has

type Int, expected Bool

  at: (check-type (add1 2) : Bool)

  in: (check-type (add1 2) : Bool)

; pass
> (check-type (add1 2) : Int -> 3)
; run time fail
> (check-type (add1 2) : Int -> 4)



name:       check-equal?

location:   eval:13:0

actual:     3

expected:   4



(check-not-type e : τ)

The test succeeds if expression e’s type is not equal to τ according to typecheck?.

This test form is particularly useful for languages with subtyping.

; pass
> (check-not-type add1 : Int)
; fail
> (check-not-type add1 : ( Int Int))

eval:15.0: check-not-type: (15:0) Expression add1 has type

(→ Int Int); should not typecheck with (→ Int Int)

  at: (check-not-type add1 : (→ Int Int))

  in: (check-not-type add1 : (→ Int Int))


(typecheck-fail e)

(typecheck-fail e #:with-msg msg-pat)
(typecheck-fail e #:verb-msg msg-str)
The test succeeds if expression e raises an exception during type checking.

Supplying an optional msg-pat argument requires the error message to match the given pattern according to regexp-match?.

Supplying an optional msg-str argument requires the error message to include the given string verbatim.

; pass: because type checking fails
> (typecheck-fail (add1 #f))
; fail: because type checking succeeds
> (typecheck-fail (add1 1))



expected:   ""

location:   eval:17:0

name:       typecheck-fail

params:     '((add1 1) "")

message:    "No exception raised"


; pass
> (typecheck-fail (add1 add1) #:with-msg "expected Int, given \\(→ Int Int\\)")
; fail: msg does not match because some chars must be escaped
> (typecheck-fail (add1 add1) #:with-msg "expected Int, given (→ Int Int)")



expected:     "expected Int, given (→ Int Int)"

location:     eval:19:0

name:         typecheck-fail

params:       '((add1 add1) "expected Int, given (→ Int Int)")

message:      "Wrong exception raised"


  "eval:19.0: #%app: type mismatch: expected Int, given (→ Int Int)\n  expression: add1\n  at: add1\n  in: (#%app add1 add1)"


  #(struct:exn:fail:syntax "eval:19.0: #%app: type mismatch: expected Int, given (→ Int Int)\n  expression: add1\n  at: add1\n  in: (#%app add1 add1)" #<continuation-mark-set> (#<syntax:eval:19:0 add1>))


; pass, with unescaped msg using #:verb-msg
> (typecheck-fail (add1 add1) #:verb-msg "expected Int, given (→ Int Int)")

The test succeeds if e type checks but raises an exception when evaluated at run time.

3.2 Top-Level Test Forms


(typecheck-fail/toplvl def)

(typecheck-fail/toplvl def #:with-msg msg-pat)
(typecheck-fail/toplvl def #:verb-msg msg-str)
Same as typecheck-fail, but for top-level definitions.

> (typecheck-fail/toplvl (define f [x : Int] : Bool (add1 x)))
> (typecheck-fail/toplvl (define f [x : Int] : Bool (add1 x))
   #:with-msg "expected Bool, given Int.* expression: \\(add1 x\\)")


(typecheck-fail/definitions [def ...])

(typecheck-fail/definitions [def ...] #:with-msg msg-pat)
(typecheck-fail/definitions [def ...] #:verb-msg msg-str)
Like typecheck-fail/toplvl, but allows multiple top-level definitions to be included in the test.

3.3 Other Debugging Forms


(print-type e)

(print-type e #:tag tag)
(print-type e #:raw)
Prints the type of expression e.

Unless explicitly given a tag argument, the returned type is the syntax property at tag ':.

If written with the #:raw declaration, returns the internal representation of the type. Otherwise, the type is first resugared according to type->str.