Хаскель поддерживает зависимые типы — это уже давно не для кого не секрет. Конечно в нем это не очень родная возможность, но все же успешные опыты существуют. Но долго мне было непонятно как такое (см. ниже код на Агде) сделать на Хаскеле. Проблема в том, что значения n и m — это (внимание) значения, а они присутствуют в типе. В Агде так можно, но в Хаскеле типы и значения строго разделены.
main : IO Unit main = getContents >>= λ stdin → let (n , m) = readℕ×ℕ stdin proof : n ≤ m ⊎ n > m proof = n ≤? m in putStrLn $ show proof