先の記事の通り、10月にシンガポールに行った。海外に行くのは初めてだったので、準備したことを記録しておく。
投稿者「mod_poppo」のアーカイブ
ML Family WorkshopでLunarMLについて発表した
海外デビュー
特定の技術について関心を持った人が集まって交流する会が開かれることがあります。関数型言語で言うと、今年の6月に「関数型まつり」という国内イベントが開かれました。もっとStandard MLにフォーカスした集まり、あるいは、国際的な集まりとなると、ML Family Workshopがあります。
ML Family Workshopは、関数型プログラミングに関する国際会議であるICFP (International Conference on Functional Programming) に付属して開催されるワークショップで、その名の通りStandard MLに限らず、ML系と呼ばれるプログラミング言語群(OCaml, F#等)も対象としています。きっちりした査読等はなく、比較的ゆるい感じのようです。
ICFPは今回はSPLASH (International Conference on Systems, Programming, Languages and Applications: Software for Humanity) という会議と合同で開催され、全体では1週間ほどあります。ML Family Workshopは10月16日の1日の開催で、私もその日だけの参加としました。
(OCamlについてはOCaml Users and Developers Workshopというイベントもあり、これもICFPと併設です。日付が重ならないように(隣になるように)配慮されているほか、(おそらくOCamlの方が人気なので)OCamlの枠に収まらなかった発表がML Familyの方に回されることもあるようです。)
LunarMLの開発を何年も続けていて、スター数もそこそこあるので目に留まりやすくなったのか、今年の前半に「今年のML Family Workshopで発表しないか」というお誘いをいただきました。ICFPは毎回開催場所が異なり、今年は10月にシンガポールでの開催でした。
続きを読む子供が生まれた/後進を育成すること
9月に子供が生まれました。出産に立ち会いましたが、妻にとっては文字通り命懸けで、感謝してもしきれません。父親として、妻と共に子育てを頑張っていきます。
今は育休をとって二人で世話をしています。職場では私はそれなりに重要なポジションなので、休むと他の人が頑張らないといけません。復帰した後は、迷惑をかけた分を挽回できるように頑張りたいところです。
それにしても、自分の子供というものは思った以上に可愛いものです。見ていて飽きません。穏やかに寝ていたら「寝る子は育つ!えらい!」、泣いていたら「赤ちゃんは泣くのが仕事!えらい!」、手足をバタバタ動かしていたら「筋トレだ!えらい!」、排泄をしたら「生命活動の証!えらい!」という具合です。親バカでしょうか。
この子がどんな大人に育つのか、その時の社会はどうなっているのか、わからないことだらけですが、少しでも良い未来になるようにできることをしたいです。
子供が生まれたことが象徴的ですが、自分の人生が「後進を育成する」段階に移りつつあることを感じます。もちろん、子供を育てていくには稼がないといけないので、自分自身もまだまだ挑戦を続けていく必要がありますが。
職場は若い人が多く、上司からは、彼らに私の技術を伝達することを期待されています。私が趣味の時間も注ぎ込んで獲得した技術をどうやって伝達すればいいのかはいまいちよくわかりませんが、なんとかやっていく必要があります。
また別の話ですが、趣味で貢献しているOSSプロジェクト(GHC)で、自分でやろうと思っていたタスクが経験の浅い人にアサインされた、ということがありました。自分でやればすぐ終わるのに、とは思いましたが、いいんです。新しい人に経験を積ませて戦力として育てればプロジェクトにとって長い目で見て得だろう、ということは私にもわかりますから。GHCに関して言うと、私はGHCにSIMDを実装することに取り組んでいますが、簡単なタスクはnewcomerのタグをつけて他の人に任せる、という手段も取っていくべきでしょう。
私としては、他の人に教えるということは性に合っていると思います。大学時代にやっていたサークルでは下の代に引き継ぎをする機会もありましたが、資料はそれなりに気合を入れて作っていた気がします。あるいは、大学院時代のTAもそれなりに頑張っていた気がします。普段書いている技術記事も、特定の読者を想定しているわけではありませんが、自分の知見を共有する行為です。
私は音声よりも文字媒体の方が得意です。会社での教育も資料を作るという形でやるべきなのでしょうか。それともペアプロ等を試すべきなのでしょうか。模索していきたいです。
プログラミング言語の表層構文の合理性/プログラミング言語の見た目を自然言語に寄せることが良いとは限らない
プログラミング言語の表層構文を見ていると、「自然言語(特に英語)に寄せたかったのかな」と思わされる語順を時々見かけます。例えば、Pythonの from somemod import a, b という語順は英語として自然に読めることを意識していると思われます。
こういう設計の背後には「自然言語のように読める構文が良い構文だ」という暗黙の仮定があるように思えます。しかし、それは正しいのでしょうか?
この記事では、いくつかの例を元に、プログラミング言語の構文の「合理性」はどのような基準で測られるべきなのかを考えます。筆者の主観(感覚)に基づく基準もあり、普遍的な基準を作成することを目指しているわけではありません。「それはお前がそう思っているだけなのでは?」と思われる部分もあるかもしれません。仮説、あるいは議論の材料の提示と思っていただくのが良いかもしれません。
続きを読むLunarMLの近況/中間言語に型をつける
私が作っているStandard MLコンパイラー、LunarMLの近況報告記事です。LunarMLに関する直近の記事は
でした。
400スター
GitHubスター数が400に到達しました。ありがとうございます(執筆時点では402に増えています)。まだスターをつけていない方は https://github.com/minoki/LunarML でスターをつけることができます。

スターが350に到達したのは2024年10月、300に到達したのは2024年5月のことだったようです。
(本プロジェクト限定というわけではありませんが)GitHub Sponsorsにも触れておくと、現在は @toyboot4e さんと @kevin-kmetz さんにスポンサーしていただいています。ありがとうございます。
https://github.com/sponsors/minoki
中間言語に型をつけたい:型をつける動機付け
JavaScript連携の記事で、
JavaScriptの
PromiseのthenはコールバックがPromise(正確にはThenable)を返したら更にそれを待ち受ける挙動をします。モナドのbindみたいな感じです。この仕様があると('a promise) promiseみたいな型をいい感じに扱えないので、Standard MLの世界のコードがPromiseの中身としてPromiseを返そうとした場合はラッパーを噛ませるようにします。
と書きました。「Promise の中身として Promise (より正確には Thenable)を返そうとした場合はラッパーを噛ませる」の部分をコードで説明すると、次のような関数 wrapThenable, unwrapThenable の呼び出しを適宜噛ませる形になります:
function ThenableWrapper(x) {
this.payload = x;
}
function wrapThenable(x) {
if (typeof x === "object" && typeof x.then !== "undefined") {
return new ThenableWrapper(x);
} else {
return x;
}
}
function unwrapThenable(x) {
if (x instanceof ThenableWrapper) {
return x.payload;
} else {
return x;
}
}
JavaScriptの通常の Promise との相互運用を可能にするため、値が Thenable ではない場合は元の値を活用します。
しかし、Promise の操作をするたびに必ず wrapThenable の呼び出しを挟むというのはダサいです。値の型が string や int など、明らかに Thenable ではないことがわかっている場合は、呼び出しを省略したいです。そのためには、最適化が進んだ段階でもコードの型情報を保持しておくことが必要です(インライン化によって型が判明する状況を考慮する)。現状のLunarMLでは最適化はCPS中間言語に対して行っているので、CPS中間言語を型付きにすることが必要です。
型情報の別の用例を挙げます。次のコードを考えます:
(* val foo : unit -> unit
val bar : unit -> string *)
val x : unit = foo ()
val _ = bar x
x は unit 型の変数で、情報を保持していません。こんなコードを書く人はいないと思われるかもしれませんが、最適化の結果としてこういうコードが現れることは十分にあり得ます。
この場合、ソース中の x という変数を出力コードに反映させるのは無駄です。特に、Luaではローカル変数は貴重な資源なので、節約したいです。そこで、「型が unit の変数の使用は値 () で置き換える」という変換が考えられます。
そんな感じで、中間言語、特にCPS中間言語に型がついていると便利そうです。
中間言語に型をつけたい:作業
LunarMLの中間言語は
- ソース(Standard ML)→(いくつかの前処理と型検査)
- →型付き中間言語→(モジュールの脱糖、オーバーロードとequality typeの脱糖)
- →System Fωライクな中間言語→(パターンマッチの脱糖)
- →System Fωライクな中間言語→(CPS変換)
- →CPS中間言語→(各種最適化)
- →CPS中間言語→(ネストされた式の回復)
- →ネストした式のある中間言語→(変換)
- →LuaやJavaScriptのコード→(変換)
- →最終的なLuaやJavaScriptのコード
という流れになっています。
従来は、System Fωライクな中間言語までは型がついていて、CPS中間言語には型がないという状況でした。3月ごろに、System Fωライクな中間言語の型検査器を実装しました。
今回、CPS中間言語を型付きにして、型検査器も実装しました。
型付きのCPS変換はしっくりくる先行研究が少なくて、なかなか難航しました。LunarMLの型付きCPSメモにいくつかメモりましたが。
最終的には、「型抽象と型適用は、通常の関数と関数適用と同様に扱う(ただしフラグをつけて区別できるようにする)」「最適化をある程度かけた段階で、多相型を消去する。完全に型を消去するのではなく、漸進的型付けのAnyのような感じで置き換える。その後再び最適化をかける」という形にしました。
最初は中間言語に対する型検査器はなくても良いかなと思っていましたが、型に関するバグがあったときに型検査器がないとエスパーでデバッグする羽目になり、しんどかったです。なので、結局型検査器を実装しました。実装したらしたで無限にバグが見つかってしんどいことになりましたが。
型周りのバグの発見には、過去に書いたテストが役に立ちました。テストは資産です。
悪いニュースとして、CPS中間言語に型をつけたことで、コンパイルが遅くなったり、メモリ使用量が増大したりしています。中間言語の型検査をやめれば時間の増加は軽減されると思いますが、テスト時はしっかり検査したいので、テストの所要時間は減らせなさそうです。
ML Family Workshop
今年のICFPはシンガポールでの開催で、それと併設で10月16日にML Family Workshopというのが開催されます。学会誌なんかは出ない、インフォーマルな集まりのようです。
このML Family WorkshopにLunarMLの話を応募したところ、通りました。というわけで、行ってきます。
このところLunarMLの作業を頑張っているのは、ML Family Workshopで話せる内容を少しでも増やしたいという気持ちからです。ですがCPS中間言語の型付けに時間を使いすぎた感があるので、そろそろ資料作成と発表練習をしないといけません。
バージョン0.3.0
ML Family Workshopの前になるか後になるかは不明ですが、そろそろ新しいバージョンとしてリリースしても良いかもしれないと思っています。ユーザー視点ではJavaScript周り(Promise連携とか)が新機能になるかと思います。GitHub Actionsでビルドする仕組みを整えたので、MLtonでビルドしたバイナリーも配布できると思います。
可算選択公理を仮定しない構成的数学での実数の構成について
可算選択公理を仮定しない構成的数学では、Cauchy列に基づいた実数の構成をやるときに完備性が示せなくなる(らしい)。この弱点は、実数の構成に使うCauchy列を有理数の点列ではなく、有理数の集合の列とすれば克服できる。
このことは「Handbook of Constructive Mathematics」のFred Richmanの記事で示唆されているが、あまり詳しい取扱いはなかったので自分でやってみた。と言っても、地味な命題の証明は省略しているが……。
https://miz-ar.info/math/real-construction-without-choice-20250816.pdf
Mathlogにも書いてみた。
続・TypeScriptのnever型の話/型付け規則についての雑談
前に書いた「TypeScript使いの憂鬱:never型はプロパティを持つか」の補足をして、関連する話題を取り上げます。前の記事では
「never型の式にプロパティアクセスができない」という動作は型システムの一貫性から外れた、アドホックな(場当たり的な)動作であるということです。
と書きました。「never型の式にプロパティアクセスができる」という動作が普通の型システムでどのように正当化されるのかを掘り下げます。
TAPLこと「型システム入門」をベースに説明します。
続きを読む有限にも無限にもなれない僕らの集合
「集合\(A\)が有限集合であるとは、ある自然数\(n\)に対し、\(A\)と\(\{0,1,\dotsc,n-1\}\)の間に全単射が存在することである。一方、有限集合ではない集合は無限集合である。」
「存在量化子\(\exists\)の有限回の除去は通常の論理でできるので、選択公理が力を発揮するのはもっぱら無限集合が相手の時である。」
……本当にそうだろうか?
「集合は有限集合か無限集合のどちらかだ」という考え方は排中律的であり、構成的数学では考え直す必要がある。
この記事では、「無限」ではないが「有限」とも言えない集合について考えたい。有限集合の定義は最初に書いたものとする。無限集合のちゃんとした定義はしない。
続きを読む良いコンパイラーは親切なエラーメッセージを出さなければならない:LunarMLの場合
プログラミング言語の静的解析の良い点として、一回の解析で複数の誤りを検出できる(場合がある)点があります。実行時エラーしか出ない言語だったら、一回の実行で一個のエラーに遭遇して、修正して、またエラーに遭遇して、ということを繰り返さなければなりません。
言い換えると、遭遇した最初の誤りでコンパイルが停止してしまうようなコンパイラーは、いくら静的な型システムを備えていても、動的言語並みの貧弱な開発体験しか得られないということです。コンパイルの手間がかかる分むしろマイナスです。
コンパイラーではなく言語サーバーでも同じことで、ソースコードの最初の誤りで解析が停止してしまう言語サーバーからは貧弱な開発体験しか得られないでしょう。
検出できるエラーの個数だけではなく、エラーメッセージの親切さも、結構開発体験を左右するのではないかと思います。よくある誤りに対して的確なエラーメッセージを出すことができれば、ユーザーがエラーの原因で悩む手間が省けます。
一つの言語仕様に対して複数のコンパイラーが存在する状況で、エラーメッセージの品質はコンパイラー間での差別化の要素になり得ます。この記事では、Standard MLコードに対して良いエラーメッセージを出す工夫について考えてみます。
続きを読む