I am working on type-changing operations for distributed data structures for my MSR internship, it's all going to be public and (hopefully) mechanised in Agda 😁
Conversation
woah does this mean you are wanting update types in a distributed system somehow?
1
2
Possibly? I never heard of update types, what are these?
1
1
oh lol I meant 'to update types' 😳
2
2
Oh yes, this is exactly what we want! Furthermore we want to update parts of types and keep track of what parts we touch, for which we think row types and what we call "data dependency annotations" are a good solution.
1
2
Replying to
Ooooh cool! This is one thing I was hoping PL people would eventually start working on!