What Algorithms Do People Use for Reinforcement Learning?