GADT学習用教材

Question

Haskell Wiki で GADT について読み始めましたが、よく理解できませんでした。Haskell 初心者向けに GADT を説明している本の特定の章やブログ投稿をお勧めしますか?

Answer 1

ApfelmusはGADTs のビデオチュートリアルをしました役に立つかもしれません。

Answer 2

の例が気に入っています GHCマニュアル. 。シンプルですが、いくつかの重要なポイントを示しています。

• GADT を使用すると、Haskell の型システムを使用して、実装している言語 (「オブジェクト言語」) の型システムをモデル化できます。

• これにより、Haskell の静的チェックで、「コンパイラー パス」またはその他が型を保持していることをアサートできるようになります。オブジェクト言語の用語を受け取る関数は、それらの用語が適切に型指定されていると想定できます。オブジェクト言語の用語を返す関数は、適切に型指定された用語を生成する必要があります。

• GADT コンストラクターのパターン マッチングにより、型の改良が行われます。 eval タイプがあります Term a -> a 全体的には右側ですが、 eval (Lit i) タイプがあります Int, 、左側のコンストラクターには型があったため、 Term Int.

• Haskell システムは、GADT コンストラクターにどのような型を指定しても気にしません。すべてのコンストラクターを同様に簡単に作成できます。 data Term a 型の結果を与える Term a, 、 または Term Bool, 、 そしてその data 定義はまだ通過します。でも、私たちには書けないでしょう eval :: Term a -> a. 。モデル化する GADT の「タグ タイプ」を選択します あなたの これにより、作成したい便利な関数が適切に型付けされます。

Answer 3

その他のリンク:

• http://www.haskell.org/haskellwiki/Generalized_algebraic_datatype
• http://www.comlab.ox.ac.uk/people/ralf.hinze/talks/FOP.pdf

Answer 4

私が見た中で最高の説明ですのダミーのためのHaskell wikiの GADTsます。

I（およびI容疑者他の人が）最も紹介していな問題は、彼らはあなたがのGADTsを理解するまで、の非自明である構文の面でGADTsの例を示すことです。これは完全に理解し、あなたが挑戦していることが、すべての文の正確な役割を理解しているパターンの多くのものを推測することができ、すべてが、特にハードに構築されている最も簡単な例になります。

ポスト解剖「ダミーのために」と、それはるかに便利な出発点になり、独自の基本的な例を説明する道に沿って、構文の意味を構築します。私は非常にお勧めます。