[qsort]

You are being needlessly antagonistic. On HN of all places we should know that research in type theory isn't purely academic navel gazing.