3 ms·

I wrote that insanitybit post. It's unrelated to Phantom types. A session type allows you to encode a state machine into your type system. What this means is t

I wrote that insanitybit post. It's unrelated to Phantom types. A session type allows you to encode a state machine into your type system. What this means is that, at compile time, you can validate that your code can't transition into an invalid state.

agumonkey 8y ago
But state machine and communication protocols.. aren't they isomorphic ?
- staticassertion 8y ago
  Sure, feel free to read 'communication protocol' where I say state machine.
  - agumonkey 8y ago
    oh ok; I double-misread your above comment. My assumption was that phantom types were also about encoding state machines in types and thus could work for communication protocols too just like your session type article; hence the question about the difference between the two.
    - staticassertion 8y ago
      Oh, yes, I see the miscommunication now. Phantom types can be leveraged in a similar way, where a type (the phantom type that you are generic over) represents that state. To answer your question - the end result of both approaches is a session type with the same guarantees. I've seen that approach used but I can't really comment too much on the differences as I've never used it myself. I find my approach simple in practice (I've shipped Python code that takes the same approach, sans affine types) because it separates the types out. So, essentially, I write my non-sesssiony struct with all of its methods, and then I wrap that in the session types. This lets me easily drop into the non-session type if necessary, and the sessions types act as thin wrappers. My imap client worked the same way, if I recall. The downside is likely boilerplate.
      - agumonkey 8y ago
        is the python code public ? I toyed with phantom type in kotlin recently (toy examples); I'm curious how it would be done in python.
        staticassertion 8y ago
        It's not. The short answer is it's the same thing as Rust, except instead of a compile time guarantee that your state isn't reused I have an assertion and test coverage.
        agumonkey 8y ago
        aight, thanks

agumonkey 8y ago

But state machine and communication protocols.. aren't they isomorphic ?

staticassertion 8y ago
Sure, feel free to read 'communication protocol' where I say state machine.
- agumonkey 8y ago
  oh ok; I double-misread your above comment. My assumption was that phantom types were also about encoding state machines in types and thus could work for communication protocols too just like your session type article; hence the question about the difference between the two.
  - staticassertion 8y ago
    Oh, yes, I see the miscommunication now. Phantom types can be leveraged in a similar way, where a type (the phantom type that you are generic over) represents that state. To answer your question - the end result of both approaches is a session type with the same guarantees. I've seen that approach used but I can't really comment too much on the differences as I've never used it myself. I find my approach simple in practice (I've shipped Python code that takes the same approach, sans affine types) because it separates the types out. So, essentially, I write my non-sesssiony struct with all of its methods, and then I wrap that in the session types. This lets me easily drop into the non-session type if necessary, and the sessions types act as thin wrappers. My imap client worked the same way, if I recall. The downside is likely boilerplate.
    - agumonkey 8y ago
      is the python code public ? I toyed with phantom type in kotlin recently (toy examples); I'm curious how it would be done in python.
      - staticassertion 8y ago
        It's not. The short answer is it's the same thing as Rust, except instead of a compile time guarantee that your state isn't reused I have an assertion and test coverage.
        agumonkey 8y ago
        aight, thanks