When will we all have effect systems?

It seems effect types are things people want, but few languages have managed to reify them, make them something we can all use. (Like, in -- cough cough -- Java et. al.) Any thoughts on how/when it will get to be more mainstream? Good enough that you'd risk using in production (at least w/in a group that is a little on the cutting-edge)? What things should a decent effect system support? Not only null checks I hope. (I was wondering about, via 'pilud' list, is how to rigorously handle immutable/mutable conversion/interaction.) Or are we just stuck with monads and related transformer boilerplate (and confusion to people like me)?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

What is an effect type?

After looking at the abstract of the first linked paper, my guess is that in a functional language aiming to avoid side effects, you want a type to abstract side effects. Is that close?

Definition of effect.

For folks asking the same question I did, an adequate definition of effect appears in the summary of fx91-report.pdf linked last in the OP. It says the unique features of FX include:

An effect system, to discover expression scheduling constraints. An effect is a static description of the side-effects an expression may perform when it is evaluated. Just as a type describes what an expression computes, an effect describes how an expression computes.

I call that a first rate definition of effect due to brevity and clarity in one short sentence, and due to an excellent analogy via comparison to types.

If this definition applies — where effect contrasts with type — then the phrase effect type looks like a types-über-alles construct that aims to reify effect ontology in terms of types. Say, while we're at it, is there also a reification of time in types, too?

Time (and Space) in Types

is there also a reification of time in types, too?

For my work on reactive demand programming, I model both time and space in the type system.

For time, I model the static, logical latency of every function. Latency is a rational number of seconds. A logical `delay` operation will delay access to a value, which might be associated with an expensive computation or communication. It is possible to logically synchronize concurrent operations by introducing logical delays. Physical latency might be less or more than logical latency, often less due to conservative estimates and speculative evaluation.

For space, I model computations as occurring in 'partitions', with explicit `cross` functions that move a value from one partition to another. These partitions are often heterogeneous, e.g. GPU vs. CPU, or client vs. server, or "the OpenGL thread" vs. "the Filesystem adapter thread". They may also be distributed, in which case the `cross` function must allow for disruption.

In general, to combine two values (e.g. to add two integers) requires that both integers have the same time and space coordinate, which is validated in the type system. One aspect of computation, then, is moving values about from one partition to another, and the RDP application can be understood to be 'distributed' among partitions. Similarly, if you want to execute a dynamic function, it must fit within the correct latency profile, be capable of accepting values at the correct partition, and emit values at the correct destination.

There is also a valuable role for 'ripening' and 'expiration' of values - i.e. a `use-by` latency and a `do-not-use-before` latency. These help with garbage collection, security, and are essential for linear types.

I find temporal-spatial types to be fascinating and extremely valuable. I haven't seen much use of them outside my own research and design, but my initial inspiration for partition types was from an FRP implementation in Haskell, called Sodium.

What a good response, cool.

That's pretty interesting. I tend to think in terms of space and time models with some structure to them, but never think about representing them with first class mechanisms. Instead that part is just informal background story for context explaining tools targeting space and time effects, without a mechanism for direct manipulation.

I like your description generally, and especially favor use of model in both noun and verb senses. Without getting nit-picky, verb to reify roughly means to model but with several flavors of qualification connoting precise, complete, explicit, and/or direct, etc, in a manner implying to model thoroughly with respect to certain essential details needed to capture a system represented and reasoned about. So model and reification seem roughly synonyms when you squint, but model can be far more inexact, shallow, and suggestive. Maybe all reifications are models but not vice versa, in a way like all squares are rectangles but not vice versa.

My following remarks are only indirectly related to models of space and time in a computing system. From the late 80's to mid-90's I was vaguely interested in making a kind of game engine with parts suitable for defining complex systems of behavior in a simulated world, where players situated within games could achieve increasingly direct control over models — represented as magic or science — in a way forcing one to reason better and learn what amounts to programming skills, but disguised as "fun" while achieving game objectives. My interest in programming languages came partly from wanting to script such things, and my interest in storage systems came from obvious need to persist elements of extended game worlds. Game world modeling is the only sort of application I find interesting, but I have never done it, and current game markets are now entirely about high end art assets and first person shooter dynamics, which doesn't require a very interesting model anyway. (Unless you can redefine how reality works, as a contest of wills between players, games seem just a bit limiting to me.) To make a living I define and optimize models other folks want in systems, but really all I'm doing is moving bytes around. Most web apps today seem like variations of gossip engines (read: pointless), so I just optimize and scale without caring about the trivial end goals of chatting and exchanging documents. Does that read like a capsule summary of career disillusionment, or what? :-)

Anyway, it sounds like you have something worth pursuing in there somewhere. Thanks for both your posts, the one above and that below, which are giving me things to think about. If anything technically interesting comes to mind later worth describing, I'll post more.

Effect types

the phrase effect type looks like a types-über-alles construct that aims to reify effect ontology in terms of types

Effectively. ;)

One could understand Haskell's use of monads as a basic effects typing model. E.g. there is a big distinction between `a -> b` and `a -> IO b`. The trouble is that monads aren't convenient to compose. It's painful to model a lot of precise subsets of IO using monads.

Recently there has been much work on Algebraic Effects, which treat effects much like exceptions, having 'effect handlers'. With that understanding, an approach similar to checked exceptions would work for the effects model. Presumably, you could even have 'effect hierarchies' i.e. where you can specialize existing operations but use the existing implementation if the more precise one is not handled. Algebraic effects are more precise and composable than monads.

The 'partition' types I mentioned above can also be leveraged as a basis for effect typing. The idea there: operations are associated partition typeclasses, and a partition may be an instance of multiple classes. Since partitions are heterogeneous, they may have different effects available to them. The set of typeclass dependencies for the function would represent the effect type. (However, I aborted an effort along these lines due to Haskell's type inference system giving me headaches.)

Since I'm interested in heterogeneous computation, I favor systems that are a fair bit more precise than `pure vs. IO`. I want heterogeneity even within the pure computations, e.g. due to varying support for matrix operations or recursion (CPU vs. GPU). The partition-based approach and algebraic effects are both promising, IMO, but I'm having some difficulty reconciling them (in a simple, correct, and convenient manner) with capability security and precise grants of authority. It may be I want effect types only for the pure ops, which would belie their name.

Koka!

Plaid, Mezzo, Rust

I think Koka is an excellent reference: the work on inferring effects, and general usability of effect systems, is an important complement to some more expressivity-oriented approaches such as DDC or Eff, Frank, Idris. In the same vein and also with Daan Leijen, Lightweight Monadic Programming in ML (LtU) is less ambitious but also nice.

I'm interested also in "permissions"-oriented programming languages: Plaid of Jonathan Aldrich et al. in the object-oriented world, and Mezzo as a rather more functional-oriented language, stemming from the more fundamental typed-capabilities work of François Pottier.

Scala

We're working on an effect system for Scala: https://github.com/lrytz/efftp/wiki

Some of the goals are lightweight annotations for effects, but also for effect-polymorphism, and providing an extensible framework that allows new domains to be implemented easily. Currently the implementation checks IO, exceptions and purity.

Frank

Effects and Monad Transformers

It seems to me that effects try to solve the problem of collapsing stacks of monad transformers.

Let's say that reading from stdin is done with the monadic function "read :: StdIn String" and writing to stdout is done with the monadic function "write :: String -> StdOut ()", and I want my program to have type "StdIO ()" which allows "read" and "write" but no other side-effects. I could do this with monad transformers, but "StdInT StdOut" is distinct from "StdOutT StdIn", even though they are equivalent. Also, I can't use "read" and "write" directly, one of them needs to be wrapped in "lift".

In Haskell we have to deal with this by either manually sprinkling "lift" all over our code, or writing custom monads for every type coercion we need (including between our custom monads!), or dumping everything in IO.

In an effect system, our type contains a list of effects, so "read :: Effect [StdIn] String", "write :: String -> Effect [StdOut] ()" and we can define "StdIO = Effect [StdIn, StdOut]". "read" and "write" can both be lifted automatically to the StdIO effect type.

Now, in a dependently-typed language like Idris, we should be able to prove that two monads commute. For example, we could prove:


stdinStdoutIndependent :: StdInT (StdOutT IdM) = StdOutT (StdInT IdM)

We can collapse any stack of monad transformers into a single monad if we have a proof that the levels commute. In the majority of cases, ie. those which effect systems target, these proofs are trivial and thus can be inferred. This basically automates the 'custom monads for type coercion' option above.

Our code would look something like this, where {} indicates a set:

myRead  ::           Collapsed {StdIn} String
myWrite :: String -> Collapsed {StdOut} ()
myCat   ::           Collapsed {StdIn, StdOut} ()
myCat = do s <- myRead
           myWrite s
           myCat

I tried to do this a few months ago, but kept hitting a wall when trying to implement those sets. I didn't want to use something hacky like string IDs for the types, so after playing with reflection for a while I gave up.

Note that the Idris effect system seems to use string IDs for types, so this might be unavoidable :(

My questions are thus:
* Can we use proof obligations that our monads commute to get something like an effect system?
* Can we do it in a user-extendible way, without relying on hacks like comparing strings?
* Would such a system just be isomorphic to an effect system?

Monads and Effect Systems

Quoting from The Sequential Semantics of Producer Effect Systems by Ross Tate speaking about The marriage of effects and monads:

Wadler and Thiemann famously showed that one of Talpin and Jouvelot’s effect systems can be formalized by what has become known as an indexed monad. An indexed monad is a join semi-lattice of monads connected by monad morphisms. The semantics of sequencing effectful computations was defined by coercing both computations to the least common supermonad and then using the join of that monad.

Aha! Thanks, that's exactly

Aha! Thanks, that's exactly what I meant :) I was having one of those "surely someone's thought of this before?" moments.

Alternatives to text editor for source code

One issue with very complicated effect typing could be the way it clutters the source code and its readability. If I was working with a system that had many different effect types, I imagine that source code with complicated effect types would benefit by having some type of collapsing view, so that the effect types can be declared in the place they are used but could show up as short collapsed strings when browsing source (color syntax highleted, etc.)

Programmers are traditionally reluctant to give up their favorite editors/key bindings etc. So making something like that practical essentially involves a kind of applied research project to implement a common framework/format for replacement editor/IDE to build around, with popular alternatives basically implemented to start with.

Or you know....one could use

Or you know....one could use a language with effect inference.