📝
Lean 4のメタプログラミングで数独チェッカーを作った
TypeScriptとScalaで型レベルプログラミングを使ってエディタ上で数独をプレイできるようにするという遊びを見かけました。
Leanでもやってみた
Leanなら割と簡単に、普通の(メタ)プログラミングでいけそうだなと思ったのでやってみました。
コードはgistにありますが、↓のリンクからWeb上で実際に遊べます。
数独をプレイするには、エディタの一番下の行に移動してこんな感じで問題を入力します。
#sudoku
- , 5 , - , 2 , - , - , 4 , - , 6,
- , 6 , 4 , 1 , - , - , - , 7 , 5,
- , 2 , 8 , - , 6 , 5 , 1 , - , 3,
8 , - , 6 , - , 7 , 2 , - , - , -,
- , - , 3 , 8 , - , 1 , 5 , - , -,
- , 1 , 7 , - , 4 , - , - , 2 , 8,
- , - , 5 , 9 , - , - , - , 4 , 1,
4 , - , - , - , 1 , 3 , - , - , 9,
9 , 8 , - , - , 5 , - , - , 3 , -
end
まるで最初からLeanに数独をプレイするための機能があったかのように見えて楽しくないですか？
コードの前半は数独のルールを素直に書いていて、後半にメタプロで「エディタ上でプレイする」部分を実装しています。
元ネタとは根本的に違うことをやっていますが、まあエディタ上で数独ができるという点では同じなので見逃してください。
(「型チェックが通るなら数独として間違いがないことが保証される」という仕組みも簡単に作れると思うので、あとで追記します)
差別化ポイントとして、並の言語では真似できなさそうな、エラーメッセージで重複がどこにあるか指摘したり、全部解けた時にお祝いする機能もあったりします。
「依存型があって数学の証明さえ書ける」というのがLeanのウリですが、数学とか関係なく自分の思いついた構文や機能を自由に追加できるというのもまた大きな魅力だったりします。
自分がインプットするばっかりで全然布教のための記事を書けてないんですが、非関数型言語ユーザのためのLean入門コンテンツもそのうち作りたい…
日本語のLeanコミュニティの紹介
-
Discord: LEAN勉強会
- Leanの教材やその他の題材をテーマにしたゼミが日夜開催されています
- 「この教材を理解したいけど一人では途中で詰まってしまう」という時はここに書いてもらえれば一緒に勉強できます
- 初心者歓迎です
-
Discord: LEAN JA
- 勉強会に限らない、Leanの話題全般のための場所です
Discussion