OCamlでGADTを実証するための具体的な簡単な例は？</p> <p>など

Question

私たちはそれを必要とするときにそれを使用する理由のOCamlにGADT の概念の周りを検索したが、私はGADTはOCamlのではなく、より一般的な用語だけではありません理解しています。私は、など

What are GADTs?

http://caml.inria.fr/pub/docs/manual-ocaml-400/manual021.html#toc85

http://www.reddit.com/r/ocaml/comments/1jmjwf/explain_me_gadts_like_im_5_or_like_im_an/

を見つけたが、それらのいくつかはHaskellであり、そして他の人がなしGADTの間の良好な比較の例を持っていない

およびGADT。

私が望むのは、GADTがないと状況が悪いかどうかを確認できるシンプルで優れた具体的な例です。

どうすればいいですか？

Answer 1

GADTは、2つの理由から有用です。

最初のもの（最も一般的なもの）は動的な型付けに関するものです。動的な型指定を静的なチェックを失うことなく追加できます。それは簡単なことではありませんが、あなたのタイプ条件が満たされることを確信することができます。 その最も簡単な例はocaml manualです。 これは、標準ライブラリでprintfをタイプセーフな方法で書き直すために使用されていました（それ以前はObjのかなり恐ろしいコレクションでした）。マジック）

GADTを使用したいと思う2番目の理由は、タイプ構造を維持したい複雑な不変条件がある場合です。これは表現するのがかなり難しいですし、しばしばそれを行うために多くの努力を払わなければなりません。 まあ、私は便利な例はありませんが、AVL木の実装を書き留めている友人が、タイピングシステムによってバランスがとれていることが証明されていました。

GADTの機能とその優れた使用例については、Mads Hartmannのかなり良いblog postを読むことができます。

Answer 2

私はGADTをよく使うアプリケーションを探しています。ほとんどの場合、私はそれらを早くまたは後で使用しても、同じことがそれらがなくても、もっときれいに。だから、これは完全な調査ではなく、ちょっとした自分の経験です。

1. ユニバーサル値、別名existentials。それらを使用すると、異種のコンテナを作成し、型保証されたシリアル化を行うことができます。例としてコアのUnivとUniv_mapモジュールを参照してください。

2. 構文木のタイプセーフな評価基準。ここでGADTはいくつかのランタイムチェックを削除するのに便利です。

3. 純正タイプセーフPrintfimplementation、それはすでにOCamlのの一部ですが、またGADT

を使用して書き直されました。ここGADTを使用することができる方法の現実の生活exampleです。この例では、GADTを使用して、表の関係を指定します（例：one_to_one、one_to_manyなど）。使用される関係に応じて、関数のタイプがそれに応じて推測されます。たとえば、one_to_maybe_oneの関係は、関数'a -> 'b optionを返します。one_to_manyは、'a -> 'b listで関数を作成します。 1つの関数link ~one_to:relationではなく、link_one_to_one,link_one_to_manyなどのようないくつかの異なる関数を作成するだけで同じことができます。したがって、このアプローチを議論の余地があると考えることができます。