[解決済み] Haskellの次に学ぶべき言語とは？[クローズド］

質問

最初のプログラミング言語として、私はHaskellを学ぶことにしました。私は分析哲学を専攻しており、Haskellを使うことで、例えば自然言語解析のためのトランスデューサー、定理証明器、インタプリタなど、興味のあるプログラムを素早く正確に作成することができました。プログラミングを始めてまだ2ヶ月半ですが、Haskellの意味論と構文は、より伝統的な命令型言語よりもはるかに学びやすく、その構成の大部分に（今）快適さを感じています。

しかし、Haskellでのプログラミングは魔術のようなもので、私はプログラミングの知識を広げたいと考えています。新しいプログラミング言語を選んで学びたいのですが、任意の言語を手に取り、それを捨てて、繰り返すのに十分な時間がありません。そこで、私が探している言語のタイプに関するいくつかの条件とともに、この質問をここで投げかけてみようと思います。いくつかは主観的であり、いくつかはHaskellからの移行を容易にすることを意図しています。

• 強力な型システム。Haskell でのプログラミングで私が好きな部分の 1 つは、型宣言を書くことです。これは、個々の関数とプログラム全体との関係についての私の考えを構造化するのに役立ちます。また、プログラムの正しさについて、非公式に推論することも容易になります。私は効率ではなく正しさに関心があるのです。
• 反復よりも再帰に重点を置いています。私はHaskellで繰り返し構造を使いますが、それを再帰的に実装します。しかし、特にコンビネータやmaps, folds, bindのような高次の関数を使う場合、複雑な反復処理よりも再帰的な関数の構造を理解する方がはるかに簡単である。
• 学ぶことにやりがいを感じる Haskell は やりがいのある 言語です。カントを読むような感じです。しかし、数年前の私のCでの経験はそうではありませんでした。私は C 言語を求めているわけではありません。言語は概念的に興味深いパラダイムを強制すべきですが、私の完全に主観的な意見では、C が好きな人はそうではありません。

回答の重み付け : もちろん、これは単なるメモです。ただ、きちんとした形の回答をくれた皆さんにお返事したいだけです。とても助かりました。

1) いくつかの回答は、再帰を強調する強力な静的型付け言語が別の関数型言語を意味することを示しました。私は Haskell で強力に作業を続けたいのですが、camccann と larsmans は、別のそのような言語が "ease the transition too much." と正しく指摘しました。証明支援ツールでは、CoqとAgdaが面白そうです。特にCoqは構成的論理と形式的型理論の堅実な入門になると思います。私は一階述語と様相論理（Mendellsohn、Enderton、Hinmanの一部）に少し時間を費やしたので、おそらくCoqで多くの楽しみを持つことになるでしょう。

2）その他はLisp（Common Lisp、Scheme、Clojure）を強く支持しました。私が調べたところ、Common LispとSchemeはどちらも入門教材が充実しているようです( Lispについて と 推論されたスキーマ , SICP ). の素材は SICP の資料を見ると、私はSchemeに傾倒している。特に、Scheme を通して SICP を通してのSchemeは、異なる評価戦略、遅延の実装、連続体、インタプリタ、記号計算などのトピックに焦点を当てる機会を提供してくれるだろう。最後に、他の方も指摘されているように、Lispのコード/データの扱いは全く新しいものになるでしょう。したがって、私は(2)のLispという選択肢に大きく傾いているのです。

3）第三に、Prologです。Prologには興味深い材料が豊富にあり、その プライマリ の領域は、まさに私が興味を持っているものです。Prologはシンプルな構文で、読みやすい。今はこれ以上コメントできませんが、Prologの概要を読み、入門書をざっと読んでみたところ、(2)にランクインしました。そして、Prologのバックトラックは常にHaskellにハッキングされているような気がするのです

4）主流の言語の中では、Pythonが最も面白そうです。Tim Yatesは、この言語がとても魅力的に聞こえるようにしています。どうやら、PythonはCS専攻の1年生によく教えられているようで、概念的に豊かであるか、学びやすいかのどちらかです。もっと調べてみないとわからないですね。

みなさん、おすすめをありがとうございました Lisp（Scheme、Clojure）、Prolog、CoqやAgdaなどの証明アシスタントが主に推奨される言語のようです。

どのように解決するのですか？

私はプログラミングの知識を広げたいと考えています。(...) 私は、私が探している言語のタイプに関するいくつかの規定とともに、ここで質問を提起しようと思いました。いくつかは主観的であり、いくつかは Haskell からの移行を容易にすることを意図しています。

強力な型システム。(...) それはまた、私のプログラムの正しさについて非公式に推論することを容易にします。私は効率ではなく、正しさに関心を持っています。

反復よりも再帰に重点を置く。(...)

あなたはここで少し移行を緩和しすぎているのでは、と私は思います。非常に厳密な型システムと純粋に関数的なスタイルは Haskell の特徴であり、主流のプログラミング言語に似たものはほとんど、これらのいずれかを少なくともいくらか妥協する必要があります。そこで、このことを念頭に置いて、以下のような大まかな提案をしています。 最も を維持しつつ、いくつかの大きな転換を行うことを目的とした、いくつかの広範な提案です。

• 実用性を度外視して、"more Haskell than Haskell"を目指す。 : Haskell の型システムは、非終端やその他の面倒な妥協のために、穴だらけです。その混乱を一掃し、より強力な機能を追加すると、次のような言語が生まれます。 Coq や アグダ であり、関数の型はその正しさの証明を含んでいます（関数の矢印も読むことができます -> を論理的含意として読むこともできる！）。これらの言語は、数学の証明や、極めて高い正しさを要求されるプログラムに使われてきた。Coqはこのスタイルの最も著名な言語でしょうが、AgdaはよりHaskellらしい雰囲気を持っています（Haskell自体で書かれていることもありますが）。

• 型は無視し、魔法を追加する : もしHaskellが魔術なら。 Lisp は生の、創造の原始的な魔法である。Lisp 系の言語(また スキーム と Clojure など）は、ほぼ無比の柔軟性と極端なミニマリズムを兼ね備えています。Lispのメタプログラミングは、いくつかの言語では非メタプログラミングよりも簡単です。

• 少し妥協して主流に近づける : Haskell は ML に大きく影響された言語の広範なファミリーに属し、どの言語もおそらく もなく移行できるでしょう。 に移行することができます。Haskellは型と関数型の使用による正しさの保証に関しては最も厳しいものの一つであり、他のものはしばしばハイブリッドスタイルか、様々な理由のために実用的な妥協をしている。もしあなたが、OOPに触れ、多くの主流の技術プラットフォームにアクセスしたいのであれば、以下のどちらかをお勧めします。 スカラ はJVM上で、または F# は、Javaや.NETプラットフォームとの容易な相互運用性を提供しながら、Haskellと多くの共通点を持っています。F# は Microsoft によって直接サポートされていますが、Haskell に比べて厄介な制限があり、非 Windows プラットフォームでの移植性の問題があります。Scala は Haskell の型システムの多くと Java のクロスプラットフォームの可能性に直接対応していますが、よりヘビー級の構文を持っており、F# が享受している強力なファーストパーティのサポートがありません。

これらの推奨事項のほとんどは、他の回答でも言及されていますが、私の理論的根拠が何らかの啓発を提供することを願っています。