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
Oooh! I'll check that out! Btw you can see some of my blunderings around this here (I'm a bit slow to understand all these complexities haha):
1
1
Been definitely interested in stuff like Granule that is trying to add modalities to type systems in a nice way - seems really handy for systems programming stuff, and maybe modular programming too.