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
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
Yeah, I was thinking you could have (using Idris' multiplicity notation):
id : {0 a : Type} -> a -> a
Which would mean that you could never introspect the `a`. I think Dependent Haskell uses the `forall` and `pi` types to distinguish between these.
2
This Tweet is from a suspended account. Learn more
Yeah, I definitely think I've been a bit confused by this! I did watch your 'worldly types' talk a couple of months ago. Is that what you are referring to here? And you're saying multiplicity 0 does not imply that a type can be in 'heaven'?
1
This Tweet is from a suspended account. Learn more
Right, that seems to be the source of my misunderstanding. The fact the they result in the same outcome (erasure/static use), but they are arrived at from orthogonal means.
Any thoughts on how this also might integrate with coeffects. It'd be nice to add other things to my binders - not just multiplicities and worlds. Could a future integration also allow for more flexibility there as well?
1
1