AFAIK using dependent records-as-modules in a simpler MLTT-based type systems is tricky, because singleton types (aka. 'manifest fields') usually depend on equality reflection. Has anyone applied cubical type theory to the problem of first class module systems?
Conversation
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Replying to
YES, looking into this draft I am excited! This looks really nice and useful, and I am so glad you are working on this stuff! 👏🤩
Can you see any connections with the 'phase distinction' and multi-stage programming or two-level/multi-level type theory? That's where I was hoping to find solutions (in my ignorant way). Still need to get my head around your 'synthetic phase distinction'. 😅
2
Those seem to be handy for typed macros, monomorphisation, and inlining at least - just seemed (on the surface) to be similar to how you might want to distinguish between different phases of runtime and compile time.