I'll read between the lines and just say, "Send us a link to your paper when it's done" (-:.
In fact, we'd really love it if gradual typing folks would tell us what set of primitives they miss in a language. They aren't constrained to what Racket or Python or whatever; there may be a primitive that makes sense that Pyret can add to enable space-efficient, semantically-meaningful contracting or gradual typing in the presence of such operations.
As one of those gradual typing folks, I'm not sure what you mean by "primitives we miss". The things I'd want for space efficiency are things like a contract language with decidable 'and', and for regular efficiency, a compiler that is good at seeing through wrappers.
Though I'm not enamored of the Typed Racket style of wrapping everything at the boundary (even as I appreciate why it's there). Not even hypothetical: we actually began developing Pyret in TR but, with great sadness, ended up having to move it out because of the enormous performance hits.
But neither of those is a "primitive". The first is a major restriction on contracts (and not a restriction Pyret enforces, AFAICT). The second isn't a language feature at all. How would having a new language help give me either of these?
And yes, soundness + interoperation + structural types = heavy performance cost. You can give up on one of those easily, but the combination can't be free.
But the best way to make TR programs not pay that cost is to not cross the boundary all the time, which it sounds like is what you were doing. Why was that necessary?
