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
Replying to
Also aware of the other tricky issues around combining subtyping in dependent types? Generative modules might also be problematic… given that these are kind of 'effectful', which is always a bit fun?
1
Replying to
And these kinds of tweets remind how much more I still need to learn about PL. Though I do plan to include OCaml modules in my next video (after the interview coming out shortly).
1
3
I think module systems are fascinating! But also the way they are presented is often rather confusing, with bewildering set of terminology to learn. I hope we can make this stuff more approachable in the future!
1
1
Show replies
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
Show replies
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
Show replies
In the sense of an ML-style module. Where you have ‘module types’ (known in SML as a ‘signatures’), ‘module instances’ (known in SML as a ’structures’), and ‘module functions’ (known in SML as ‘functors’):
1
Show replies