Conversation

Anyone know of literature on preserving parametricity but also allowing static introspection like D? They seem in conflict.

Brendan Zabarauskas

@brendanzab

May 10, 2018

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

@bentnib

doesn’t say that explicitly in his paper.

Brendan Zabarauskas

@brendanzab

May 10, 2018

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 🤔

deech

@deech

May 10, 2018

Nice! I was thinking along the lines of a linear variable that get consumed when a type is introspected, so eg. id :: a -> a is still has only one possible implementation if a's associated linear variable (not pictured here) is intact.

Replying to

and

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:26 AM · May 10, 2018Twitter Web Client

Replying to

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

This Tweet is from a suspended account. Learn more

Brendan Zabarauskas

@brendanzab

May 10, 2018

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'?