When to use `form:` in Typed Racket?

Question

ts-guide said:

In addition to the : form, almost all binding forms from racket have counterparts which allow the specification of types.

But it does not say when to use which one.

And ts-reference said form: is legacy, for backwards compatibility.

But in ts-guide, form: are used in a lot of places.

So is : v t preferred than form:? And what about form?

For example:

; form:
(define: (id [z : Number]) : Number z)

; : v t + form
(: id (-> Number Number))
(define (id z) z)

; form (it seems recent versions of Racket add this?)
(define (id [z : Number]) : Number z)

Answer 1

First Form

The first form uses the special form define:. It and other forms ending with : are legacy forms in the current version of Racket (v 6.1.1 at the time of this answer). It is equivalent to typed/racket's define but does not accept the second form. It is available for backward compatibility.

Second Form

The second form more closely reflects the idea of a function signature as described in the process for designing functions in the book How to Design Programs*. Even better, because typed/racket allows writing

(: id (Number . -> . Number) 

using the reader's infix macro we can get a much closer correspondence to How to Design Programs at the price of a few extra characters.

Third Form

The third form is more traditional in terms of statically typed languages...by which I mean it maps more closely to the C language, Java, ML, etc. It is also more general because it can be used in anonymous functions:

> ((lambda ((x : Number)) : Number (+ x 10)) 4)
- : Number
14 

Remarks on Type Inference

Note that typed/racket has type inference and it was not necessary to specify the return type as in:

> ((lambda ((x : Number))(+ x 10)) 4)
- : Number
14

Indeed typed/racket will always do it's best to infer types if none are specified:

> ((lambda (x)(+ x 10)) 4)
- : Integer [more precisely: Positive-Index]
14
> ((lambda (x)(+ x 10)) 4.0)
- : Flonum [more precisely: Positive-Flonum]
14.0
> ((lambda (x)(+ x 10)) 4/1)
- : Integer [more precisely: Positive-Index]
14

Conclusion

Of course, what typed/racket infers may not be what the programmer expects. Using the second form has the advantage of making the programmer's intent explicit and making the programmer's intent explicit is a core principle of How to Design Programs and at the heart of the motivations for developing typed/racket in the first place.

Answer 2

But it does not say when to use which one.

In most cases they are equivalent.

I like the second form - it makes it easy to remove the TR annotations again.