Munksgaard / session-types

MIT License
550 stars 21 forks source link

Added .pop() to Chan as a complete alternative to .succ() and .zero(). #26

Open ebfull opened 8 years ago

ebfull commented 8 years ago

.pop() will automatically bring the type upward from the "recursive" depth indicated by Var<N>, obviating the need for .succ().succ().succ().zero() or similar things.

Closes #25

ebfull commented 8 years ago

One thing I have not tested is how far the compiler is willing to resolve this recursively, though I'm sure similar issues pop up anyway with highly recursive protocols.

laumann commented 8 years ago

I like this - IMO it's mostly an ergonomics thing, but it still adds value. :+1:

Munksgaard commented 8 years ago

Yeah, I like this too. One thing that might be a concern is if error messages get polluted with Pop types. I can't test it right now, but I'll try to take a look at it tonight.

laumann commented 8 years ago

I understand this a little better now - pop() substitutes zero() as well, right?

EDIT: This sounds like a really silly question in hindsight...