Yes, it's super difficult to limit the receiving end. If you use a mailbox type, it quickly needs to handle basically all shapes of data. Session types or simil

Yes, it's super difficult to limit the receiving end. If you use a mailbox type, it quickly needs to handle basically all shapes of data. Session types or similar are needed to get all guarantees we want but are super complicated. I looked at this in my MSc thesis "Singly typed actors in Agda": http://studentarbeten.chalmers.se/publication/256251-singly-typed-actors-in-agda-an-approach-to-distributed-programming-with-dependent-types http://studentarbeten.chalmers.se/publication/256251-singly-...