Idrisでの関数型プログラミング

注意：これはIdris2入門の原版ですが、現在は非推奨です。 現在のバージョンはIdris2コミュニティで維持されており、こちらにあります。 全ての修正や新しく貢献する際はそちらでお願いします。

中文翻译, 日本語訳

このプロジェクトの目標を手短かに説明するとこうなります。 Idrisプログラミング言語の多少なりとも網羅的な手引きとし、関数型プログラミングの入門者を対象とした入門的な題材をちりばめることです。

内容は幾つかの部にまとまっています。 中核的な言語の特徴についての部は、Idrisでの関数型プログラミングのための手引きです。 各部は幾つかの章からなり、それぞれの章ではIdrisプログラミング言語や中核ライブラリの一側面を踏み込んで扱います。 ほとんどの章は（時に多くの）演習が付録しており、ディレクトリsrc/Solutionsに解法があります。

現時点では、中核的な言語機能の部分もまだ完了しておらず、活発に開発されているところです。 その開発には筆者の生徒の中からも数名挑戦しており、関数型プログラミングを完全に初めたばかりの人もいます。

目次

第1部：中核にある言語の特徴

この部ではIdrisプログラミング言語への導入を地道に一歩ずつ進めることを試みます。 もし関数型プログラミングが初めてであれば、必ず順番にこの部の章にしたがい、また全ての演習を解いてください。

Haskellのような他の純粋関数型プログラミング言語を使ったことがあるなら、 導入的な内容（関数 その1、代数的データ型、インターフェース）に素早く目を通すのでもよいでしょう。 ほとんどは既に馴染みのある事柄でしょうから。

1. 導入
   1. プログラミング言語Idrisについて
   2. REPLを使う
   3. 最初のIdrisプログラム
   4. Idrisの定義の形
   5. 困ったときは
2. 関数 その1
   1. 1つ以上の引数を持つ関数
   2. 関数結合
   3. 高階関数
   4. カリー化
   5. 匿名関数
   6. 演算子
3. 代数的データ型
   1. 列挙型
   2. 直和型
   3. レコード
   4. 汎化データ型
   5. データ定義の別の文法
4. インターフェース
   1. インターフェースの基本
   2. もっとインターフェース
   3. Preludeにあるインターフェース
5. 関数 その2
   1. let束縛と局所定義
   2. 関数引数の真実
   3. 虫食いプログラミング
6. 依存型
   1. 長さ指標付きリスト
   2. Fin: ベクタから安全に指標で引く
   3. コンパイル時計算
7. IO: 副作用のあるプログラミング
   1. 純粋な副作用？
   2. doブロックとその脱糖
   3. ファイルを取り回す
   4. どうIOが実装されているか
8. 関手と仲間達
   1. 関手
   2. アプリカティブ
   3. モナド
   4. 背景とその先へ
9. 再帰と畳み込み
   1. 再帰
   2. 全域性検査についての注意
   3. Foldableインターフェース
10. 作用付き巡回
    1. CSVの表を読む
    2. 状態付きプログラミング
    3. 組み立ての強力さ
11. シグマ型
    1. 依存対
    2. 用例：核酸
    3. 用例：スキーマに基づくCSVファイル
12. 命題の等値性
    1. 型としての等値性
    2. 証明としてのプログラム
    3. Voidへ
    4. 規則を書き換える
13. 前提と証明検索
    1. 前提条件
    2. 値同士の契約
    3. 用例：柔軟なエラー制御
    4. インターフェースの真実
14. 原始型
    1. どのように原始型が実装されているか
    2. 文字列を取り回す
    3. 整数
    4. 精錬後の原始型

第2部：補遺

補遺は身近な話題の参考情報として使えます。 最終的には、Idrisの文法、典型的なエラー文言、モジュールシステム、対話的編集などについての簡潔な参考情報にしようと模索しています。

1. packとIdris2で始めよう
2. Neovimでの対話的編集
3. Idrisのプロジェクトを構築する
4. 数量的型理論を深掘りする

予め必要なもの

現時点でこのプロジェクトは活発に開発中で、Idris 2リポジトリのmainブランチとともに進展し続けています。 GitHubでnightlyにテストされており、packのパッケージコレクションの最新版に対してビルドされています。

この入門を読み進めるにあたってはこちらに記載されているようにpackパッケージ管理を介してIdrisをインストールすることを強くお勧めします。