　これは筆者（κeen）がIdris Advent Calendar 2020に投稿した内容を土台とし、一冊の本になるように増補改訂を行なったものです。

　本書では依存型のあるHaskellことIdrisについて紹介します。Idrisは純粋関数型言語であり構文もHaskellに似ていますが、大きな特徴として依存型があることが挙げられます。依存型があるとリストの長さを指定したり整数同士の割り算でゼロ除算が起きないことを保証したり、究極的には数学の証明をしたりもできます。また、依存型以外にもインタラクティブな開発環境を使った型駆動開発であったりElaborator Reflactionによるメタプログラミングだったりと注目に値する言語機能も揃っています。
　総じてIdrisは非常に尖った言語です。作者がプログラミング言語理論の研究者ということもあり、かなり攻めた言語機能が入っています。依存型を搭載したプログラミング言語はほとんどみかけませんし、GADTや暗黙のパラメータなど使い慣れると手放せなくなるような機能も揃っています。まだ若いのもあって明日仕事で使うかもというような言語ではないですが、その分月並な言語にはない新しい体験をさせてくれます。
　本書は自在に使えるプログラミング言語が1つはある人を対象に、Idrisの基本や関数型プログラミング、Idrisの際立った機能などを紹介していきます。プログラミング言語の入門には「言葉で説明されても手を動かしながらじゃないと分からない」という人と「説明のない機能を使われると無理」という人がいます。両者の間をとって説明が多めの部分と手を動かす部分をほどほどに織り交ぜながら徐々にIdrisを深堀していく構成になっています。一緒にIdrisの世界を探訪し、刺激を受けてみませんか？面白そうと思った方は是非キーボードを手に取ってIdrisに入門して下さい。


プログラング言語Idrisに入門させたい（v0.9）

Idrisってどんな言語？

Idrisのインストール

基本文法

BMIを求める

型とデータ型

インタフェース

List、Maybe、Eitherに親しむ

REPLを使いこなす

ファンクタやモナドなどなど

標準ライブラリざっと見

競技プログラミングに挑戦

モナド色々

モジュールとプレリュード、標準ライブラリ

ビットマップ画像の書き出し

名前つきパラメータとGADT

型駆動開発

パッケージとipkg

Idrisdocの使い方

テストとCI

糖衣構文とオーバーロード、あとユーザ定義構文

[WIP] Forth処理系を作る

with構文と依存型、View

依存型を使った定理証明入門

文芸的Idris

依存型で正しいAVL木を定義する

CodegenとFFI

Elaboratorリフレクションでメタプログラミング

zenn.dev

入門

プログラミング言語

関数型

idris

κeen