良い感じのプログラミング言語習得ルート
初回書込日時:2024-01-06
初めはRust
Rust→Lean4,Erg
この3つはどれもドキュメントが良く出来ている。
初めはRust
問答無用で初めはRustを学ぶべき。
まずコンパイルエラーが神。他の言語のみなさんはあのコンパイルエラーを見習ってほしい。んでもって所有権ルールと借用規則(shared xor mutable)も良い。所有権ルールによって値をガチに"物"として見ることができる(変数は人、関数は機械に例えれると思う)し、借用規則は当たり前のことしか言っていない。
自分はRustからプログラミングを学び始めたので、基本情報技術者試験のためにサラッと覚えていたデータベースのロック機構と同じようなものと捉えていたところ、"所有権システムは難しい"なんて言われるほどでは一切ないと感じた。
テキトー言ってるサイトを排除し(Rustを選んだ時点で大多数排除できる)、とにかくまずはThe Book読んだほうがいいと思う。2章で急にボコボコにしようとしてんのか分からん実践をかましてくるけど、ここは辛かったら飛ばしてもいい。ただとにかく「Rustが出来るようになればこんなものも作れるようになるよ！」みたいなことを示したいんだと思う。
本当にThe Bookで学ぶのが辛いなら別に他のリソース読んでもいいと思う(例えばZennの本とか)。よく知らないけど。
The Bookを読み終えたら次にRust by Exampleをやった方が良い。例から学ぶことで「そういうことだったんだ！」「そういう書き方やっていいんだ！」みたいなことを得られる。
もし他のリソースを読んで「この書き方なんだ…？よく分からないな…」となったら、公式リファレンスで調べると良いだろう。"リファレンス"と聞くととても辞書的で端的にしか書かれていないようなイメージがあるが、Rustのリファレンスは違う。懇切丁寧に説明してくれる。
またstdライブラリもドキュメントが丁寧に書かれている。「この型/関数/メソッド/etc.どう使うんだ…？」ということを全部話してくれるし使い方の例がメソッド1つ1つにあるし注意事項も書かれている。
Leanについて
Leanは書き方としては、現在勉強しているあたり(パターンマッチング)までではRustとHaskellの中間のような感覚。
Rust寄りかも。
ただ括弧(コードブロックの波括弧とか関数の引数のための括弧とか)は無い。
だけどオフサイドルールな訳でもない。オフサイドルールにヒヤヒヤしないで済むのは大分ありがたい。
追記2024-01-16
今第3章まで読んでいるが、神言語かもしれん
追記2024-01-29
とにかくあらゆるものに境界がない。値と型の間には階層の違いしかない。特に型として命題を指定できるし、帰納型と構造体型と型クラスにはほぼ境界がなく、構造体は帰納型にコンストラクタやフィールドのアクセス関数を自動的に提供する機能が生えたものとして、型クラスは構造体にコンパイラによる自動インスタンス探しが生えたものとして、結局帰納型と同一視される。インスタンス宣言はデフォルトの名前が提供されるdefなだけ。inductive、structure、class、instanceにはよくwhereが使われるが別にdefにおいても使える。命題の集まりとして型クラスが定義されているのもある(モナド則を満たしたモナドのLawfulMonadとか)
というかError Lensとの兼ね合いが神
追記2024-01-30
関数は値として捉える。そもそもLeanでは概念を全部階層で考えたほうがいい。とりあえず命題と関数と値はSort 0。帰納型、構造体型、型クラス(の値とかではなく型そのもの)はSort 1。関数はSort 0だから、その実装は構造体型のフィールドにはならない。代わりにその構造体型の名前空間に値のようにして存在する。
※↑ガチで違うこと言ってる (2024-03-22追記)
でも以前の記述の通り、型クラスは構造体で、関数をフィールドとしているわけだけど、こいつらは何なのか。こいつらは関数の実装を持っているわけではなく、関数のシグネチャ(で言葉合ってる？)が型である。だからその実装は値(inst{型クラス}{実装した型})である。
何が言いたいのかというと、ダイヤモンド継承問題は"関数(の実装)はフィールドにならない"で解決されている。
"望むならオブジェクト指向にも手続き型にもなれる定理証明できる関数型言語"とか究極の言語すぎない？
追記2024-03-03
えーSort 0はProp(命題)のみであり、関数や値は"関数や値"です、すまん
階層的にはSort 0っぽく考えていいと思うけど
なんでLeanを選んだの？
いくつかの定理証明支援系とか依存型付き言語の中でなんでLeanを選んだか、メモって置こうと思ったので
- @tanakhさんと@hisaketMさんが言及していたから
- ほぼどれにしようかな的に決めた
Idris、Agda、Lean、Koka、Ergの中でどれにしようかな～って小一時間悩んでたんだけど、どれもコミット活発だしスター数ほぼ同じくらいだし…で、スター数が3.4kで唯一ギリギリ3k超えだったので選んだ。あとTwitterで見た中で"言及され回数"が一番多かった。
Ergについて
ごめんね今はLean勉強中でErgのことはまだ初めの方しか触れれていません><
僕はMojoよりもErgを応援しています！
他のメジャー言語について
他のメジャー言語はRustが分かってたら多分ちょっと覚えればすぐ出来るようになるだろ~~~~~~~~