こんにちは, ねりあです.

この記事は Idris という言語についての記事になります.

僕は別件で依存型に関する記事を書いていたんですが, その途中で
「依存型の話を書いてるのに Idris 触ったことないの〜プークスクスw」
と脳内の自分が煽ってくるので, とりあえず環境構築したので, その話を記事にします.

インストール

まずは install です.
と言っても以下の通り, brew install するだけです.

$ brew update
$ brew install idris

これで, Idris のインストール終了です.
インストールというか環境構築が終了してしまいました.
以下でバージョンが表示されれば完了です.

$ idris -v
1.3.2

プログラムを実行してみる

流石にこれで終わるのは味気ないので, 世界に挨拶ぐらいはしましょう.
以下を作成します.

hello.idr

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

あとは実行するだけです.
コンパイルして実行する方法と REPL から実行する方法の2種類があります.

コンパイルして実行する方法

以下の通り実行すればコンパイルして実行することができます.

$ idris hello.idr -o hello
$ ./hello
Hello World

REPL で実行する方法

idris コマンドで REPL を起動でき, REPL 内でも実行できます.

$ idris
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 1.3.2
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
Idris> :load hello
*hello> :exec main
Hello World

REPL 内では : を付けるとコマンドとして認識してくれます.
REPL を抜けたい場合は :quit で抜けることができます.

まとめ

まあ, 大したことを話していないので, まとめもくそもないのですが,
Idris は依存型について調べているとサンプルコードで大量に見ます.
依存型が何かという話は現在記事を執筆中なので, またの機会に.