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
It sounds like someone should invent them 😁
1
2
Replying to
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
Ooooh cool! This is one thing I was hoping PL people would eventually start working on!
2