Great! Well, do drop me a line if I can be of any help with anything.
“Effect system” is not something precisely defined, so it’s not clear whether “the handle pattern” is a rudimentary effect system or not. I would say that it is.
If you have used effecful then you have seen a type-level handle. Consider an effectful constraint State Int :> es, and observe the role :> plays; it encodes an Int:
class (e :: Effect) :> (es :: [Effect]) where
-- | Get the position of @e@ in @es@.
--
-- /Note:/ GHC is kind enough to cache these values as they're top level CAFs,
-- so the lookup is amortized @O(1)@ without any language level tricks.
reifyIndex :: Int
That Int is the position of e in es, so e :> (e : es) encodes 0, e :> (e1 : e : es) encodes 1, etc. What are these Ints? They are indices into arrays in the Env (itself inside effectful’s monad Eff):
newtype Eff (es :: [Effect]) a = Eff (Env es -> IO a)
data Env (es :: [Effect]) = Env
{ envOffset :: !Int
, envRefs :: !(PrimArray Int)
, envStorage :: !(IORef Storage)
}
-- | A storage of effects.
data Storage = Storage
{ stSize :: !Int
, stVersion :: !Int
, stVersions :: !(MutablePrimArray RealWorld Int)
, stEffects :: !(SmallMutableArray RealWorld Any)
, stRelinkers :: !(SmallMutableArray RealWorld Any)
}
I don’t recall which array it is an index into (probably envRefs?) but in any case, the value at that index is used to determine how to perform some effect, i.e. it’s an effect handle.
So, I call State Int :> es a type-level effect handle. This corresponds to Bluefin’s State Int e, which is a type not a constraint, so its values are value-level effect handles. I’m not sure this is standard terminology, but it’s the terminology I use.
In fact that seems to be precisely what he meant!
side-effects T A = (A × S)^S , where S is a set of states, e.g. a set U L of stores or a set of
input/output sequences U∗
So, what Haskellers call “effects” is far broader than Moggi’s “side-effect”. Exceptions are “effects” for Haskellers. For Moggi it seems they’re just exceptions. Anyway, Moggi is more about semantics than programming languages, so I’m not sure it’s of much help. It was Wadler, as far as I know, who introduce monads to programming language practice.
Probably not, unfortunately, no more than I can help you with what a function is. Of course, I could say “it’s a mathematical function, as axiomatized by set theory”, but that doesn’t help with operational semantics, polymorphism (see Reynolds) or what C programmers call “functions”.
Up to isomorphism. Yet your isomorphism ignores a great deal of structure, including operational semantics.
Unfortunately, I think your wish will go unfulfilled, for now. I know of know precise definition of “effect” or “effect system”.
No, effect systems that are IO wrappers (Bluefin, effectful, ReaderT IO, etc.) can only deal with effects that have at most a single continuation. Most effects have a single continuation, exceptions have zero. Therefore IO wrapper effect systems cannot handle the style of “non-determinism” as seen in LogicT.
(And if you don’t ignore operational semantics, then of course they have all sorts of performance differences, and differences in the way they interact with Haskell’s RTS. For some discussion of the latter, see effectful’s docs.)
And indeed a type of lists that’s strict in the spine, or only part of the spine …
I think you mean 2^ℕ types of lists. Yes, I would say that. I’d also say that they are all lists.
Yes, why not? And they are all still tuples of length 10.
I’ve never found this a useful way of thinking. What non-trivial conclusion have you obtained from that knowledge?
I don’t know what that means, but I doubt it. It may well encode free and non-free models of certain algebraic theories. They will be ones that correspond to zero-or-one shot continuations.
I don’t know what they’re encoding, but something that you might like is that I draw a distinction between “synthetic” and “analytic” effect systems.
Transformers are “synthetic”. They build “effects” from language primitives and allow you to compose them. For example, StateT s (ExceptT e (Reader r)) a is an algebraic data type, just formed from the language primitives sums, products and exponentials.
By contrast, Bluefin and effectful are “analytic”. They are simply IO underneath. The kitchen sink. The whole world. There is no attempt to synthesise from smaller pieces. On the other hand, they analyse individual pieces of IO and determine how they can be partitioned into small pieces that correspond to the primitives of the synthetic approach. Thus, they come to roughly the same end building on a different basis.