What connection, if any, is there between ML modules and PureScript-style records/rows? Also, if there is a relationship, what is the module-world equivalent of row polymorphism?
Conversation
Yeah, it seems nifty at first, but seems like it would be a pain later on. I am surprised that the thesis paper for Agda seems to describe a cumulative hierarchy, where as in actuality it seems to be implemented in a stratified way...
1
2
I might be using my terminology incorrectly though - I’ve been assuming ‘cumulative’ means that there is subtyping to make things less annoying...

