Ich habe nach dem Konzept von GADT in OCaml gesucht, warum wir es brauchen und wann wir es verwenden sollen, usw.
Ich verstehe GADT ist nicht nur in OCaml, sondern ein allgemeiner Begriff.
Ich habe
gefundenusw., aber einige von ihnen sind in Haskell, und andere haben kein gutes Vergleichsbeispiel zwischen no GADT und GADT .
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?
GADTs sind aus zwei Gründen nützlich.
Bei der ersten (und der gebräuchlichsten) handelt es sich um dynamisches Schreiben: Sie können eine dynamische Eingabe 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 finden Sie im ocaml-Handbuch . 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 jedoch ziemlich schwer auszudrücken, und man muss sich oft sehr anstrengen, das zu tun. Nun, ich habe kein praktisches Beispiel, aber ich habe einmal 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 die GADT-Funktion und ihre guten Anwendungsfälle, können Sie die ziemlich gute Blogpost von Mads Hartmann.
Ich bin auch auf der Suche nach einer guten Anwendung von GADT, da ich die meiste Zeit, wenn ich sie früher oder später benutze, feststelle, dass das Gleiche ohne sie und normalerweise auf eine viel sauberere Art gemacht werden kann. Also, das ist keine vollständige Umfrage, nur ein bisschen meiner eigenen Erfahrung.
Universelle Werte, auch bekannt als Existenzen. Sie ermöglichen es Ihnen, heterogene Container und typsichere Serialisierung zu erstellen. Siehe zum Beispiel die Module Univ und Univ_map von Core.
Typsichere Evaluatoren für Syntaxbäume. Hier sind GADTs nützlich, um einige Laufzeitprüfungen zu entfernen.
Reine und typensichere Printf Implementierung , das ist schon ein Teil von OCaml, wurde auch mit GADT umgeschrieben
Hier ist ein echtes Beispiel , wie GADT sein kann benutzt. Im Beispiel verwende ich GADT, um Tabellenbeziehungen anzugeben, z. B. one_to_one , one_to_many usw. Abhängig von der verwendeten Beziehung wird der Funktionstyp entsprechend abgeleitet. Beispiel: one_to_maybe_one relation, gibt eine Funktion 'a -> 'b option zurück, one_to_many erstellt 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.
Tags und Links ocaml