Tutte le esercitazioni su GADT che ho visto (in Haskell, Coq e Idris) usano una stessa versione di un interprete ben tipizzato per mostrare come le GADT possono essere utili, in cui si utilizza l'indice di tipo per codificare il tipo di GADT termine nella lingua dell'oggetto.
Quali sono alcuni altri esempi e regole generali per quando dovremmo pensare a GADT come soluzione?