# Type-and-effect systems, stochasticism and effect squelching: how about quicksort?

There's a feature of Haskell's type system which bugs me: you can't implement a randomized sorting algorithm without the use of randomness spilling out into all of its callers. That seems undesirable.

I know in vague terms that there' something called type-and-effect systems, and I guess those are the ones you would use to describe a randomized QuickSort.

It is the case that QuickSort consumes entropy and doesn't emit any, unlike the Fisher-Yates(-Knuth) shuffle which has randomness both in its input and its output. I think it should somehow be possible to specify two effects, e.g. takes-entropy and yields-entropy such that QuickSort can be validly type+effect-checked as having one effect and the FYK-shuffle as having both.

A lower bound on their effects can probably be inferred easily when they call rand() or its equivalent. If you annotate quicksort, being a sorting algorithm, as yielding an output which is sorted and which contains the same elements as the input but in a different order, can you also infer that the randomness won't leak out---that is, an upper bound of anything-except-yield-entropy on the effect---of QuickSort?

Is this approach viable? Is it useful? When it comes to stochastic effects, I think what most callers would care about is whether the outputs of their callees are random, i.e. it's the yields-entropy effect which is the most likely to introduce bugs in your programs, and thus the interesting one to limit, which is why you would want the narrower type for QuickSort.

Are my thoughts here remotely correct? Do they make sense? I'm not versed in effect systems, but I think this idea might work. How does it connect to the established literature? Am I on to something? If so, why hasn't this been done yet? ;-)

-
The state monad can be used to squelch effects, perhaps by combining it with the Random monad transformer to throw some randomness in there. –  Dave Clarke Feb 23 '13 at 15:17
@DaveClarke: how so? Let's say I have a single-threaded program with a global PRNG. Can I put everything inside the takes-entropy monad and only FYK-shuffle but not quicksort in the yield-entropy monad? If so, how? (Oops, takes-*pseudo*-entropy is probably a better name, but I take it you know what I mean) –  Jonas Kölker Feb 23 '13 at 15:26
Maybe what I mean is this: can I have a get-random-tape-for-QuickSort inside the Random monad and a QuickSort outside of it, with the callers of QuickSort also being outside the Random monad? In other words: is there a type-and-effect system where effects can go away? It seems like it should be the case: if the throws of Java can be captured tightly in an effect system and callers can squelch the throws-effect of the callees by catching all checked exceptions, surely you could declare "throws RandomResult" and a no-op catch block... –  Jonas Kölker Feb 23 '13 at 16:58
The state monad hides the computational effects ... or at least, the ones involving state. John Riecke did some work on type and effects systems where one could encapsulate effects, I think in a paper called "Isolating side effects in sequential languages. –  Dave Clarke Feb 23 '13 at 21:37
Again, how would QuickSort and FYK-shuffle differ using Riecke's encap thing from that paper? Judging from the summary description, it sounds like nothing more than using only local mutable variables, IOW the state monad. Maybe what I want is to express in the type/effect system that "this procedure takes a random tape as its input and consumes some bits on it, but the output doesn't depend on the random bits on it". That way, I can put my whole program in the consumes-random-bits monad without putting it in the can-produce-random-output monad. If that makes sense... –  Jonas Kölker Feb 24 '13 at 11:53
show 1 more comment