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
Hey, been pondering this today (been wanting to implement this in Pikelet), and been curious whether you know of any existing implementations of singleton types that don't rely on equality reflection? Or is that something yet to be done? Kind of wondering how easy 'easy' is. 😅
1
1
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
Yeah I think you bring those up in the Logical Relations as Types paper?
2
1
Hoping that I can try to implement singleton types, then later on extend (??) them to be those extension thingies?
1
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Oh, and one thing I'm hoping to do is have each source file be an expression - wired together by the build system in a way that's similar to what's talked about in "A Principled Approach to REPL Interpreters":
1
1
1
But yeah, got a bit to go before I get to that stage 😬