бля прикол

% cat << EOF > hello.idr
heredoc> main : IO ()
heredoc> main = putStrLn "Hello world"
heredoc> EOF

% idris hello.idr
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 0.9.11.2
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help                

Type checking ./hello.idr
*hello> :compile hello.native
*hello> :js hello.js
*hello> 
Bye bye

% ./hello.native 
Hello world

% ls -l hello*
-rwxrwxr-x 1 ulidtko ulidtko 110K чер 19 02:15 hello*
-rw-rw-r-- 1 ulidtko ulidtko  240 чер 19 02:17 hello.ibc
-rw-rw-r-- 1 ulidtko ulidtko   43 чер 19 02:17 hello.idr
-rw-rw-r-- 1 ulidtko ulidtko  36K чер 19 02:18 hello.js
-rwxrwxr-x 1 ulidtko ulidtko 110K чер 19 02:18 hello.native*

110K
36K

-- на самом деле будущее.