How do I use with-type to use Typed Racket fragments within untyped modules?

4
votes

The Typed Racket reference indicates that it's possible to use with-type to created “typed regions” within untyped code.

The with-type form allows for localized Typed Racket regions in otherwise untyped code.

It’s a little unclear how to actually use this, though. Obviously, using such a feature needs to take place within an untyped module using #lang racket or something similar. How should the with-type binding be imported?

A naïve attempt is just to require Typed Racket, but this causes failures with how TR overwrites existing syntactic forms.

(require typed/racket)

(struct point (x y)) ; complains about missing type annotations

Trying to use only-in to simply require with-type and nothing else sort of works, but then none of the required type bindings (such as Number or ->) exist.

It seems like the only way to do this would be to manually use only-in to import only the things that I need, but this feels laborious. I could also use prefix-in, but then of course everything would be scattered with prefixes.

Is there a recommended way of doing this, or is this feature somewhat deprecated?

2
schemerackettyped-racket

2 Answers

2
votes

I don't know the fundamental answer. A guess is that it's the sort of thing that would be useful when writing macros, as opposed to code you'd write directly?

A practical idea: You can use local-require to limit the "contamination" of the TR require. And you can flip to using except-in if that's less work then only-in.

For instance this example from the docs get close, but gives a weird error presumably because it's using TR's quote:

#lang racket/base

(let ([x 'hello])
  (local-require typed/racket)
  (with-type
    #:result String
    #:freevars ([x String])
    (string-append x ", world")))
; /tmp/so.rkt:7:21: quote: identifier used out of context
;   in: quote

Excluding that with except-in gives the desired error:

(let ([x 'hello])
  (local-require (except-in typed/racket quote))
  (with-type
    #:result String
    #:freevars ([x String])
    (string-append x ", world")))
; x: broke its contract
;   promised: String
;   produced: 'hello
;   in: String
;   contract from: /tmp/so.rkt
;   blaming: /tmp/so.rkt
;    (assuming the contract is correct)
;   at: /tmp/so.rkt:14.17

But yeah. This is just fiddling with the edges and not getting to the heart of it.

1
votes

I would just use except-in (or perhaps rename-in) to avoid the few identifiers that don't work in both typed and untyped programs. Like this modification of Greg's program:

#lang racket/base

(require (except-in typed/racket struct))

(struct point (x y))

(let ([x 'hello])
  (with-type
    #:result String
    #:freevars ([x String])
    (string-append x ", world")))