依存型を持つ純粋関数型言語 Idris - Ryusei’s Notes (a.k.a. M59のブログ)

Idris http://idris-lang.org/ は依存型を持つ純粋関数型言語。C言語経由でネイティブコードを生成する他、JavaScriptコードの生成もできるようだ。*1

cabalを使ってインストールする。

cabal update; cabal install idris

ハローワールドのソースコード。IdrisはHaskell風の文法を持っている。型注釈は必要。

module Main

main : IO ()
main = putStrLn "Hello world"

コンパイルして実行してみる。

prog_idris$ idris hello.idr -o hello
prog_idris$ ./hello 
Hello world
prog_idris$ idris hello.idr -o hello.js --target javascript
prog_idris$ node hello.js 
Hello world
prog_idris$

後で色々やってみるかも。

Idris - Example

*1:コンパイルされたコードは人が読めるようなものではないです。