Typed Racket guidelines

Questions & Answers
1

Hi,

Frankly, the question should be "Typed Racket: is it safe to use?". I sensibly asked the similar question about the Lazy Racket, and the unanimous answer was "forget it". Well, not exactly, but unless the general laziness is more than a means to an end for you, better stay away from it.

If I start my project with #lang typed/racket at the head of each file, am I going to feel just as happy and optional as with Python type annotations, or there's a price to pay?

2

First restriction: type annotations are mandatory. Fortunately, on a per-file basis.

3

[[ You overinterpret the answer concerning #lang lazy a bit. You can write cool generally lazy programs in it, if that’s your thing. The interop with strict Racket is the problem, and that’s what you seem to want. ]]

Typed Racket is real and usable for any kind of project. It’s type system is sound (modulo bugs). It’’s types are checked at the boundary to untyped modules. Higher-order values are tracked to ensure that they obey the types across boundaries.

What’s the catch? On occasion you may encounter a performance problem if your program’s execution involves a high densitive of mutually recursive typed-untyped calls. Most other performance costs due to checks are tolerable. If you do run intol such performance problems, complain here.

1 Like
4

I suppose the catch you mentioned isn't relevant in case of compiled binaries. Is it really so?

5

Racket is complied so I am not sure what you mean. I think the answer is ‘no’.

6

I mean two different cases:

  1. You can start a script with a hashbang: #!/usr/bin/env racket. This means compile time plus run time.

  2. You can make a binary first: raco exe ... , run time only.

With typed languages type checking adds to compile time only. Do you mean that with Typed Racket type checking adds to run time in both cases?

7

Hi @Tyrn,

Just to complement @EmEf's answer: Typed Racket is great and covers a lot of Racket, but not all of the libraries have types, and converting untyped code to typed code is not automatic. You can import untyped code into typed code by explicitly giving types to the identifiers you import, but you have to write out those types on your own as well.

Personally, I find this a great occasion to contribute to Racket ecosystem and totally worth the additional effort, but this is something you have to factor in your development time.

8

Racket compiles code in both cases. Compiling includes type checking.

Run-time checks come in when you link typed and untyped Racket into a single program:.

Say module A is this untyped code:

#lang racket 

(provide f)

(define (f x) 
   (+ x 1))

and modyle B is typed:

#lang typed/racket 

(provide main) 

(require/typed A ;; adjust for concrete file/collects
  [f (-> Integer String)])

(define (main x) 
  (string-append “hello “ (f (* 2 (string->number x)))))

The creator of B mistakenly assumes that f returns a String. Now run B as a script like this

$ ,/B 10

Facts:

— Both get compiled.
— A type checks.
— The call from B to A is fine, because it type checked.
— The return from A to B sends over 21.

Question: What would you like to happen as someone who equipped B with types?

— Typed Racket inserts a run-time check to make sure that types don’t get usurped.
— TypeScript does nothing. It happily returns some string from main.
— Python’s types aren’t worth mentioning.

Indeed, TR is the most advanced type system in the world that comes with such checks.

Question: are such checks useful?

Based on some recent research, the answer has to be nuanced:

— for someone who makes a mistake in formulating types for untyped code (like above),
the information from run-time checks helps.

— for someone who makes a mistake in code (untyped imports typed, calls it with bad arguments),
the information from run-time checks is still useful but less so.

2 Likes
9

you have to write out those types on your bbbown as well.

This can be difficult if the untyped part does not document its data structures.

-- hendrik

10

I'm not sure that anyone here has said this: I believe that Typed Racket is extremely dependable and very widely used, much more so than lazy racket. If you were to make a "Ring 0" / "Ring 1" distinction, I would say that Typed Racket is in ring 0, and lazy racket is in ring 1.

I use Typed Racket constantly. A common use case for me is that I write code hastily in Racket, then come back a year later and can't easily understand what it means and refactor it to be in Typed Racket.

I would say that Typed Racket can impose some irritating code-writing-time overhead in the case of certain racket idioms (uses of higher-order functions like sort, map, and filter can become syntactically heavy (inst is your friend here)), but I absolutely love the ability to hover over an identifier and see what its type is.

1 Like