[saityi]

> Edit: Can someone tell me... Is it necessary to have a new type system or could this be done with dependent types?

I played around with trying to implement an effect library (via the research) in dependently typed languages (Idris, Agda) and found type inference issues to be too much to work around. I found I was having to help the type checker along at every step -- explicit signatures on everything and, in Haskell terms, type/proof applications on function calls. On the other hand, I have found Koka -- until I started pushing the type system to its limits -- to require no hand-holding to figure out how to type its set of effects.

I am curious if a dependently-typed wizard could figure out an encoding to make these issues go away, but it was beyond my capability.