Anyone know of literature on preserving parametricity but also allowing static introspection like D? They seem in conflict.
Conversation
Replying to
You can have your cake and eat it if you have two different quantifiers. One that admits introspection, and one that doesn’t. Definitely interested in this for Pikelet, because static type dispatch is super important for systems programming.
Here is a post by on it: stackoverflow.com/questions/2322 - not sure how this links in with the later work on Quantitative Type Theory though. Ie. multiplicity=0 (erased) seems to imply parametericity, but doesn’t say that explicitly in his paper.
2
1
Also, thinking about it now, you might want to ensure that introspected types are still thrown away at compile time, so maybe it’s still useful to maintain the distinction 🤔
1
1
Show replies