The "random" algorithm in a media player is not supposed to be "random pick with replacement". It is meant to be shuffle, and that's indeed what it is called instead of "random". A shuffle algorithm that plays the same song twice is indeed a broken shuffle algorithm (except if, of course, the playlist actually contains two instances of the same song).