こんにちは｜こんばんは。カエルのアイコンで活動しております @kyamaz です。

はじめに

様々なプログラミング言語がありますが、本稿では『Idris』という型駆動開発を促進するために設計されたプログラミング言語を取り上げます。Idris では、型が言語の第一級構成要素です。型を関数に引数として渡すことができ、数値、文字列、リストなどの他の値と同じように関数から返すことができるように設計されています。
Idris には、バージョン１系とバージョン２系があり、バージョン１からバージョン２へ破壊的な仕様変更があり、本稿ではバージョン２系である Idris2 を扱います。

Idris2

Idris2の記述はHaskellに似た記法で、関数の型定義がHaskellではコロン２つ（func :: types）なのに対してIdris2ではコロン１つ（func : types）という違いがありますが、ほぼ同じ記法です。
Idris2の特徴は、依存型を扱える関数型プログラミング言語です。Idris2の型システムはAgdaに、証明はCoqに似ていると言われています。
Haskellでも『実世界を扱う依存型プログラミングのたぶん基本～外界から安全な世界までの道』のエントリで解説のあるように依存型を考慮した実装ができますが、この記事にあるMatrixの例のような課題があります。この課題を解消できる依存型を予め備えているのがIdris2です。型をプログラムの計画として扱い、コンパイラと型チェッカーをアシスタントとして使用して、型を満たすようにプログラムを実装します。そのためプログラムが完全に動作するよう導くことができます。

Idris2のインストール

本稿では、Idris2をmacOSにインストールしてコンパイル環境・実行環境を整える方法を紹介します。Idris2をインストールするには次のような幾つかの方法があります。

Homebrew を使ってインストールする
パッケージ管理『pack』をインストールする
ソースコードからインストールする

これらの３つのインストール方法を紹介します。

Homebrew で『Idris2』をインストール

Homebrewを使える環境であれば、次のとおり簡単にインストールできます。

idris2のインストール

$ brew install idris2

なお、brew install idrisではバージョン１系がインストールされますのでご注意ください。

Idris2のパッケージ管理『pack』をインストール

Idris2には、Haskellのstackやcabalのような、インストーラ兼パッケージマネージャ兼ビルドツールである『pack』というツールがあります。これを次のようにインストールシェルでインストールすることができます。

packのインストール

$ bash -c "$(curl -fsSL https://raw.githubusercontent.com/stefan-hoeck/idris2-pack/main/install.bash)"

ただし、事前にChezSchemeのインストールが必要となります。 brew install chezschemeで事前にインストールしておいてください。

インストールされるデフォルトのフォルダは $HOME/.pack です。
.zprofile（や.bash_profile）にPATH=$HOME/.pack/bin:$PATHを追加してパスが通るようにしてください。

ソースコードからインストール

適当なワークフォルダ（$HOME/work)にソースコードをダウンロードしてビルドします。この場合も事前にChezSchemeのインストールが必要となります。

Idris2のビルド

$ cd $HOME/work
$ git clone https://github.com/idris-lang/Idris2.git
$ cd Idris2
$ make all
$ make install

インストールされるデフォルトのフォルダは $HOME/.idris2 です。
.zprofile（や.bash_profile）にPATH=$HOME/.idris2/bin:$PATHを追加してパスが通るようにしてください。

※前述のpackのインストールでもIdris2がソースコードからビルドされます。

動作を試してみる

が尊敬する κeenさんが、Idris入門の記事をnoteに書かれております。

この中にBMIを計算して判断するプログラムが紹介されております。早速そのプログラムをファイルに書いて実行してみましょう。

Bmi.idr2

bmi : Double -> Double -> Double
bmi weight height = weight / height / height

diagnostic : Double -> Double -> String
diagnostic weight height =
  let index = bmi weight height in
  if index < 18.5
  then "Underweight"
  else if index < 25.0
  then "Normal range"
  else if index < 30.0
  then "Pre-obese"
  else if index < 35.0
  then "Obese class I"
  else if index < 40.0
  then "Obese class II"
  else "Obese class III"

以下のようにして実行するとインタラクティブなプロンプトで実行できるようになります。（体重65.0kg /身長1.70mを例に試します）

% idris2 bmi.idr2
     ____    __     _         ___
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.7.0-1a3df3fb6
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
 /___/\__,_/_/  /_/____/   /____/      Type :? for help

Welcome to Idris 2.  Enjoy yourself!
Main> diagnostic 65.0 1.70
"Normal range"
Main>

うまく動作しているようです。

（投稿後2024/6/30追記）
インタラクティブのコマンドidris2ではシェルのヒストリ機能のような上下キーによる入力支援がされません。Idris2公式のFAQの"How do I get command history in the Idris2 REPL?"に書かれていますが、rlwrapを使うように勧められています。macOSではHomebrewでインストール（brew install wlwrap）して、rlwrap idris2で実行するとコマンドヒストリが使えます。

おわりに

本稿では、Idris2の動作環境を整えるのみでしたが、プログラミングも色々と試してみると楽しそうです。現状ではIdris2の実装に関する情報がそれほど多くないですが、試してみてはいかがでしょうか。

なお、お手元の環境で検証する際に、動作が異なるときには参考になるかもしれませんので、最後に、本稿を記載するために検証したmacの環境を挙げておきます。

本稿の環境

本稿のために使用した環境は以下となります。

macOS: Sonoma 14.5 (chip: Apple M1)
Homebrew 4.3.6
LLVM: Homebrew clang version 12.0.1
XCode: Apple clang version 15.0.0 (clang-1500.3.9.4)
（PATH環境変数により、Homebrew LLVMを先にしてあります）
ChezScheme: chez 10.0.0

ご一読いただきまして有り難うございます。
（●）（●） Happy Hacking!
/""　＿＿""＼

macOSでIdris2のコンパイル環境・実行環境を整える（2024年6月現在）