Ein konkretes einfaches Beispiel, um GADT in OCaml zu demonstrieren?

Question

Ich habe um für das Konzept der GADT in OCaml gesucht, warum wir es brauchen, und wenn es zu benutzen, usw.

Ich verstehe GADT nicht nur in OCaml Eine allgemeinere Begriff ist.

Ich habe

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/

etc gefunden, aber einige von ihnen sind in Haskell, und andere nicht haben einen guten Vergleich zwischen Beispiel kein GADT und GADT.

Also was ich möchte ist ein einfaches, aber gutes konkretes Beispiel, wo ich sehen kann, ob ohne GADT, die Dinge schlecht sind.

Kann ich das bitte haben?

Answer 1

GADTs sind aus zwei Gründen nützlich.

Die erste (und die gebräuchlichste) ist die dynamische Typisierung: Sie können eine dynamische Typisierung hinzufügen, ohne die statische Überprüfung zu verlieren. Es ist zwar nicht einfach, aber Sie können sicher sein, dass Ihre Typbedingungen erfüllt werden. Das einfachste Beispiel dafür ist in der ocaml manual gegeben. Dies wurde zum Beispiel in der Standardbibliothek verwendet, um printf typsicher zu schreiben (vorher war es eine ziemlich schreckliche Sammlung von Obj.magic)

Der zweite Grund, warum Sie GADTs verwenden möchten, ist, wenn Sie eine komplexe Invariante haben, die Sie in Ihrer Typstruktur pflegen möchten. Das ist ziemlich schwer auszudrücken, und man muss sich oft sehr anstrengen. Nun, ich habe kein praktisches Beispiel, aber ich habe mal gesehen, wie ein Freund eine Implementierung von AVL-Bäumen aufschrieb, wenn das Typisierungssystem bewiesen hatte, dass das Balancieren richtig war, was ziemlich cool ist.

Für mehr ein die GADT-Funktion und seine guten Anwendungsfälle, können Sie die ziemlich gute blog post von Mads Hartmann lesen.

Answer 2

Ich bin auch auf der Suche nach einer guten Anwendung von GADT, wie die meiste Zeit, wenn ich sie früher oder später benutze, entdecke ich, dass das gleiche ohne sie gemacht werden kann, und normalerweise auf eine viel sauberere Weise . Also, das ist keine komplette Umfrage, nur ein bisschen von meiner eigenen Erfahrung.

1. Universelle Werte, auch bekannt als existentials. Sie ermöglichen es Ihnen, heterogene Container und typsichere Serialisierung zu erstellen. Siehe zum Beispiel Core's Univ und Univ_map Module.

2. Typsichere Evaluatoren für Syntaxbäume. Hier sind GADTs nützlich, um einige Laufzeitprüfungen zu entfernen.

3. pur und typsichere Printfimplementation, ist, dass bereits ein Teil von OCaml wurde auch

mit GADT neu geschrieben

Hier ist ein echtes Leben example wie GADT verwendet werden kann. In dem Beispiel verwende ich GADT, um Tabellenbeziehungen zu spezifizieren, z. B. one_to_one, one_to_many usw. Abhängig von der verwendeten Beziehung wird der Funktionstyp entsprechend abgeleitet. Zum Beispiel, one_to_maybe_one Beziehung, gibt eine Funktion 'a -> 'b option, one_to_many schafft eine Funktion mit 'a -> 'b list. Dasselbe kann erreicht werden, indem einfach mehrere verschiedene Funktionen wie link_one_to_one, link_one_to_many usw. anstelle einer Funktion link ~one_to:relation erstellt werden. Also kann man diesen Ansatz als strittig betrachten.