4 ms·

The design of Effekt revolves around a different view of effects and effect types. Traditionally, effect types express which _side effects_ a computation might

The design of Effekt revolves around a different view of effects and effect types. Traditionally, effect types express which _side effects_ a computation might have. In Effekt, effect types express which _capabilities_ a computation requires from its context. This[1] sounds similar to some access control systems. Interesting. While this new point in the design space of effect systems impedes reasoning about the absence of effects, we demonstrate that it significantly simplifies the treatment of effect polymorphism and the related issues of effect parametricity and effect encapsulation. A useful definition for those not in the know: Effectful expressions are expressions that depend on or modify the context they are evaluated in Edit: Can someone tell me... Is it necessary to have a new type system or could this be done with dependent types? 1. http://ps.informatik.uni-tuebingen.de/publications/brachthaeuser20effekt/ http://ps.informatik.uni-tuebingen.de/publications/brachthae...

mananaysiempre 5y ago
You can do almost everything with dependent types, but dependent type systems expressive enough to be practical are usually heavy, permit almost no (guaranteed) inference and tend to require a total language (unless you toss out soundness, like TypeScript does with its non-dependent types). The hope is usually that a weaker system might relieve some of these problems; besides, studying the weakest type systems that can express whatever it is you want is good mathematics in any case. I’m absolutely hoping for a practical dependently typed language as well, but we still have a ways to go there.
saityi 5y ago
> 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.

mananaysiempre 5y ago

You can do almost everything with dependent types, but dependent type systems expressive enough to be practical are usually heavy, permit almost no (guaranteed) inference and tend to require a total language (unless you toss out soundness, like TypeScript does with its non-dependent types). The hope is usually that a weaker system might relieve some of these problems; besides, studying the weakest type systems that can express whatever it is you want is good mathematics in any case. I’m absolutely hoping for a practical dependently typed language as well, but we still have a ways to go there.

saityi 5y ago

> 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.