IRC channel logs
2025-12-09.log
back to list of logs
<cwebber>where the contracts between the boundary of typed racket and untyped racket lead to explosive performance cost <identity>we just need to use our gradual-typing stuff to convert all of our code into the typed subset non-gradually <cwebber>I think the more linter-like approach of typescript and python's typing system has turned out to be more successful <cwebber>one thought was that typed racket would make programs faster, because the soundly typed parts could be statically optimized <cwebber>but the contract costs far outweighed that <cwebber>so an approach like typed racket but where the types at the perimeter are maybe more selectively enforced and otherwise are linted might be better <dthompson>one the biggest issues to static typing as a DSL inside Scheme is that you can't, in general, optimize across procedure boundaries. <cwebber>cps soup does sometimes with inlined stuff, right? but the "in general" is the thing <dthompson>right, if you inline a bunch of stuff into the procedure you can get a lot of benefits <dthompson>but once you make a call to the outside you have to do all the type checks again <cwebber>in other words, if you make a rewritten version of the procedure when you see a code path that can be more efficient, you can optimize that part of the soup by writing a special path version of it <cwebber>but, in general, the procedure is a ravioli <cwebber>and can be accessed by things you don't even know in the future <dthompson>when all call sites are known, lots of optimizations are available. when you don't know, you have to follow the general scheme calling convention <dthompson>like you can use contracts to indicate that this procedure should only accept a float for x: (define (incf x) (+ x 1.0)) <dthompson>but now consider another typed procedure that calls incf: (define (foo y) (* (incf y) 2.0)) <dthompson>and let's pretend there's a contract on it such that y is also a float <dthompson>leaving aside inlining, etc. the call to incf is going to re-check that it was passed a float even though the caller already knows it's a float <dthompson>in the general case each procedure is an island and it has to enforce its contract at the border <dthompson>what I would like is a statically typed scheme-ish language that can have its own internal calling convention that doesn't have this problem but exports wrappers that can be called from scheme that do the dynamic type checking only at the entry points. <dthompson>fun fact: this is how hoot's wasm interpreter handles functions! <dthompson>a wasm module can export a function and it's callable from scheme. wasm functions are statically typed so we have to peform some type checks at the scheme/wasm boundary. <dthompson>however, it's also possible to import a wasm function into another wasm module. dynamic type checks would be wasteful in this case because both sides have already done the static type checking, so there's a fast path that skips all that. <dthompson>okay ramble over. hopefully someone finds this interesting ;) <cwebber>dthompson: that sounds a lot like typed racket! <dthompson>yeah I figured they would do something like this <cwebber>dthompson: I recommend reading the above paper :) <dthompson>this paper seems to be about gradual typing, which is different <cwebber>will be interested in whatever you do, dthompson :) <cwebber>also something something we should use propagators for the type solver ;) <dthompson>I guess what I had in mind was less of a mix between typed and untyped code, which definitely will have a lot of type checking overhead. <dthompson>I mostly want to be able to write some fully statically typed code for some performance/correctness critical component and then call into it from scheme. I'm less interested in typed code calling out to untyped code. <dthompson>there have been several occasions where my guile optimization efforts have been thwarted by a procedure call boundary. <weary-traveler>if the manner in which the performant/type-safe code is restricted, one can avoid type-checking overhead considerably. two approaches come to mind. one, have a lazily-describe-then-run semantics. similarity to things like STRef monad in haskell. this doesn't help the situation where you have interleaving of build-run. <weary-traveler>for the latter, the trick that could work is to pick a representation domain that allows you to propagate the proof-witness for the invariants of the output along with the output <weary-traveler>in short, i think it's quite doable. the specifics would depend on the specific problem however <dthompson>it's just not doable in scheme. fortunately guile is a multi-language vm so we can compose scheme with another language that has the properties we want. <jfred>maaaan I got added to a meeting tomorrow... at 2pm x.x <jfred>it's half an hour so maybe I'll be able to catch the last half of the office hours