Anyone know of literature on preserving parametricity but also allowing static introspection like D? They seem in conflict.
Conversation
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.
1
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
This Tweet is from a suspended account. Learn more
Any thoughts on twitter.com/brendanzab/sta? This comes up when I want to pass instance records too. Like, I want to use them within the body of my function, but I also want to ensure that I get static dispatch by default. I think Idris has a `%static` annotation for this 🤔
Quote Tweet
Replying to @brendanzab @deech and 2 others
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 
This Tweet is from a suspended account. Learn more
Awesome, this is super helpful, thanks for helping me get things straightened out. I've really appreciated following your papers by the way. I'm very thankful for all the hard work you and your colleagues have put in over the years! 😀