<p>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.</p>

<p>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.</p>

<p>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. <code>takes-entropy</code> and <code>yields-entropy</code> such that QuickSort can be validly type+effect-checked as having one effect and the FYK-shuffle as having both.</p>

<p>A lower bound on their effects can probably be inferred easily when they call <code>rand()</code> 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?</p>

<p>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 <code>yields-entropy</code> 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.</p>

<p>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? ;-)</p>

CC BY-SA 3.0
2013-02-23T15:17:42.580Z
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
CC BY-SA 3.0
2013-02-23T15:26:17.133Z
@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
CC BY-SA 3.0
2013-02-23T16:58:27.397Z
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
CC BY-SA 3.0
2013-02-23T21:37:26.540Z
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
CC BY-SA 3.0
2013-02-24T11:53:03.367Z
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
CC BY-SA 3.0
2013-02-24T18:56:08.703Z
Dunno. I just gave you a pointers that that might come in handy.
Dave Clarke
<type-theory><randomized-algorithms><sorting><type-systems><haskell>
Type-and-effect systems, stochasticism and effect squelching: how about quicksort?
Jonas Kölker
# Type-and-effect systems, stochasticism and effect squelching: how about quicksort?

(Asked by: username_0 on 2013-02-23)

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

**Tags:** type-theory, randomized-algorithms, sorting, type-systems, haskell

> **Comments:**
> **username_1**: The state monad can be used to squelch effects, perhaps by combining it with the Random monad transformer to throw some randomness in there.  
> **username_0**: @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)  
> **username_0**: 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...  
> **username_1**: 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.  
> **username_0**: 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...  
> **username_1**: Dunno. I just gave you a pointers that that might come in handy.  

---

## 0 answers

