This is nice, but makes it hard to use Typed Racket to handle define-type and generate contracts.
Those actions require the type checker's "global" context, but a local require/typed/scv can't get access to that.
and works by (1) fully expanding FILE.rkt (2) parsing the contract defs from the fully-expanded code ... which should be possible (3) running raco scv on a rewritten untyped module (4) maybe rewriting FILE.rkt to have unsafe-require/typed
So it's very clearly a pre-processor, and you're not running SCV every time you raco make, and it re-uses the important parts of Typed Racket without any changes to Typed Racket.
OH BY THE WAY the generated FILE2.rkt should have a checksum for the untyped file it depends on. That would be very cool and useful.
The current API is:
(require/typed/scv ....)
formraco make FILE.rkt; racket FILE.rkt
like normalThis is nice, but makes it hard to use Typed Racket to handle
define-type
and generate contracts. Those actions require the type checker's "global" context, but a localrequire/typed/scv
can't get access to that.Alternate API
(require/typed/scv ....)
formraco scv-expand FILE.rkt
generatesFILE2.rkt
(or whatever)FILE.rkt
(2) parsing the contract defs from the fully-expanded code ... which should be possible (3) runningraco scv
on a rewritten untyped module (4) maybe rewritingFILE.rkt
to haveunsafe-require/typed
So it's very clearly a pre-processor, and you're not running SCV every time you
raco make
, and it re-uses the important parts of Typed Racket without any changes to Typed Racket.OH BY THE WAY the generated
FILE2.rkt
should have a checksum for the untyped file it depends on. That would be very cool and useful.