κeenです。関数型まつり楽しかったですね。関数型という広めのトピックに人が集まって色々な知識が聞けるのがこういう大きなカンファレンスの醍醐味の一つです。
ところがトピックが広いということは様々な講演を聴講するのに必要な前提知識も広範に渡るということでもあります。実際、終了後に必要だった知識のまとめや解説がほしいという声を多数みかけました。

そこで私が分かる範囲で出てきた知識の入門への案内を書いておこうと思います。

ガッと書いたので誤りがありそうですが、気付いたら優しく教えて下さい。

6/17追記: いくつか誤りを訂正・説明の補強、プログラミングテクニックに末尾再帰とFBIPを追加

言語

色々な言語が登場しました

関数型言語

Haskell
ML語族
- OCaml
- SML
- F#
Lisp語族
- Clojure
- Emacs Lisp
Scala
Elixir
Elm

関数型言語は今回の主役ですね。Haskell、ML、Lispあたりが20世紀からの伝統のある関数型言語ですが、最近はScalaやElixirやElmなどの言語も人気です。一昔前はHaskell、ML語族のどれか、Lisp語族のどれか、で3種類の言語をなんとなく理解していれば大体の発表を楽しめると言われていましたが、最近は登場する言語が多様化したのでそうもいかなくったようです。

Lisp語族は登場当時は高階関数やラムダ式があることから関数型言語と言われていましたが、今どきは大抵の言語に入っているのであまり関数型言語感はなくなりましたね。Lispを使っている側もあまり関数型言語とは思っておらず、こういう場からはだんだん離れつつあります。今回もLispの発表は2件、それも1件はタイトルが「Lispは関数型言語(ではない) by うさみけんた」でした。因みにLisp語族にはこれ以外にもCommon LispやSchemeがあり、さらにSchemeは処理系毎に分かれたりします(Racketとか)。

それぞれの言語で調べると入門記事などが出てくると思います。どれか1つだけ入門するならHaskellを選ぶ人が多いようですが、私はOCamlも面白い言語だと思いますよ。関数型言語を学んで副作用、再帰関数、代数的データ型とパターンマッチ、高階関数などのワードに触れておくと楽しめる講演がぐんと増えます。

形式手法関連

形式手法そのものの解説は後回しにします。

Alloy
TLA+
Rocq(旧Coq)
Lean 4

AlloyやTLA+は形式仕様を記述したり検証したりするための言語です。一方でRocqやLeanは定理証明支援系です。

それぞれ入門記事を調べると多少は記事がヒットするかと思いますが、まだ知名度が低くあまり多くはありません。英語で書かれた公式ドキュメントをLLMなどで翻訳しつつ読むことも時には必要です。
AlloyとCoqは書籍も出版されています。

Rocqについては比較的最近Coqから改名したので情報を得るならCoqの方がヒットしやすいでしょう。

その他プログラミング言語

Rust
TypeScript
Ruby
Excel
XSLT
Julia
Swift
Kotlin

これは解説不要でしょう。

数学っぽいやつ

なんかこんな感じの式っぽいのがたくさん書いてあるやつです。

\begin{align} (\to^\prime) \quad & \langle\lambda{}x.v_1|v_2\cdot{}e\rangle & \to \quad & \langle{}v_2|\tilde\mu{}x.\langle{}v_1|e\rangle\rangle \\ (\mu) \quad & \langle\mu\beta.c|e\rangle & \to \quad & c[\beta \leftarrow e] \\ (\tilde\mu ) \quad & \langle{}v|\tilde\mu{}x.c\rangle & \to \quad & c[x \leftarrow v] \end{align}

この他にも分数っぽい記号とかも出てきましたね。あとはラムダ計算とか操作的意味論とか言ってたのもこの類です。

これらはプログラミング言語の理論研究で使われる記法です。ぶっちゃけ知っても実務でに立つものではありませんが、それでも学びたければ大学の教科書が参考になります。

前者二つは名前が似ていますね。さらに加えて著者の下の名前がどちらも淳なのでたまに間違えて買う人がいます。

プログラミング言語の基礎概念はこの中では一番薄く、とっつきやすい本です。

プログラミング言語の基礎理論は今回招待講演をされていた大堀先生の本です。招待講演で触れられていた多相レコードの理論も載っています。

型システム入門(通称TaPL)は今回招待講演をされていた遠藤さんも訳に参加している本です。有名ですがその分挫折した人も多い本です。

どれも大学の教科書なので独習するのは骨が折れます。周りに興味がある人がいれば巻き込んで読書会などするとよいでしょう。

数学

代数学の概念がちらほら登場しましたね。数学者のように研究する訳ではなく概念と名前を使わせてもらってるだけなのでWikipediaの項目をさっと読むだけでよいでしょう。

これらは色々な物事をよく抽象化しているのでプログラミングする際の抽象化としても使えるのです。

また、モナドや双対などの圏論の用語も出ましたね。これはプログラミング言語を研究する上でプログラムと数学的対象を関連づけておいて数式を使ってプログラムの振舞を理解するときに使われる道具です。プログラミング言語の研究者でもない限り知っていてもあまり役立つものではないですが、関係あると言われると気になってしまうのが人の性なのでちょいちょい顔を出しがちです。もし興味があるなら意外と豊富に資料があります。

これ以外にも書籍、Webページ、PDF問わず様々な資料がみつかるでしょう。

ある程度知識がついてピンポイントに出てきた用語が分からなかったらnLabで調べると色々載っています。例えばGraded monadなんかは今回の講演で登場しました。

形式手法

数学的にバグをなくすための手法です。大きく分けても色々手法がありますが、2つ紹介しておきます。

形式仕様記述
定理証明

形式仕様記述

仕様をコンピュータ言語で書くことで仕様を明確にしたり、仕様の性質を明かにする手法です。また、あいまいさのないコンピュータ言語で仕様を書くことで人間同士のミスコミュニケーションを防ぐ効果もあります。実装としては先に出てきたAlloyやTLA+などのツールがあります。

定理証明

圏論のところで「プログラムと数学的対象を関連づけておいて数式を使ってプログラムの振舞を理解する」と書きましたが、定理証明は逆にプログラムを使って数式の証明をする手法です(これ以外のアプローチもありますが)。こうすることで機械的に正しさを確かめられます。

本格的に入門する前に雰囲気だけ知りたいという方は我田引水ですが以前私が書いた記事を読んでみて下さい。

どのような数学的対象と関連づくかはプログラミング言語ごとに違うので、できるだけ面白い数学的対象と関連づくようにした上で数学の証明に便利な記法などを導入したのが定理証明支援系です。先に出てきたRocq(Coq)、Lean、あとはAgdaやIdrisなどが知られています。少し前まではCoqの人気が高かったのですが最近はLeanの勢いがすごいですね。

これらはベースはプログラミング言語なのでプログラムを書けますし、そのプログラムに証明をつけることもできます。テックジャイアンツを中心に採用事例が増えてきてるので徐々に知名度が上がってきてますね。もちろん、巨大資本でなくても個人的に使っても便利なものです。世の中には競技プログラミングをするときに定理証明支援系で正しいことを証明しながら解いている人もいるらしいですよ。

この分野に興味があればProof SummitやTheorem Prooving and Provers Meeting (TPP)などのイベントも覗いてみて下さい。

継続とか

プログラムの「その後の計算」という概念です。値がどの言語にもあるように継続もどの言語にもあるかなり基本的な概念です。この継続を取り出して陽に一級市民として扱えるようにするSchemeの call-with-current-continuation (通称 call/cc)が有名です。実はRubyにも callcc があったりします。

継続は基本的な概念なので色々なものの基礎になっています。その分目にする機会も多いでしょう。

継続の入門は色々あるので自分のレベルや前提知識にあわせた記事を探してみましょう。ヒントとしてはSchemeで一級市民として扱えることからScheme関連の記事が多かったり、継続の研究で有名な浅井健一先生がいらっしゃるので検索ワードに「浅井」とつけるとしっかりした解説PDFがみつかったりします。また、継続勉強会の資料も役に立つかもしれません。

限定継続

call/cc はありったけの継続を捕捉してしまうので少し不便です。そこで捕捉する継続の範囲を区切った(限定した)オペレータが考えだされました。この区切り方とか区切った継続を呼び出したときにどうなるかとかで4種類の演算子に区別されます。

shift/reset
shift0/reset0
control/prompt
control0/prompt0

control0/prompt0 が一番基礎的なオペレータで、実用上便利なのは shift/reset とされています。これら4つと call/cc は互いが互いを実装できるのでどれを使うかは好みの問題です。shift/resetがよく使われるので気になる人はとりあえずshift/resetを理解するのを目指しましょう。

応用例は広く、例外の実装、ファイバーやコルーチンや非同期処理、ネストしたコードの整理など色々なところに使える強力なツールです。

Algebraic Effects

代数的効果、代数的エフェクト、あるいは固有名詞的に単にエフェクトと呼ばれることもあります。モナドと同様に関数型言語で副作用を扱うための仕組みですが、モナドより記述の自由度が高く使いやすいです(主観)。理論的にみつかったあと、ぼちぼち実用的なプログラミング言語に取り入れられはじめてるといった段階です。OCaml 5に入ったというのは今回も話題に出ましたね。

このエフェクトの実装に限定継続が有用な他、APIとしても継続の概念が登場するので継続の話題の中に入れておきました。

入門するにはeffect system勉強会の資料は…あんまり向かないかな。エフェクトを全面的に押し出した言語Kokaに入門するのが一番手っ取り早いと思います。簡潔で分かりやすい(主観)のでモナドで挫折して純粋関数型言語をあきらめたという人もぜひ試してみて下さい。

型

関数型言語には強力な型システムを備えた言語が多くあるので型の話題も多くなります。そこそこの数の人が型システム入門(TaPL)の内容を既知として喋ることが多いです。今回出てきたワードをピックアップしますが、高階多相(Higher-Kinded Polymorphism)や高ランク多相(Higher-Rank Polymorphism)などのワードも頻出です(両者ともTaPLで解説されています)

依存型

依存型(Dependent Types)は型の部分にプログラムを書ける仕組みです。よくあるのは数値を使って「長さ5のリスト」のような制限された型を使うテクニックですかね。
理論的な話はTaPLに載っていますが、とりあえず知りたいだけなら私が昔書いた例が参考になるかもしれません。その他調べると色々解説記事はあると思います。

篩型

篩型(ふるいがた、Refinement Types)は型の部分に式を書いて値を制限できる仕組みです。この説明だけだと依存型との違いが分からないですね。実際依存型と似たようなことができますが、やや表現力が劣ります。
ですが、仕組みが結構違って依存型は専用の言語設計やコンパイラが必要(らしい)なのに対して篩型は既存の言語に後付けできるので既に普及している言語の型を強力にしたいというモチベーションでよく使われます。

そもそも値を制限して何が嬉しいの？というところは今回の講演であったより安全で単純な関数定義 by がくぞが参考になると思います。スライドは以下のツイートからどうぞ

線形型

線形型(せんけいがた、Linear Types)、あるいは線型型は値を一度しか使えない型です。一番分かりやすい説明は「Rustの所有権の親戚」です。概略を理解するにはRustに入門するのが一番早いと思います。

線形型だけなら話は早いのですが、そのままだと不便なので色々な亜種が登場したり、線形型のない言語にどうやって入れるかで方針が違ったりするのでどの言語の機能なのか注意深く聞いておかないといけないのが難しいところです。

線形時相論理

線形時相論理(Linear Temporal Logic)は「いつかAになる」のような時間の概念を表わせる論理です。型じゃないじゃんって言われそうですが、近しい概念なのでここに並べておきます。

並行プログラムの振舞などの記述に便利なので先に出てきた形式仕様記述とかの分野で登場します。

私も詳しくないのでいい入門あったら教えて下さい。

プログラミングテクニック

末尾再帰

末尾再帰は関数を再帰させるときに効率的に実行するためのテクニックです。
詳しく説明している講演がありましたが、逃した人もいると思うので書いておきます。
関数が自身を呼び出すことを再帰呼出といいます。関数の末尾で関数呼び出しをするのを末尾呼出といいます。再帰呼び出しを処理の末尾で行うことを末尾再帰と呼びます。

(* 再帰呼出だが、sumを呼んだあとに+の処理があるので末尾再帰でない *)
let rec sum n = if n == 0 then 0 else n + (sum (n - 1))
(* 実行例
  # sum 10;;
  - : int = 55
*)

(* sum_loopを呼んだあとに何もしないので末尾再帰 *)
let rec sum_loop n acc = if n == 0 then acc else sum_loop (n - 1) (n + acc)
(* 実行例
  # sum_loop 10 0;;
  - : int = 55
*)

全ての再帰呼出が末尾再帰になっている関数を末尾再帰関数といいます。

これだけだとプログラムの字面の問題にみえますね。しかしプログラムの最適化により末尾呼出はスタックを消費しないようにできる(末尾呼出の最適化、Tail Call Optimization、 TCOなどと呼ばれる)ので、より効率的に動作します。特にループを関数で表現する関数型言語ではスタックオーバーフローを防ぐのに必須のテクニックです。言語によっては一般の末尾呼出の最適化はせずに末尾再帰だけを最適化するケースもあります。

ところが sum_loop をみてもらうと分かるように関数を末尾再帰の形に書き換えると引数が増えることがよくあります。これだと元の関数と同じように使えないので、末尾再帰関数を関数内関数として定義して、余計な引数を渡しつつ呼び出すのが常套手段になっています。

(* ユーザが使うのはsum関数 *)
let rec sum n =
  (* sum_loopを関数内関数として定義する *)
  let rec sum_loop n acc = if n == 0 then acc else sum_loop (n - 1) (n + acc) in
  sum_loop n 0
(* 実行例
  # sum 10;;
  - : int = 55
*)

(ところで増えた引数のことは今回の和のように累積する(Accumulate)ので acc といったり補助的(auxiliary)な役割なので aux といったりします。)

このよくあるパターンを綺麗に書ける構文があるとかないとかで盛り上がったりします。

簡単には末尾再帰にできない関数もあり、それは継続渡し形式(Continuation-Passing Style、CPS)に変換して末尾再帰にするテクニックなんかもあります。しかしぱっと理解するのが難しいですし実行効率はあんまりなのでよく分かるCPS変換とか工夫して速くするCPS変換とかで1本講演できます。

DSL

ドメイン特化言語 (Domain Specific Language)とはある領域に特化した言語です。ある問題を解きたいときに直接プログラムを書いて解決するのではなく、一旦その領域を記述できる小さな言語を作っておいて、その言語で問題を解くと変更に強くなるよねって考え方を基に作られます。
外部DSL(使っているプログラミング言語とは別に言語を作る)か、内部DSL(使っているプログラミング言語のAPIとして作る)かに大別されます。特に後者はeDSLと呼ばれます。

名前を知らないだけで普段から使っているという人は多いでしょう。よくあるのが設定ファイルなどでRubyのRakeなんかがパッと思いつきます。

関数型言語ではeDSLを作って問題を解決するのがエレガントなアプローチとされ、こういう事例でこういうeDSLを作りました、という発表がよくあります。

あんまり構えずにeDSL作ったと聞いたら綺麗なAPI群作りましたって意味と捉えておくといいと思います。

幽霊型

幽霊型(Phantom Type)はデータ型に付加的な型を加えることでより詳細に区別するためのテクニックです。

幽霊型を知らない人の方が多いので幽霊型で1本講演ができたりしますが、たまに普通に使われることもあります。知っておきたければ手前味噌ですが昔ブログを書いたので読んでみて下さい。幽霊型を知った | κeenのHappy Hacκing Blog

幽霊型の応用例は以下の記事が詳しいです。
日本一詳しい幽霊型テクニック集

tagless-final

tagless-finalはExpression Problem(後述)を解決するために提案された手法です。Olegさんによって提案されました。調べると世の中に入門記事はありますが、簡潔な説明なら記事内に収まりそうなので解説してみます。ベースはこのPDFです

モチベーションとしては、このようなデータ型を書いて

data Exp = Lit Int
         | Neg Exp
         | Add Exp Exp

このような実装を与えたとき、

eval :: Exp -> Int
eval (Lit n) = n
eval (Neg e) = - eval e
eval (Add e1 e2) = eval e1 + eval e2

view:: Exp → String
view (Lit n) = show n
view (Neg e) = "(-" ++ view e ++ ")"
view (Add e1 e2) = "(" ++ view e1 ++ " + " ++ view e2 ++ ")"

-- 使用例
ti1 = Add (Lit 8) (Neg (Add (Lit 1) (Lit 2)))

あとからデータ型のヴァリアントを追加するのが難しいよね(Expression Problem)というのがあり、それを解決する手法です。

tagless-finalで解決するにはこのようにデータ型ではなく型クラスで表現します。

class ExpSYM repr where
  lit :: Int → repr
  neg :: repr → repr
  add :: repr → repr → repr

そしてこのように実装を与えます。

instance ExpSYM Int where
  lit n = n
  neg e = - e
  add e1 e2 = e1 + e2

instance ExpSYM String where
  lit n = show n
  neg e = "(-" ++ e ++ ")"
  add e1 e2 = "(" ++ e1 ++ " + " ++ e2 ++ ")"

-- 使用例
tf1 = add (lit 8) (neg (add (lit 1) (lit 2)))

この状態で新しいヴァリアント Mul を与えることを考えてみましょう。元の data Exp を使った実装だと Exp の定義や eval や view の定義を変更する必要がありますが、この手法だと定義を変更せずに追加できます。具体的にはこうです。

class MulSYM repr where
  mul :: repr → repr → repr

instance MulSYM Int where
  mul e1 e2 = e1 * e2
instance MulSYM String where
  mul e1 e2 = "(" ++ e1 ++ " * " ++ e2 ++ ")"

-- 使用例
tfm1 = add (lit 7) (neg (mul (lit 1) (lit 2)))

FBIP

Functional But In Place (FBIP)はPerceusというガベージコレクタを使ってできるプログラミングスタイルです。PerceusはKokaやLeanなどのMicrosoft Research発の言語に入っています。
パターンマッチして即同じ大きさのデータを作り直す系の操作を、他でデータが使われていない場合はデータを破棄して新しく作り直すのではなく、その場で書き換えるように最適化してくれます。

コード例を出します。Perceus: Garbage Free Reference Counting with Reuseに載っている例です(中身を読みたい人はタイトルで検索すると著者が公開しているPDFが出ます)。

題材は普通の二分木です。

type tree {
  Tip
  Bin(left: tree, value : int, right: tree )
}

この木に対してmap処理を書こうと思うとこうなりますね？

fun tmap( t : tree, f : int -> int ) : tree {
  match(t) {
    Bin(l,x,r) -> Bin( tmap(l,f), f(x), tmap(r,f) )
    Tip -> Tip
  }
}

ですがこれは末尾再帰になってませんし、受け取った木を破棄して新しい木を作り直しているので非効率です。

これをFBIPな処理に置き換えましょう。
まずこの木を渡り歩く visitor を作ります。 visitor の中身は本筋とは関係ないので難しく考えないで下さい。1つ重要な点として visitor と tree は同じサイズを持ちます。

type visitor {
  Done
  BinR(right:tree, value : int, visit : visitor )
  BinL(left:tree, value : int, visit : visitor )
}
type direction { Up; Down }

これを使って tmap を書き換ます。

fun tmap(f : int -> int, t : tree, visit : visitor, d : direction ) : tree {
  match(d) {
    Down -> match(t) {       // going down a left spine
      Bin(l,x,r) -> tmap(f,l,BinR(r,x,visit),Down)
      Tip -> tmap(f,Tip,visit,Up)
    }
    Up -> match(visit) { // go up through the visitor
      Done -> t
      BinR(r,x,v) -> tmap(f,r,BinL(t,f(x),v),Down)
      BinL(l,x,v) -> tmap(f,Bin(l,x,t),v,Up)
    }
  }
}

すると末尾再帰になりましたね。もう1つ重要な点として、 Bin にマッチして即座に(関数の再帰処理をする前に) BinR を、 BinR にマッチして BinL を、 BinL にマッチして Bin を作っています。これらは同じサイズのデータなので、 tree が他で使われていない場合Perceusが空気を読んでマッチしたデータを上書きして新しいデータにしてくれます。

こうして副作用がないコードを書きつつ効率的な実行ができるというわけです。

おわりに

資料を見返したり次回参加するときの参考になれば。

他にもここ分からなかったとかこの資料分かりやすいよとか俺にこれを解説させろとかあればコメントに書いて下さい。

Discussion