Lambda the Ultimate

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?

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.

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.

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.

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.

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 what I meant :) I was having one of those "surely someone's thought of this before?" moments.

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