alt Hacker NewsYeah I think this project could use a little guidance.
The real magic with types parameters is that they can both be dynamic and erased!
> That is, Syl is dependently typed at compile time and simply typed at runtime.
This is not full dependent types. And there is no reason to limit oneself this way for performance, because again dynamic + erased has no overhead.
> 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.