README.md

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

中文翻译, 日本語訳

この企画の目標を手短かに説明すると、 関数型プログラミングの入門者を対称とした導入例をちりばめつつ、 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のプロジェクトを構築する

予め必要なもの

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

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