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.
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? ;-)