неділя, 1 вересня 2013 р.

Из значений в типы...

Хаскель поддерживает зависимые типы — это уже давно не для кого не секрет. Конечно в нем это не очень родная возможность, но все же успешные опыты существуют. Но долго мне было непонятно как такое (см. ниже код на Агде) сделать на Хаскеле. Проблема в том, что значения 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