Хотите угореть по системам типов? Посмотрите на реализацию сортировки на зависимых типах в Idris.
https://github.com/stepancheg/idris-sort/

#types