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
Caveat being (as previously stated): I don't know if a multiplicity of 0 implies parametericity - you might *still* need separate quantifiers if not.