alt Hacker News> And there is no reason to limit oneself this way for performance, because again dynamic + erased has no overhead.
Not entirely, since Syl uses static data to describe types' runtime layout. Allowing dynamic there would require overhead (e.g. a uniform representation).
That said, there's not a good reason to prevent types from ever mentioning dynamic values. I didn't include it in the post as I haven't entirely thought it through, but with OxCaml-style modalities, you should be able to mention runtime data in types under a dynamic modality.
> Not entirely, since Syl uses static data to describe types' runtime layout. Allowing dynamic there would require overhead (e.g. a uniform representation).
This is where it is crucial to distinguish types from layouts. "uniform representation" means the layout is static while the type is dynamic. But this isn't an overhead in the sense of dynamic checks or lack of erasure.
Having static (erased) layout parameter and dynamic (erased) type parameter is the fully-general solution: monomorphization per layout, not type. And the caller decided whether to thread a layout parameter, or fix a single layout.