Has anyone succeeded in implementing or designing a type-system that combines both type-state (linear types) and effect types (e.g. Koka)?

  • $\begingroup$ Kitten has some linear typing (still being figured out) as well as an effect system based on Koka’s. $\endgroup$
    – Jon Purdy
    Commented Jun 21, 2016 at 1:07

2 Answers 2


Edwin Brady has done some work in that area using dependent types in IDRIS. Take a look at his work, in particular Programming and Reasoning with Algebraic Effects and Dependent Types and Resource-dependent Algebraic Effects.

  • 3
    $\begingroup$ Welcome and thanks for your answer! Could you give at least a very brief summary of what the linked preprints contain? That way, your answer would be more self-contained. A few sentences would be fine. $\endgroup$ Commented Jun 16, 2016 at 10:10
  • $\begingroup$ Dependent types are very heavy to use. I was hoping for a system more like Rust + Koka. $\endgroup$ Commented Jun 16, 2016 at 14:14

A lot of work on types for $\pi$-calculus does this. See e.g. (1) for a unified system. Sequential languages can be embedded into $\pi$-calculus, so this work also applies to sequential languages.

(1) A Uniform Type Structure for Secure Information Flow, K Honda and N Yoshida.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.