今からTyped RacketのType Checkerを分からせます(多分こっちが負けます)

はぁい皆さんこんにちは. これは, UEC Advent Calendar 2019 5日目の記事です. ちなみに前回の記事は こちら. 良いです. 私もvimを使う(neovim)のですが, 人様のプラグインの情報を拾うたびに生活が豊かになっていくのでこういう話題はありがたいです. 私も今日は恐らく皆さんに知見を提供できる記事を書きます(フリ).

軽く自己紹介

私はUEC B2 一類CSのaskjfbd(email: askjfbd@protonmail.com, Twitterはやめたと言いつつひっそり活動しているので探し当てられたらすごい)と申します. 0x14歳です. 趣味で使う言語はRacket, Rust, Haskell(の順番で理解している)です. 授業サボって数学の独学するのも趣味で, 好きな定理は一点コンパクト化(フリ), 好きな数学分野は複素解析です(フリ). 数学に関わるプログラミング のお話(型理論, ラムダ計算とか)が好きすぎて好きです. TaPL通読してぇなぁ?(フリ) ところで, 12/17はZornの補題と呼ばれる定理を使って線形空間の基底の存在証明のお話したいと思っています. 線型代数なら一年生も今やってるはずです. 意外と抽象度が高い分野なのでちゃんとやると奥が深いです. その端っこの端っこの端っこを紹介できたら...

そして今回はですね, Typed Racketという言語で書かれた, とある単純な関数にお型付けしていこうと思います. まずはTyped Racketの解説から.

Typed Racket

Typed RacketはRacketのgradually-typed variantです. マクロを用いて動的型付け言語であるRacket上に静的型検査を実装しています. HaskellやRustみたいな人気で成熟しつつある言語の型検査器は驚くほど型推論が効いて書いていてひじょーにスッキリしますが, Typed Racketのそれはまだ未成熟, というよりLispのダイナミズムに合わせたLisp向けの型システムという物自体がまだ未完成であるためいろいろな試行錯誤が現在進行中です.

主な問題点はなんか知らんけど型推論が まともに効かない!!! ことです(怒りのダブルアスタリスク). こちらによればTyped Racketの作ろうとしている型検査器はHindley-Milner型検査器の機能を超える??らしく, HaskellみたいにREPLに直接関数定義したらいい感じに型変数が配置されているみたいにはいかないです.

まぁ自己書き換えさえ簡単に許してくれるLispに型付けしようと思ったら, 言語仕様に制限を加えるかType Checkerとの格闘を決断するかしか無いよね, うん. Typed Racketは後者を選んだわけで, まぁ辛いね. 体感ではTyped Racketの書き手は自分が書いている関数について極めて詳細な理解がないとそもそも永遠に型検査通らないです. 私も呻きながら型付けしてます. 構内で,もしくは気分転換で出掛けた先のキャッフェで黒ターミナル内neovim上のS式に向かって唸っている奴がいたらそれ私です. 探さないで下さい.

生意気なType Checkerを分からせる¹

さぁこのわからず屋で生意気なType Checkerを一緒に分からせていきましょうか. 今回お型付けする関数はこれです.

今回の討伐対象

これは, 任意のheterogeneous listが与えられたらそこから生成される順列全体を生成してlistに入れて返す関数です.

まずはとりあえず型宣言します.

とりあえずお型付け

はい, lintが警告を発しています. "Cannot apply polymorphic function"ということですが, これこそがtyped racketの苦しみの原因, polymorphic関数同士の掛け合いみたいなのが上手く推論できないのです. どういうことかというと, foldr, appendはこういうふうに型宣言されていて, ²

foldr, appendの型宣言

ここのAllの一番目のargumentが型変数であるわけですが, ここの整合性を人間が保ってやらないといけない, つまり今回の呼び出しがfoldrのtype-caseのうちのどのケースに属していて, 引数のappendがpolymorphicであるので実際にどのような型(ここは型変数でもオッケイ. なぜなら一番始めにcombinations自体の型宣言をしているから)で呼び出されるのかを人間が指摘してあげないといけないわけです. 私はこれをPoP(Polymorphic on Polymorphic)エラーって呼んでます. これこそが苦しみの源. 災いの芽. この問題が解決されないままなら卒研で取り組んでも良いんじゃないかレベルで解決してほしい問題の一つですね...

ところで

やばい書く気力が失われてしまった!! (@ Wed 04 Dec 02:59:09 PM JST) からちょっと休む. 一人籠もって自分が生みたい進捗(最近はあれです, 赤雪江を年内に終わらせる宣言したのとTaPLを1年かけて読み込むプロジェクトが熱い...熱い)をうめないと気が狂ってしまう人間なので, 生みます進捗. 進捗産みます. ところで生むと産むってどう違うんだろう.

帰ってきたぞ (@ Thu 05 Dec 2019 12:36:56 JST)

それじゃあつづき始めましょうか. まず, foldrをなんとかします. 今回我々が使うfoldrの利用例はHaskellのそれと全く変わりがないので, ちょっとしたwrapperを書いて苦労を減らしましょう. 多分意味ないけど. いや, Racketって日本語の情報がほぼ無いので, あるのはアカデミックな公式ドキュメントだけですからこっちもいろいろ試行錯誤なわけです. 外人お兄さんお姉さんがYouTubeで熱く語っている動画を漁ってまで解決策を探したりします...

迫真お型付けされたmy-foldr

あとはこのa, bにうまいことappendを当てはめますが, appendも自作しましょうか.

迫真自作append

そしたらテストしてみます. 見た感じListの中身(combinationsだと型変数a)でmy-appendをinst(こちら. 関数の型シグネチャを指定してます)するだけで通る!!

生意気なType Checkerをとうとう分からせました(@ Thu 05 Dec 2019 02:38:55 JST)

見て下さい!!! このブログを書きながら試行錯誤してたら通りましたよ! あとはこれの解説をしていけばいいかな.

やったぜ

再掲載(高らかな勝利宣言)

まず, 先程作ったmy-foldrとmy-appendで最初の関門は突破しました. あとは, my-foldrに渡されるListが(Listof (Listof (Listof a)))であることを指定すれば通ります. 式がある特定の型であることを示唆するのには(私が知っている範囲では)2つの方法があり, 一つはann, もう一つはcastで式を修飾するというものです. これらの違いを実はよく理解していないのですが, 恐らくannの方は静的チェック, castの方は動的チェックが実行されます. つまりtype checkerに補助的な情報を渡してコンパイルするときにはann, type checkerに我々のことを信頼させて実行時に型チェックを入れるようにするのがcastっぽいです. ここは間違ってそうなので指摘お願いします. そうして, 2重のmapのところに来るべき型情報を指定してmy-foldrに補完情報を与えてあげると...コンパイルが通ったわけです. 嬉しい. 勝てないと思ってたので...

追記(@ Thu 05 Dec 2019 07:33:19 PM JST)

今までの作業は全部いらんかった...ただappendの一番目の型変数を指定したらコンパイル通っちゃいましたわ... まぁこれを理解するための試行錯誤みたいなところあったのでaskjfbd的にはオルオーケイです.

最終形態

唐突な終わり

これでひとまず終わりです. Typed-Racketお型付け配信またやりたい...それでは次の人にバトンタッチします. 明日の記事は, rbsd66さんの, "創造に対する所感"です. 私は人の経験からくる知見を聞くのが好きなので楽しみにしていまっす. ではでは.

---

1. マリン船長控え目に言って好きです(激白)↩

2. Allというのは,こちらにある通り, 型変数を用いたシグネチャ宣言をする時に用いるitemです. ↩