@[email protected] @grainloom wish I had satisfying answers. I ought to explore Rain’s suggestions more sometime.
There seems to be tension between how much is done at compile-time (validation, code generation, optimization) and run-time. Many intentionally designed type systems use type erasure to intentionally lighten the output and prevent runtime cheats. Idris does some clever tricks to determine which dependent types need to be checked at runtime.
@[email protected] @grainloom I think dynamically typed languages tend to have better runtime introspection, but there’s nothing fundamentally preventing that with strong, statically typed langs. I’m exploring BEAM languages largely because I appreciate how much runtime introspection and interaction it offers.
OTOH, those benefits also weaken runtime security properties depending how you use it.
@[email protected] @grainloom Typed Racket is another interesting point isn’t the design space. Broadly it’s using gradual typing to ease interoperability with the untyped stuff, and it has to do more work at runtime than many compiled langs.
Generally Racket’s concept of phases blur the distinction a bit between compile-time and run-time, while maintaining explicit control. I haven’t gotten used to using them directly yet, but it seems like a useful concept.
Jake Mitchell