43

Idrisチュートリアル、Agdaチュートリアル、および他の多くのチュートリアルスタイルのペーパーと、まだ学習していないことへの終わりのない参照を含む入門資料があります。私はこれらすべての真っ只中にいるようなもので、ほとんどの場合、数学表記と新しい用語が説明なしに突然現れることに固執しています。おそらく私の数学は最悪です:-)

依存型プログラミングにアプローチするための統制のとれた方法はありますか？Haskellを学びたいときのように、「自分自身にHaskellを教えて」から始め、Scalaを学びたいときは、Oderskyの本から始めます。Rubyの場合、変異したバグを含む奇妙なチュートリアルを読みます。しかし、私は彼らの本でアグダやイドリスを始めることはできません。彼らは私の頭上にあります。私はCoqを試してみましたが、そのすべてを証明するスタイルで立ち往生しました。アグダは巨大な数学のバックグラウンドを必要とし、イドリスは、まあ、今はそれを残しましょう！

私は静的型システムをよく理解しています。私はScalaにある程度精通しており、必要に応じてHaskellを使用できます。私は関数型パラダイムを理解し、それを日常的に使用しています。代数的データ型とGADT（実際には非常にスムーズに）を理解し、最近ラムダキューブを理解することができました。しかし、私は数学と論理の部分が不足しています。

4

2 に答える 2

30

Software Foundationsを強くお勧めします。この本は、Coq を 1 ステップずつ紹介するのに非常に適しています。はい、多くの定理が証明されていますが、それは依存型の利点の一部です。「プログラミング」と「証明」の境界線がぼやけ始めるのは素晴らしい気分です。

ただし、数学と論理の部分が不足しています。

Software Foundations は、知っておく必要のあるロジックについて理解を深める上で非常に優れた仕事をしていると思います。ただし、含意の概念にすでに慣れていると役立ちます。

于 2012-11-21T17:30:33.877 に答える
22

（注意：これは自己宣伝です）

私はAgdaチュートリアルを書いています。私の主な目標は、理論的な背景がなくても、人々がAgdaで遊べるようにすることです。

このチュートリアルは、ほとんどの問題を解決する可能性があります。

  • 外部参照なしでAgdaプログラミングを説明しようとします
  • 中等学校の数学だけが必要です
  • プログラミングの実践も教えようとします

開発中ですが、前半は準備ができています。

于 2013-01-12T10:32:29.993 に答える