Thank you. I really appreciate your help. I upgraded to Racket 7.8, latest available package on the website. I’ll keep an eye on the server and see if the problem goes away.

looking at @ben ’s upcoming RacketCon talk about contracts (Shallow Typed Racket), I wonder if there’s such a thing as “compile-time-only Typed Racket”. It would be just like Typed Racket, but no contracts would be added at runtime. I want to use the types at compile time only. The idea is that if a module passes through the type checker, I want just plain old racket to come out. No additional contracts beyond the ones already baked into #lang racket. Does that make sense? Perhaps one could fake it with a new require/typed/uncontracted form that would allow me to pull in TR code sans additional contracts. Maybe what I describe already exists, but I just don’t know about it.

There’s unsafe-provide. There’s not a way to import things without the invariants the types imply unless the module you’re importing sets that up.

The reason that we haven’t added typed/racket/optional is that then the types are just sort of hints, but you can’t trust them.

ah, I see. So if I have a TR module that unsafe-provides a function f and if I typed/require f in a #lang racket module, then the runtime behavior of f in that module won’t have the extra contract implied by the type of f in the TR module?

I’m not sure I understand the intuition behind saying that the types would be mere hints. Sure, they’d no longer have any runtime significance, but getting a big chunk of code to go through the TR type checker is, to my mind anyway, a pretty strong sign that my code is good(ish)

or to put it another way: what can be done to close the gap, and make the hints (the types) more confidence-inspiring (that is, to remove the “mere” from “mere hint”)

There isn’t a typed/require for you’d use in plain #lang racket. If you use TR to define a function, you can just require that from plain racket. If you use provide, that will have a contract. If you use unsafe-provide, it won’t have a contract.

perhaps I’m thinking about types in an unintended way. I guess I’m thinking about them the way types would be handled in, say, C

The sense in which they’re just hints is that if you write (lambda ([x : String]) ...) in Typed Racket, you can trust that x is a really a string in the body of the function. If you remove the contracts, then that’s not true any more.

perfect, thanks for clarifying. I think that’s what I’m looking for, at least, that’s the answer for how to make TR “unctracted”

perhaps what I have in mind here is another #lang (“Fast TR”), or some kind of parameterized version of TR

yes I’m hoping to add a “typecheck only” lang too in the Shallow pull request

For now you can use the live-free-or-die package to get TR code without contracts. (The pkg name is a great summary of the kind of excitement you should be ready for.)

And that’s not even mentioning the alias for the exported form :smile:

I would recommend against using unsafe-provide: the TR code might be optimized in such a way that, if you call a function provided unsafely with the wrong arguments, the entire application will crash (i.e. segmentation fault).

This comment explains a bit more: https://github.com/racket/plot/blob/4df34897acba74f689954188183e367c160911b8/plot-gui-lib/plot/private/gui/plot2d.rkt#L5

And if the comment is too long, this is the important bit: https://github.com/racket/plot/blob/4df34897acba74f689954188183e367c160911b8/plot-gui-lib/plot/private/gui/plot2d.rkt#L19

FYI, it sounds like the sort of concept you’re aiming for is roughly the approach that Rust takes to something of an extreme - type the heck out of everything at first to provide all sorts of checks and guarantees, but remove many (if not all) of the typing information from the final executable.

@jcoo092 yeah, that’s essentially what I have in mind

thanks for all the discussion! This has been illuminating.