2022-12-09

TIL: OCamlで再帰とlet多相

OCaml

これは相互再帰ではないですが、
let main = id(3);
let id(n) = n;
のようなプログラムの時に、main: Int -> Int, id: a -> aと型推論したいのですが、現在(単相型推論)の場合構文解析時にトップレベルで定義された変数名を記録しておいて、型推論時に予め型環境に上記変数名とフレッシュな型変数続き
— taka2 (@Jj1Fxh) December 8, 2022

こちらの話が大変興味深かったのでOCamlでどうなっているか試した。

結論からいうと、順序関係なく単相化されてしまう：

utop # let rec id x = x
and main () = id 3;;
val id : int -> int = <fun>
val main : unit -> int = <fun>

考えてみたら相互再帰じゃなくても

utop # let rec f b x =
  if b then x else (ignore (f true 5); x);;
val f : bool -> int -> int = <fun>

のように単相化されてしまう。

明示的に全称型な型注釈をつければ大丈夫：

utop # let rec f : 'a. bool -> 'a -> 'a = fun b x ->
  if b then x else (ignore (f true 5); x);;
val f : bool -> 'a -> 'a = <fun>

ただしOCamlの場合はHaskellと違って相互再帰な可能性のある範囲が非常に狭い（let rec ... and ... and ...と指定された範囲のみ）のでこの挙動がlet多相化の邪魔をする可能性はそこまで高くない。Haskellだとスコープ全体で再帰の可能性があるので強連結成分を算出してそれらの依存関係を出して、その順番で型推論していく必要などが生じるのだろうか。

と思って調べたらそういう話がredditで出ていた

www.reddit.com

そして今ふと思い出したのだけどcamlspotter's blogでもこの話に触れられていた：

camlspotter.hatenablog.com

「SCC を計算すればいいのにサボっている」は間違い

これは、値の使用グラフを作ってその SCC (Strongly Connected Component) を計算すれば let/let rec の区別は付くはずなので、let/let rec の区別は必要ない。必要なのは型推論器の実装に手を抜いているから、という意見だ。

Haskell ユーザーはついこの批判をしてしまうように見受けられる。(実際私もこの主張を日本語であれ英語であれ何度か見ている。) なぜなら Haskell では実際に SCC を計算する事で let束縛の入れ子をフラットにしたまま多相的なプログラムを書くことが出来るからだ。

OCamlはサボってるわけではないが、自作言語ではlet rec相応のものを入れて遠慮なくサボりたい所存。

2022-12-01

Lispを実装したくなったら読んでほしい本６選

言語処理系 Lisp

言語実装 Advent Calendar 2022の１日目の記事として書いた。

Lisp Advent Calendar 2022でも枠が空いていたのでダブル投稿。

プログラミング言語を実装してみたい！と思ったらまずは簡単なLisp インタプリタから始めるというのは一つの王道だと思う。

複雑な構文解析は要らず最低限の再帰下降法パーサで手に入る構文木を、そのまま再帰的な関数で実行していくtree walking評価器。メモリ確保もヒープにそのまま置いていって、メモリ解放は実装言語のGCに任せるなりプログラムの終了時までやらなかったり。そんなインタプリタを作る経験から得られるものは非常に大きく、どんなプログラマでも一回は試してみてもいいのではないか？と思っている。（個人的な感想です）

そんな簡易Lispを実装してみて沼にハマってしまい、より精緻な言語処理系を作りたいと思ったとする。その時点で：

C言語のコンパイラでセルフコンパイルを目指す
ML系言語で型システムも加えた言語処理系を作る

などを目標に掲げて邁進することも非常に面白いと思う。

しかし「せっかく簡単なインタプリタを作ったのだから、ここからさらにいいLisp処理系を作ろう」と考えるのも自然な流れだろう。構文解析や型システムに手間取られずにいろんな言語機能の実装、インタプリタのバイトコード化、コンパイラの作成、GCなどのランタイムといったトピックを試したいなら尚更だ。

本記事ではそんな人に役に立つと思われる以下の書籍を紹介する：

Structure and Interpretation of Computer Programs
Anatomy of LISP
Lisp in Small Pieces
Lisp System Implementation
Functional Programming Application and Implementation
Topics in Advanced Language Implementation

（ただし英語＆絶版のものもいくつかあるので注意）

Structure and Interpretation of Computer Programs

www.amazon.com

言わずと知れた魔術師本。MITのプログラミング入門の教科書として使われていたことでも有名。Lisp方言のSchemeを使って書かれたこの本では、最初の方ではプログラミング言語の基本機能について（かなりの駆け足で）語っているのだが、最後の2章ではSchemeを使ってSchemeのサブセットの処理系を書く話になる。本当にこの本でプログラミング入門した人がいるのか、いつも気になっている。

第4章ではMetacircular Evaluatorを作る。これは何やら難しそうな名前だが、基本的にSchemeでScheme インタプリタを実装するというだけの話だ。この章ではさらに静的解析を行なうことで実行前に部分的に評価できるところはやってしまうといったインタプリタの効率化や、遅延評価・非決定的な演算などのインタプリタ拡張を行なっている。

第5章ではまずSchemeでレジスタマシンのシミュレータを書き、第4章と同じSchemeのサブセットをそのレジスタマシンで実行できるように、まずはそのレジスタマシン上で動くインタプリタを作り、そしてその後そのレジスタマシン向けのコンパイラを書く。Lispのデータをどうメモリで表現するか、どのようにガベージコレクションを行うか、なども見ていく。

Anatomy of LISP

www.amazon.com

今回のおすすめ本では一番古く（1978年）残念ながら絶版。どうにかして読む価値はあると思う。

本の前半はLispの解説で、なんとS式ではなくM式で話が進むので時代を感じる。後半では満を持して今まで解説してきたLispをどのように実行するかという話になる。そしてそれは「Lisp Machineという抽象機械上での実行」に絞られており、例えばSICPで出てくるようなインタプリタの話はない。

この抽象機械がどのようなメモリレイアウトやレジスタを持っていて、ガベージコレクタはどのようなアルゴリズムで、この抽象機械のマシン語にコンパイルするためのコードはこれこれ、さらにそれを最適化するための手法、とどんどんこの抽象機械を対象としたLisp処理系を深化させていく。この一点集中型の話がこの本の特色でかなり勉強になる。

Lisp in Small Pieces

www.amazon.com

Lisp実装についての本では一番有名だと思われる本。原著はフランス語で書かれていて、英訳されたものが頭文字がLiSPになるこの題名を付けられている。

章ごとに別のLisp インタプリタ・コンパイラが書かれていて、実にさまざまなトピックについてどう言語処理系を（Lispで）書くかがこれでもかと紹介されている。

SICPよろしく簡単なmetacircular evaluatorからはじめて、Lisp-1とLisp-2の比較をしたと思ったら、継続のあるインタプリタの実装、さらにそのような複雑なソース言語を実行できるラムダ計算的なdenotationalインタプリタなどを書いていった上で、効率化のための部分的コンパイル、バイトコードへのコンパイル、実行時に言語のさまざまな部分を参照・変更できるreflectionやマクロシステム、LispコードのC言語へのトランスパイル、そして最後にはオブジェクトシステムの実装。この一冊でLispの諸機能の実装方法についてはとりあえず包括的に触れられるぐらいの幅を持っている。また継続についてはMLコミュニティなどでもこの本の内容を参考にしている話が出たりするのでLispに限らず言語実装全般において役に立つ。

一つ難をあげるとすれば、翻訳されたものだからか何となく読みにくく感じてしまう点。書いてあるトピックは文句なしに面白いのだが・・・。

Lisp System Implementation

www.t3x.org

LISP9というオレオレLisp処理系の解説書。作者のNils M HolmはR6RSのAcknowledgementsにも名前を連ねている。（が本人はR4RSが好きでR6RSは嫌いらしい）

6000行弱のC言語による処理系のコードをかなり詳しく解説している。処理系としてはバイトコード・コンパイラと抽象機械の組み合わせ。扱っているトピックについてウェブサイトを引用すると：

LISP data objects, syntax analysis, closure conversion, lambda lifting, operational semantics, bytecode generation, bytecode interpretation, primitive functions, bootstrapping LISP code, macro expansion, lexical and dynamic binding, tail call elimination, garbage collection, non-local exits, the read-eval-print loop (REPL), reading and printing LISP objects, input and output ports, error handling, heap image files, etc ...

と多岐にわたっている。文字列の処理などある程度実用に耐える処理系としての機能をそろえているようで、コードリーディング・写経などに良さそう。個人的には近いうちにZigの勉強がてら移植してみたいと考えている。

Functional Programming Application and Implementation

www.amazon.com

Lispkit Lispという純粋関数型な（副作用がない）Lispの言語機能と処理系の解説。この本の最大の特徴はLispのコンパイル先の抽象機械がPeter LandinのSECDマシンだということ。SECD抽象機械とそのマシン語をターゲットにするコンパイラの実装を学ぶには多分最良の資料だと思われる。

ちなみにこの本を元ネタとして記事を何本か書いた：

zehnpaard.hatenablog.com

またSECD機械の非決定性や遅延評価への拡張などの話題もあって楽しい。

ただしSECDがLispのための効率的な処理系になるかというといろいろと疑義が出ている。実際の処理系で使う抽象機械としてはFelleisenのCESKやLeroyのZincの方がおすすめかもしれない。

Topics in Advanced Language Implementation

www.amazon.com

１５人のプログラミング言語実装の専門家によるアンソロジー。かなりLispの話題が多い。Lisp関連の章題を抜き出してみると：

Data-Flow Analysis and Type Recovery in Scheme
Design Considerations for CMU Common Lisp
Compilation Issues in the Screme Implementation for the 88000
The Implementation of Oaklisp
An Experimental Implementation of Connection Machine Lisp
A Simple System for Object Storage in Common Lisp

というものがある。各章は短めとはいえ実装者による生の経験談なので「実用的なLispを実装するためにどのようなデザイン上の選択肢があってどのような意思決定をしたのか」という話が豊富。メモリ、GC、並列化、オブジェクト指向などの話題もカバーされていてLisp in Small Piecesとはまた違う形で非常に幅広いトピックを漁れる。

まとめ

見直してみるとLisp実装本の豊富さに驚く。方言があるので単一言語ではないとはいえ、例えば「ML系言語の実装本」だとここまで多くはならないだろう（論文はたくさんあるが）。やはり言語実装者の心の琴線に触れる何かがあるのだろうか。

何はともあれ、この記事では

入門的なStructure and Interpretation of Computer Programs
個別の実装について詳しくみていくAnatomy of LISP、Lisp System Implementation, Functional Programming Application and Implementation
Lisp実装におけるさまざまなトピックをみていくLisp in Small Pieces、Topics in Advanced Language Implementation

と趣の違う本を6冊紹介してみた。皆様がLisp実装沼にハマる一因となれば幸いである。

2022-11-29

TIL：源氏二十一流

TodayILearned

今年の大河で出てきた源仲章が源姓なのに明らかに公家＆いわゆる源平合戦の源氏とは別な描写だった。

武家ではない公家な源氏というのは百人一首に選ばれた歌人として源融、源兼昌がいるし、さらにフィクションでは源氏物語の光源氏もいるわけだが、どういう理屈なのかよくわかっていなかった。

そもそも源氏というのは親王が臣籍降下した時に与えられる賜姓で、嵯峨天皇の親王たちが降下した814年が最初、正親町天皇の孫忠幸王が1663年に降下したのが最後。実に800年以上の間、天皇家から枝分かれする形で多数の源氏が生まれている。その数を２１とし源氏二十一流とも称される。

ja.wikipedia.org

ただしこの２１に含まれない臣籍降下の例もあるらしいのと、さらに例えば清和源氏から河内源氏が枝分かれするなど、何々源氏という分類がすべてこの２１に入るわけではない。

源融は嵯峨源氏、源兼昌や源仲章は宇多源氏。源頼朝以降の武家の棟梁は清和源氏の流れを汲む河内源氏。光源氏はまさに自身が臣籍降下して賜姓されたという設定。

「源氏長者」というタイトルはこれらすべての源氏の頂点という意味で、長らく村上源氏から輩出されていたのを室町時代から清和源氏の足利も（たまに）なることもあり、徳川幕府成立後は徳川の将軍が必ず源氏長者になったとのこと。

ちなみに源平藤橘では平氏も臣籍降下の折に賜姓されるもので、桓武、仁明、文徳、光孝の四流ある。藤原氏は中臣鎌足の子孫。橘氏も賜姓ではあるがすべて葛城王の子孫。

2022-11-28

TIL：OCamlのバリアントは比較できる

TodayILearned

wamlのコードを読んでいて

let rec enforce inf (p : pred) = function
...
| Bool | Byte | Text when p <= Eq -> ()

のようなコードに行き当たった。predというのは

type pred = Any | Eq | Ord | Num

のように定義されている。つまり普通のバリアントだ。

数年OCamlを使ってきてバリアントが自動的に比較できることを初めて知った。かなりびっくりした。

type t =
  A of int
| B of string
| C of float
| D of int * string * float

で試すと：

utop # A 0 < C 0.1;;
- : bool = true

utop # A 0 < A 1;;
- : bool = true

utop # A 1 < A 1;;
- : bool = false

utop # D(0,"",0.1) < D(0,"",0.2);;
- : bool = true

utop # D(0,"a",0.1) < D(0,"",0.2);;
- : bool = false

utop # D(0,"a",0.1) < D(1,"",0.2);;
- : bool = true

まあ直感的な結果になる。lexicographicalというか。

ドキュメントやReal World OCamlみても言及なさそうなのだが・・・。時々便利そうな、でも実際使いたいかは少し微妙な機能な気がする。

2022-11-27

wamlのコードを読んでる

OCaml 言語処理系

Andreas RossbergがwebassemblyのGC proposalを試すために作ったミニML言語waml。以下の記事で紹介した：

zehnpaard.hatenablog.com

それからもちょこちょこと眺めていたのだが、

考えれば考えるほどwamlは(wasmとは関係なく)すごいな。正格評価なラムダ計算ベースのコア言語、代数的データ型、パターンマッチ、型推論、モジュールやファンクタとまさにML言語の本質っぽいところがつまったミニ言語だ
— zehnpaard (@zehnpaard) November 26, 2022

と、見れば見るほどちゃんと勉強したいと考えるようになった。というわけでコードリーディング中。

現状ではwasm自体はそこまで興味があるわけではなく、どちらかというとASTなどの内部表現と型推論まわりをどう実装しているのかが一番知りたいポイントなのでそこら辺を重点的に（写経も含めて）読んでいる。

コードはここ：

github.com

webassemblyのGCレポジトリのwamlブランチのディレクトリの一つとして存在している。サブディレクトリとして

js - 生成されたwasmを実行するための非常に簡単なJavaScriptコード
src - 言語処理系の中身。OCamlで書かれている
test - wamlの言語機能のテスト。ほぼすべてwamlそのもので書かれている

がある。wamlの言語機能がどのように使われるのかを知るならtest、実装の内容を知りたいならsrcを見るべき。（まあここら辺は普通だ）

srcの内容としては

字句・構文解析関係

lexer
parse
parser

各種内部表現と意味解析

env
prelude
scc
source
syntax
type
typing

wasm関係なしに実行するインタプリタ

eval
value

wasmへのコンパイル関係

compile
emit
intrinsics
lower
link

wamlコードをコンパイル・実行する

main
run
runtime

他諸々

arrange
flags

のように分類できると思う（かなり大まかかつ私見のみな分類であることに注意）。

とりあえず「各種内部表現と意味解析」の部分を現在読みはじめたところ。

2022-11-26

再帰型の実装に関して悩んでいること２ equi-recursive対iso-recursive

OCaml 型理論言語処理系

TaPLを読むと再帰型の理論と実装について、equi-recursiveとiso-recursiveという二つの流儀があると書いてある。

equi-とiso-については以下の記事でも少し触れた：

zehnpaard.hatenablog.com

しかし実際どういう違いなのかをメモった上でどちらにするのかを決めていきたい。

前回に続いて

type intlist = Nil | Cons of int * intlist

という再帰型を考える。これを「環境なしで」表そうと思うと内部的に不動点コンビネータを使っていると見做せる「μ」を利用してこう書ける：

type intlist = μt.Nil | Cons of int * t

さて、ここでintlistに対するパターンマッチについて考える：

let rec sum xs = match xs with
| Nil -> 0
| Cons(x, xs') -> x + sum xs'

この場合xsの型は何か。当然intlistつまりμt.Nil | Cons of int * tであるのだが、同時にmatch xs with | Nil -> 0 | Cons(x, xs') -> x + sum xs'の部分を見ると

Nilというタグを持つ
Consというタグを持ち、その保有する型はintと「sumの引数の型」すなわちμt.Nil | Cons of int * t

というバリアントになる。つまりNil | Cons of int * (μt.Nil | Cons of int * t)だ。

この型はμt.Nil | Cons of int * tのimplicitなFixを一回展開している形で、つまり(λt.Nil | Cons of int * t) (μt.Nil | Cons of int * t)の結果だ。

さてこの展開した形であるNil | Cons of int * (μt.Nil | Cons of int * t)と元のμt.Nil | Cons of int * tがどのような関係にあるか、というのがequi-recursiveとiso-recursiveの観点の違いだ。

equi-recursiveな立場をとるとこの二つの型はまったく同一のものとなる。

type intlist = Nil | Cons of int * intlist

という定義からすれば、右辺のintlistを一回展開してNil | Cons of int * (Nil | Cons of int * intlist)にしても同一性が保たれる、というのは納得できる理屈である。ということは型検査や単一化などの処理で再帰型の扱いは特殊化して、このような形の違う型が同一だと判定したり単一化できたりしないといけない。

それに対してiso-recursiveな立場だとこれら二つの型は同型ではあるが別物と考えられる。そのままでは同一と判定したり単一化したりできない。

うまく単一化させるためにはFoldやUnfoldが正しいところに挟まれていないといけない。これはかなりめんどくさそうではあるが、実際にはプログラマが手動でFoldやUnfoldを書く必要はなくパースから型検査の間のどこかでFold/Unfoldを自動で挿入するステップがあればいい。コンストラクタの適用時に自動的にFoldが追加され、パターンマッチなどで代数的データ型が分解されるときに自動的にUnfoldが追加されるようになる。

例えば

Cons(0, xs)

という式はそのままだと0がint、xsがμt.Nil | Cons of int * tなのでNil | Cons of int * (μt.Nil | Cons of int * t)な型となる。しかしこの式をAST化する時に自動的にFoldを入れる：

EFold(ETag("Cons", [EInt 0; EVar "xs"]))

（実際にはEFoldにはintlistの型定義も入るのだがややこしいので割愛）

逆にパターンマッチの

let rec sum xs = match xs with
| Nil -> 0
| Cons(x, xs') -> x + sum xs'

でも、match xs with ...のxsの部分の周りにUnfoldがつくことでその式の型がNil | Cons of int * (μt.Nil | Cons of int * t)になる。これでパターンマッチの各ケースに直接対応する形になる。

なので「 Iso-recursiveだとFold/Unfoldを明示的にプログラマが書く必要が生じて煩雑」ということはない。

ただしFold/Unfoldがコンストラクタやパターンマッチによって自動的に挿入される都合上、再帰型を導入するためにはコンストラクタを導入するバリアントを使う必要がある。ただのタプルを使った再帰型、例えば

type t = (int * t)

といった型は定義できない。

OCamlやHaskellなどは基本的にIso-recursiveな再帰型が実装されている。上記の制限が実際のプログラムで大きな問題になることはなさそうで、その上で理論・実装の両面からIso-recursiveな方がEqui-recursiveより単純なようだ。

というわけで私の実装もIso-recursiveでやっていきたい。

2022-11-24

再帰型の実装に関して悩んでいること１　再帰する型変数の表現

OCaml 型理論言語処理系

型システムにどうやって再帰型を追加するかで悩んで手が止まっている。何に悩んでいるのかを書き出して整理していきたい。

今回は「現在、型そのものをtyというバリアント型で表現しているが、その枠組みで再帰型をどう表現するか」について。

そもそも再帰型はOCamlでいうところの

type intlist = Nil | Cons of int * intlist

のような型のことで、左辺で定義されているintlistという型が右辺の定義にも出てくるのがポイント。

ただ、この形だと「型の定義」として独立しておらず、「型が名前付きで存在している環境」とセットでようやくNil | Cons of int * intlistの部分が解釈できる。

再帰関数の場合は

let rec length xs = match xs with Nil -> 0 | Cons(_,xs) -> 1 + length xs

のような関数を

let length = fix (λf.λxs.match xs with Nil -> 0 | Cons(_,xs) -> 1 + f xs)

のようにfixを使って環境に依存することなく再帰的に定義する表記がある。

型レベルでも似たようなやり方があって

type intlist = Nil | Cons of int * intlist

が

type intlist = μt.Nil | Cons of int * t

のように表現できる。μtでtという「再帰的な型変数」を導入してCons of int * tで使っていて、この定義は左辺に出てくる型の名前に依存しない。

じゃあμt.Nil | Cons of int * tをどうやってバリアントとして表現するか。

現在、型を表すバリアントは以下のようになっている：

type ty =
| TVar of tvar ref
...
| TTuple of ty list
...
| TVariant of (string * ty) list
...
and tvar =
| Unbound of int * int
| Link of ty
| Generic of int

一つの素直な考え方としては

type ty =
...
| TRec of string * ty
...
and tvar =
...
| Rec of string

のような形にしてμt.Nil | Cons of int * tは

TRec('t', TVariant [("Nil", TUnit); ("Cons", TTuple [TInt; TVar{contents=Rec "t"}])])

と表現するのも一法。かなり直訳になっている。

しかし∀x.x -> xのような型を

TArrow(TVar{contents=Generic 0}, TVar{contents=Generic 0})

と表現するのと整合性が取りづらい。こちらに寄せるなら

type ty =
...
and tvar =
...
| Rec of int

とTRecは消してμt.Nil | Cons of int * tは

TVariant [("Nil", TUnit); ("Cons", TTuple [TInt; TVar{contents=Rec 0}])]

にしてしまうのが良さそう。あるいは相互再帰のことも考えると

type ty =
...
| TRec of ty list
| TRecNth of ty * int
and tvar =
...
| Rec of int

で

TRec [TVariant [("Nil", TUnit); ("Cons", TTuple [TInt; TVar{contents=Rec 0}])]]

という手もありそう。TVar{contents=Rec 0}の中の数はTRec [...]内での添字を表している。

相互再帰的な型としてはなんだか変な例だが

type t = Tup of s * int * s
and s = Leaf of int | Branch of t

について考えてみる（変というのはtype t = Leaf of int | Branch of t * int * tで事足りるため）。

再帰全体の型は：

TRec
  [ TVariant [("Tup", TTuple [TVar{contents=Rec 1}; TInt; TVar{contents=Rec 1}])]
  ; TVariant [("Leaf", TInt); ("Branch", TVar{contents=Rec 0})]
  ]

そして個別のtとs型はそれぞれ：

TRecNth(
  TRec
    [ TVariant [("Tup", TTuple [TVar{contents=Rec 1}; TInt; TVar{contents=Rec 1}])]
    ; TVariant [("Leaf", TInt); ("Branch", TVar{contents=Rec 0})]
    ],
  0)

と

TRecNth(
  TRec
    [ TVariant [("Tup", TTuple [TVar{contents=Rec 1}; TInt; TVar{contents=Rec 1}])]
    ; TVariant [("Leaf", TInt); ("Branch", TVar{contents=Rec 0})]
    ],
  1)

となる。大変冗長だが相互再帰まで表現できるので、この方法で実装していこうと思う。何が問題が生じて変更するかもしれないが・・・

Arantium Maestum

プログラミング、囲碁、読書の話題

TIL: OCamlで再帰とlet多相

Lispを実装したくなったら読んでほしい本６選

Structure and Interpretation of Computer Programs

Anatomy of LISP

Lisp in Small Pieces

Lisp System Implementation

Functional Programming Application and Implementation

Topics in Advanced Language Implementation

まとめ

TIL：源氏二十一流

TIL：OCamlのバリアントは比較できる

wamlのコードを読んでる

字句・構文解析関係

各種内部表現と意味解析

wasm関係なしに実行するインタプリタ

wasmへのコンパイル関係

wamlコードをコンパイル・実行する

他諸々

再帰型の実装に関して悩んでいること２ equi-recursive対iso-recursive

再帰型の実装に関して悩んでいること１　再帰する型変数の表現