PythonのRust製新型型チェッカー Pyrefly vs Ty 比較

やってみたよ。＜コードは省略＞うーん、これ、全然うまくいかないな。mypyは互換性のない型の値を自由に混ぜるのを許しちゃうんだ。どうしたら直せるかわかんない。Dとintを直接足そうとするとmypyは怒るのに、join_stuffの引数がSemigroupであることに加えて、全部互換性のある型であることを insist する方法が見つからないんだよ。mypyは join_stuff の中では Semigroup を具体的なクラスとしてチェックしてるみたいで、引数の実際の型はどうでもよくなっちゃうっぽい。でも、加算が定義されてない引数は受け付けないって言ってくれるのはマシだけどね。

長年Python書いてるけど、人が犯す一番ひどい間違いは、型ヒントをつけないことと型チェッカーを使わないことだって思うよ。

バカはまあいい。でも ＿Nonsense＿ はダメ。君の挙げた例はナンセンスで、不合理だったよ。最初の例を見た瞬間、「あ、これは add_ints にして int だけ取るべきだ」って思ったもん。「”the human body is dumb！ Here’s an example： if I stab myself, it bleeds！”」って俺が言うようなもんだと思ってみて。それってバカな例？ それとも不合理な例？

でも、ここまでやったの、めっちゃクールだよ！ この時点でもうPythonと戦い始めてる感じだね。Pythonはこういう風に設計されてないからさ。でも、それでもクールだ！

言語使ってもないのにどうやって意見持つのか教えてくれない？ 型の議論で、使ってない言語に文句言って不自然な例作る人いるの面白いね。＞”I think that the goal there is to understand that even with the best typing tools, you will have troubles, unless you start by establishing good practices.”
Likeーwhat makes you think that python developers doesn’t understand stuff about Python, when they are actively using the language as opposed to you？

あと、カスタムで表現力豊かな Pydantic 型を作らないで、色んなとこでネストした dict を使うこと。ネストした dict はマジ最悪だよ。中に何が入ってるか全然わかんないし、クラスに変換する時間は絶対かける価値あるって。

こういうもの 중심으로作られてる、とんでもない量のPythonコードをあんたは過小評価してると思うよ。たくさんの企業がLLMのAPIじゃなくて、自分たちでモデル改造したりファインチューニングして自社データセンターにデプロイするんだ。それって、さらにPythonコードが増えるってこと。LLM APIに頼るだけならどの言語でも書けるけど、それがAIブームの全部じゃないからさ。

モダンなPythonアプリ開発を始めて半年経ったけど、リンター、型システム、テスト、仮想環境、パッケージマネージャーとかさ…。Rustって難しいって言われてるけど、Pythonを”大規模”に使いこなして、それを維持し続けるより、よっぽど簡単だって気づいたよ。

＞ でも、その性質上、ダックタイピングは無限の入力型をサポートしてるし、それがPythonの基盤なんだ。それは四角い釘を丸い穴に押し込むようなものだよ。正しいとか間違ってるとかの話じゃないんだ。
関数がどんな型でも動作してほしいのか、2つの値を加算（またはサポートされてるか分からない操作、つまりダックタイピング）しようとして、うまくいかなければ実行時エラーを投げるのか
—この場合は型付けしないかAnyを使えばいい—
それとも、不正な引数でメソッドが呼び出されないように、実行前に強力な型安全性を保証したいのか
—この場合は受け付ける型を何らかの方法で表現する必要がある—
完全にダックタイピングされたメソッドを使いたいなら、Anyを使うべきなんだよ。それがAnyが存在する理由なんだ。Anyを使えないなんていうこじつけのシナリオを作り出すのは、論点を外してるよ。ポインタを使っちゃダメって言われたらCが動かないって文句を言ってるようなもんだ。
歴史的にPythonコードはダックタイピングを念頭に書かれてたっていうのは君の言う通りだけど、今やPandasみたいな柔軟なライブラリですら型定義をサポートしてる。エコシステムは5〜6年前とは全然違うし、今では良い型付けサポートがない有名ライブラリなんて思いつかないな。

この点が全然理解できないな。俺はDjangoのコードベースで働いたことあるけど、そこには膨大な型付けの問題があったよ…。100%じゃないにしても、型チェックから得られる価値は大きいんだ！
十分な関数にアノテーションをつければ、すごく良いリンターになるんだよ！

俺の車のエアバッグだって、99.99%の時間は必要ないんだぜ。

もし君が”ソフトウェアに長けてる”って自称してるのに、Pythonを動かすのに時間をかけすぎてるなら、もしかして君はソフトウェアが得意じゃないんじゃないかって可能性を考えてみてよ？
Pythonには欠陥もあるし、大きなものもあるけど、人気があるのには理由があるんだ。特にpydanticやfastapi、uv（とstreamlit）みたいなツールを使えば、以前は数週間や数ヶ月かかってたようなクレイジーなことも数時間でできるんだ。AIがこれらのフレームワークでコードを生成するのもどれだけ優秀か言わずもがなだよね。pydanticを使った型付けが特にお気に入りだよ。どんなメソッドもファイルやDBからデータをダンプ＆ロードできるし、極めて簡潔で検証済みのコードが手に入る。最新のIDEも部分的に型付けされたコードからでも価値を素早く引き出すのを簡単にしてくれるよ。完璧じゃないものにも心を開いて、試してみることをお勧めするね。

＞ あと、多くの企業はLLMのAPIを使うことにはあまり興味がなく、自分たちのモデルを修正・ファインチューニングして、自分たちのデータセンターにデプロイするでしょう
モデルトレーニングに何百万ドルもかかるって分かってる？「多くの企業」ってのは、どうもおかしいな。
訓練に必要な膨大なデータも数に入れてないし、高価な専門家もだ。
それに、古くなったモデルを定期的に再訓練する必要がある。
AI分野で最先端モデルを提供してるのが一握りのプレイヤーだけで、しかも彼らが皆50億ドル以上の価値があるのには理由があるんだよ。

みんなが、そしてその辺の犬まで、Pythonで自分たちのモデルを開発する準備が必要だって思ってるからだよ。
これは正直、特にスタートアップの世界では現実にあることだね。

AIが理由でサーバーコードをPythonに移行してる人がいたら、俺はびっくりするね。

そうするとコンパイルが必要になるでしょ。つまり、Pythonプログラムと一緒にテキストファイルを配布するだけじゃ済まなくなるんだよ。Pythonの各バージョン、各アーキテクチャ、各OSごとにビルドインフラが必要になるんだ。
それ楽しんで！

型アノテーションがどれだけ簡単か忘れてると思うよ。
古いPythonコードをいじるのにたまに2時間くらい使うことがあるんだけど、そのうち15分くらいを型アノテーションの追加に費やすんだ（たまに簡単なリファクタリングが必要だけど）。これはとてつもないROIがあるよ。コストはめちゃくちゃ低いのに、メリットはすぐに出るんだ。
こういう場合、コードをちゃんとした言語に移行して相互運用性を考えるなんて、俺の頭の中にはないね。それは正気の沙汰じゃない。だから、ベストエフォートで型安全性を得られる選択肢があるのは、絶対的に素晴らしいことなんだ。
君の言うことも確かに理解できるよ。精力的に開発中のプロジェクトにとっては有用な分析だね。でも、ほぼ問題なく動いてて、ほんの少しずつ変更があるだけの大きなPythonコードベースがあるなら、型アノテーションを追加するのは素晴らしい戦略だよ。

あの記事が明確にしてるのは，PythonとTypeScriptの型システムの違いかな．TypeScriptは，ヤバいダックタイピング言語でみんながメチャクチャなコード書くのを，現状のまま型で固めちゃうのが目標なんだ．
でもMypy（とそれを元にしたPythonや他の型チェッカー）は，ヤバいダックタイピング言語なのに，そうじゃないフリしてアカデミックな厳格なルールを押し付ける感じ．これは実際のコードの書き方とかライブラリとの連携とかあんまり気にしてないんだよね．
最初から型ヒント書いてたら，Mypyが許す限られた範囲で書くから“大丈夫”になる．
でも成熟したプロジェクトに型ヒント足そうとすると，型システムが超限定的でコードベースの多くの部分が表現できないって気づいて，マジで発狂するよ．

＞tyは，その一方で，違うマントラに従ってるんだ：gradual guarantee．主要なアイデアは，型付けされたプログラムで，型アノテーションを消しても型エラーが起きないこと．つまり，動いてるコードに型エラーを直すために新しい型を追加する必要はないってことだ．
Tyが提供する gradual guaranteeは興味深いね．それに基づいて試してみようか考えてるよ．
既存の動的コードベースがあるPythonみたいな言語では，gradual typingの正しいやり方って感じだね．

Gradual typingってのは，コードベースのどこかに暗黙的な“any”（不明な型）があってもエラーにも警告にもならないってこと．完全に型付けしたと思ってた重要なコードでさえね．タイプミスとか推論の限界で型チェッカーが突然お手上げになって，「このファイルは問題ないよ！」って自信満々に言ってくる場所でね．
彼らの考えはわかるんだけど，Mypyを試した時に究極的に問題だったのは，型から保護されてるって保証が全くなかったこと．「このファイルにはgradualityはない，完全に型付けされてる！」って断言できる方法が重要なんだ．でもgradual typingは移行のためだけじゃなくて，動的言語でできるヤバいこととか，静的型付けを重視しない人を遠ざけちゃう誤検出を恐れてる部分もある．Maybe “soft” typingって呼んだ方が分かりやすいかもね．
俺はgradual typingは今の段階ではアンチパターンだと思うよ．

＞Gradual typingってのは，コードベースのどこかに暗黙的な“any”（不明な型）があってもエラーにも警告にもならないってこと．完全に型付けしたと思ってた重要なコードでさえね．タイプミスとか推論の限界で型チェッカーが突然お手上げになって，「このファイルは問題ないよ！」って自信満々に言ってくる場所でね．
これは良い指摘で，ty開発時に考慮してる点の一つだよ．
The benefit of the gradual guarantee is that it makes the onboarding process less fraught when you want to start (gradually) adding types to an untyped codebase．No one wants a wall of false positive errors when you first start invoking your type checker．
The downside is exactly what you point out．For this，we want to leverage that ty is part of a suite of tools that we’re developing．One goal in developing ty is to create the infrastructure that would let ruff support multi-file and type-aware linter rules．That’s a bit hand-wavy atm，since we’re still working out the details of how the two tools would work together．
So we do want to provide more opinionated feedback about your code — for instance，highlighting when implicit Anys show up in an otherwise fully type-annotated function．But we view that as being a linter rule，which will likely be handled by ruff．（文字数制限のため一部英語のまま・記号変換のみ）

これ，すごく理にかなってるし，TypeScriptがやってることと全く同じだね．暗黙的なanyはTypeScriptのエラーにはならない（これは定義からして当然だけど），でも当然，anyがあると潜在的に安全じゃないってことだ．これを対処するために，noImplicitAnyやstrict mode（99％のプロジェクトで有効になってるだろうけど）をオンにできる．
ここでの違いは，strict modeがtscのオプションなのか，それともリンター（ruff）にこの種のルールがあるのか，ってことだけど，最終的な結果は同じだ．
とにかく，長々と説明したけど，tyかruffには型チェックのための「strict」モードみたいなものが絶対に必要だってことだね．:)

Gradual guaranteeをオフにして，より厳格な挙動にするフラグとかって，あり得るのかな？

異なるフォルダやファイルにスコアを与えて，「型付けの確実度」のレベルを示し，失敗の閾値を定義できるようにするってのはどうかな．

＞Gradual typing means that an implicit “any” （unknown type） anywhere in your code base is not an error or even a warning．
それは gradual typingの実装によるね．Elixirは gradual set-theoretic typesを実装してて，動的な型は既存の型の範囲で，型違反に対して洗練されるんだ．ここに trivialな例があるよ：
def example（x） do
{Integer．to_string（x）， Atom．to_string（x）}
end
この関数はuntypedだから，xは初期値としてdynamic（）を得るけど，Integer．to_string（x）でdynamic（integer（））に洗練された後，Atom．to_string（x）でatom（）型と互換性がなくなるから，still typing violationを報告するんだ．
俺たちはstrong arrowsっていう概念も導入したんだ．これは動的な部分と静的な部分のコードベースが，実行時チェックを導入せずにsoundなままで連携できるようにするもの．詳細はここを見てね：https://elixir-lang．org／blog／2023／09／20／strong-arrows-gradua…

この関数定義（あるいは parameter x だけかな）はどうして“untyped”なの？ parameter x の型がemptyで，関数の型はエラーがあるから関係ないって推測するのに十分な情報はあると思うんだけど．
関数の本体に最初か二番目の呼び出しだけが含まれていたら，x はそれぞれ Integer か Atom で，関数の型は含まれる式の型だって判断されるはずだよ．

オレたちにとって、型推論と型チェックは、全パラメーターが dynamic 型の場合と同じなんだ。だから、たとえ明示的に dynamic ってシグネチャを付けても、他のツールが見逃すような違反もオレたちは見つけるよ。 dynamic ってのは”何でもあり”って意味じゃなくていい、ってのがポイントね。

ty は gradual set-theoretic types や”範囲付き” dynamic 型（Any や Unknown との組み合わせ）もできるよ。全ての使い方で dynamic 型を洗練化はしてないけど、似たことは考えたことある。
君の例だと、 Integer.to_string（x） と Atom.to_string（x） の両方を満たす x の型って none（） にならない？ none（） はエラーにしてるの？

へぇ、それはすごいね！情報交換したいな〜。 set theoretic types の研究者も興味あるって。面白そうなら、Gmail で。
オレたちのシステムは双方向。 Integer.to_string に適用前にドメイン（ integer ）計算。 x が dynamic なら洗練。最初の呼び出しで x は dynamic ＆ integer に。２回目の洗練は none で失敗→捨てる。 Atom.to_string も失敗。だから none はチェックして捨てる。

他のコメントでも触れたけどさ、 gradual typing に従ってる TypeScript にはそれを無効化する（徐々にね）フラグがいっぱいあるんだよ。 ty がそれをやらない理由はないよね。

gradual typing anti-pattern の話ね。 dynamic 言語は極端になるけど、ヤバい型システムも簡単。型システムの話は置いといて、 pydantic みたいなランタイムチェックで型を現実と一致させることもできるよ。 Sorbet （ Ruby の型チェッカー）はシグネチャにランタイムチェックを入れる。 ts では zod があるね。

＞ チームは pydantic みたいなランタイムチェックで型を現実と一致させられる
それがバグの問題。常に避けられた方法はある。 pydantic はユーザーデータ検証など特定の場所は良いけど、静的型チェッカーの代わりには現実的じゃない。
全ての呼び出し側が関数呼び出し（引数、名前）をチェック、全ての呼び出される側が手動で引数型を検証する必要がある。

pydantic は CPU 時間も食うし、ランタイムまで何もしないんだ。型チェックは IDE でリアルタイムにできるから、実際に実行して１５分も無駄にする前に修正できるよ。

はっきり言うと、オレは健全な型システムが好き。でも現実では、型なし Python 、 Ruby 、 Javascript から始めて生産的だったチームが、今も生産的でいるには静的型を徐々に追加する必要があるんだ。
＞ 全ての呼び出し側が関数をチェック
ここが良いのは、段階的な部分。コードの型付けが進むにつれて、ランタイムバリデーションの場所を移動、最終的にシステムのエッジに全部移動できる。

pydantic にはこのユースケース向けの @validate_call ってのがあるよ。

プロファイルしてみて、どれだけ遅くなるか見てみ？

本当に厳密な保証が欲しいコードでは、mypyで“no implicit any”みたいなエラーをオンにして、大事なファイルの制限を厳しくするんだ。境界ではまだ“garbage in/garbage out”問題はあるけど、少なくとも信頼性は上げられるよ。もしマジでやるなら、全部にオンにして、明示的なAnyはオフ、型なし依存関係全部にラッパー書くとかね。欲しいものは手に入るけど、結構大変かもしれないね。

うん、悩ましいよね。僕の経験だと、gradual typingって、やりたい人が自分のコードに適用して、やらない人は全くやらないか超適当なんだ。gradualとstrictを切り替えられる仕組みがあるといいなと思うよ。

“man mypy”してから15秒もかからないよ。–disallow-any-exprってすぐ出る。君が全部書くより早かったんじゃない？

新規開発じゃない限り、gradual typingが唯一の方法だよ。僕はmypyでいくつかの既存Pythonコードベースに型ヒント入れたけど、現実的なのはモジュールごとに“opt-in”していくしかないんだ。もしPyreflyがそれをサポートしないなら、使い道はかなり限られると思うな。あるいは、LLMコード生成向けなのかな。LLMがPythonスクリプトを生成するのには、すごく速くて厳密な型チェッカーが役立つかもしれないね。

これ、Typescriptが初期の頃、既存の大きなプロジェクトへのスムーズな導入パスに焦点を当ててたのを思い出すな。“noImplicitAny”みたいな厳しい要件も、全部のチェックを有効にする“strict”スイッチを最後にオンにする前に、一つずつオンにできたんだ。

PythonじゃなくてRustを書くことでお金をもらってる身だけど（色々ある中の一つ）、自分としてはRustプログラマーって感じだし、僕にもgradual guaranteeが一番理にかなってると思うな。

これは僕にとっては大きなマイナスポイントだな。Pythonに型アノテーションを追加する目的の半分は、エラーになりやすい動的型付けを制御することなのに。技術的にはPythonで許されてても、何か馬鹿なことしたら知りたいんだよ。願わくば、ちゃんと動くコードを気にする人向けに、何らかのno-implicit-anyとか“strict”モードを追加してほしいね…

” my_list ＝ ［1, 2, 3］”
” pyrefly, mypy, and pyright all assume that my_list.append(“foo”) is a typing error, even though it is technically allowed (Python collections can have multiple types of objects!)”
” If this is the intended behavior, ty is the only checker that implicitly allows this without requiring additional explicit typing on my_list.”
編集：こんなキツいコメントにするつもりじゃなかったんだ、本当はtyを応援してるんだよ：）
元コメント：ここのtyの挙動には強く反対だな。プロダクションコードではほぼ常に単一型のリストを使うし、型チェッカーがそれを仮定するのはすごく重要だよ、特にリストに既に同型のリテラルが入ってる場合はね。Pythonがこれを許してるかどうかは全く関係ない。型チェッカーがlist［int | str］を暗黙的に許しちゃうのは、初心者レベルのコード向けに最適化してるみたいに見えるんだ。

” Ｉ am strongly against ty behaviour here.”
［ty開発者です］
tyはまだ完成してないことに注意してね！
この特定の例では、tyがリストリテラルの型を推論する際に気の利いたことを何もしてないからつまずくんだ。要素に何が入ってても、プレースホルダーとしてlist［Unknown］と推論してるだけなんだよ。Unknownはgradual type（Anyと全く同じ）で、だからappend呼び出しが成功するんだ、どんな型もUnknownに代入可能だからね。
リストの型をもっと正確に推論する計画はあるよ。思ってるより複雑になるだろうね、周囲のコンテキストでそのリストをどう使ってるか考慮するための“双方向”型付けが必要になるから。それに関するトラッキング課題がここにあるよ：https://github.com/astral-sh/ty/issues/168

怒ってるみたいに聞こえなかったら良いんだけど、その挙動には本当に驚いたんだよ：）
4万行くらいの型なしコード（辞書があちこちで使われてたり）を完全に型付けされたコードに変換した経験から話してるんだ（最初はmypyに頼ってたけど、4分の1くらいでpyrightに移行したよ）。その状況だと、この挙動はたくさんのバグを隠しただろうね。
でも、まだ開発中だって聞いて安心したし、プロジェクトの成功を祈ってるよ。

記事の引用の”段階的な保証”って考え方と、これどう関係すんの？
tyの今の動きはそれに合ってるみたいだけど、変えちゃうと合わなくなるんじゃない？（いろんな型のリストに型付けできなくなるって話じゃなきゃ）

不変ジェネリックをもっと正確に型付けする方法はあるよ。
例えば
x = [] # list[Unknown]
x.append(A()) # list[Unknown | A]
takes_list_of_a_or_b(x) # list[A | B]
どうするかはまだ決めてないけどね。このへんで段階的な保証を少し妥協するかも。これは絶対のルールじゃなくて、考慮してる要素の一つなんだ。

list[int | str]みたいに型付けはできるけど、使うときに要素の型をチェックする必要が出てくるよ。
もしコードがそうしてないなら、Pythonの型付け的には”well typed”じゃないと思う。
だから色々な型のリストは持てるけど、型ガードが必要になったりするんだ。
もちろん、tuple[int, int, int, str]みたいのもあるし、いつかFixedListみたいなのも出るかもね。

Pyreflyがどうやってるか見た？ それともやり方違うの？

うちはまだ実装してないから、互換性があるかはまだ言えないな（笑）。
でも冗談抜きで、Pyreflyとかmypy、pyrightの開発者とはよく話してるよ。ツール間で大きな非互換性が出ないようにね。
食い違いがあるときは、それが事故じゃなくて意図的なもので、ちゃんと理由があって、仕様通りで、しっかり文書化されてるようにしたいんだ。

これ、初心者向けじゃなくて、既存のレガシーコード向けに最適化してるんだと思う。
型なしのデカいコードベースに型チェッカーを入れるのは大変だけど、既存コードがほとんど通るなら楽になるからね。

それなら、その挙動を有効にするオプションを用意すべきだよ。
型エラーが出たときに設定で例外を追加する方が、黙ってパスして本番のバグで型が混ざってるのに気づくより安全だと思うな。

これは型チェッカーじゃなくて、型アシストのリンターでやるべきだと思うな。
俺的には、動的言語の型チェッカーは実行時エラーを防ぐのが主な役割。
複数の型があるリストだと、型チェッカーは要素を使う前に型チェックしろって強制すべきだ。
静的な型が必要なら、Pythonは間違った言語だよ。

このツール、まだバージョン番号もないプレビュー版なんだから。
落ち着けってば。