About
概要:
巨大データ処理で活躍したParquet＋Polarsの話から、開発環境を快適にするzoxideやStarship、そして数学の証明もできるプログラミング言語Leanまで、2026年のはじめに試した技術・ツールについて話しました。
- Apache Parquet（パルケ／パークエット）とは CSVとの違い（行指向 vs 列指向） カラムごとにデータをまとめることで、必要な列だけを高速に読み出せる構造 Row Group／Column Chunkという単位で保存され、並列処理と相性が良い フッターにスキーマ（型情報）を埋め込むことで、型推定不要＆圧縮効率アップ
ランレングス圧縮・辞書圧縮などにより、CSVよりも小さいサイズ＆高速読み込みを実現
Parquet＋Polarsで1000万〜1400万行をさばいた話
1000万行のCSV処理でI/O待ちがボトルネックになり、CPUコア（32コア）が遊んでいた問題 データをParquetに変換＋Polarsを利用することで、読み込みが約30倍高速化 Polarsの- ストリーミングモード：ファイルと接続しつつ少しずつ処理 レイジーモード（遅延実行）：フィルタやマップをチェインして、最後に一括最適化実行
- 「金で殴る」戦略で処理が一瞬で終わるように
CSVとParquetの使い分け（ヒューマンリーダブル vs 型付き・高速・大規模向き）、手札を増やすことの大事さ
zoxide：次世代CDコマンド
cdコマンドの「賢い」代替として使えるツール 一度訪れたディレクトリを学習し、曖昧な入力からジャンプできる- 例：cd doc で、どこにいても「documents」的なディレクトリに飛べる
コマンド自体は z だが、ホストは cd にエイリアスして完全な置き換えとして使用中
Starship：リッチなシェルプロンプト
ターミナルのプロンプトをカラフルかつ高機能にするツール Gitリポジトリの状態、使用中の言語ランタイムやバージョン（例：UV管理下のPython 3.x）などを自動表示 見た目がきれいになるだけでなく、「今このディレクトリはどんな環境か」を一目で把握できるそこまで意識して凝視はしていないが、入れておくと地味に便利な存在
Lean：数学の証明もできる関数型言語
マイクロソフト発の定理証明支援・関数型プログラミング言語 数学の証明（定理・公理系の形式化）にも使われる一方、普通のプログラミング言語としても利用可能 現在ホストがやっていること：- 四則演算をする簡単な電卓プログラムをLeanで実装（パーサ付き） いずれは本格的な研究にも組み込みたい構想
- 例：ペアノの公理系で自然数を定義 0があり、その「次の数（サクセッサ）」として1, 2, 3…を定義する 足し算のルールなどを公理として書き、そのルールから「1+1=2」が導けることを機械的に証明 Leanでは、ループや再帰が「必ず停止する」と証明されないと実行できない構造もあり、無限ループを防ぐ ソート関数がどんな入力でも必ず終了し、正しく並び替えることなども数学的に保証できる