Lambda the Ultimate

For the simple "typed evaluator" example, yes, you cannot define incorrect ASTs. However, this wont be the case in general. Most ASTs are more complicated and contain variable definitions and references (things that, AFAIK, aren't usually checked by leveraging the host's type system). Even for pure expression evaluator ASTs, complete assurance requires that the host language's type system be able to express the type system of the target language.

GADTs are a mechanism for defining more precise types. It helps you make stronger guarantees on an AST structure, which reduces the number of explicit consistency checks you have to perform in code.

I come from an OO background. When I started learning Haskell, I noticed that I couldn't exactly express the types I wanted, though I couldn't put my finger on exactly why. Turns out, Java-style OO with generics provides a level of precision that wasn't available in Haskell without GADTs. The following paper helped me see what GADTs bring to the table by looking at them from an OO perspective: Generalized Algebraic Data Types and Object-Oriented Programming

To me, probably the most exciting aspect of GADTs is the possibility of adding dynamic security level support to type-based information flow security a lá Flow Caml. However, it also seems that GADTs offer many, if not all, of the benefits of dependent types, and I think Tim Sweeney's POPL 06 slides do an excellent job of enumerating a few critical benefits of dependent types. But it's worth pointing out that GADTs are very general, which unfortunately means that you might need to read a lot of the literature to get a good cross-section of application domains, since you're right—everyone does seem to trot out the "typed term evaluator" example.

You can get safe code by encoding the properties you desire, but just how easy it is encode properties remains to be seen.

Check out Tim Sheards page for a few examples. GADTs can be used to marshall/unmarshall data in a type safe manner, enforce patterns of usage, encode semantic properties (e.g. a tree is balanced, a list has length > n, etc). They've come up a few times in the haskell' list, but people are still figuring out how they interact with haskells other features.

I don't know if this counts as 'interesting' as such, but I needed GADTs to build an AST for the 'language' formed by a monad and write an evaluator for it (this turns out to be a pretty easy way to implement a new monad). While return was trivial and bind doesn't need GADTs per se (just existentially quantified datatypes), the put and get operations for a state monad constrain the computation's return type and GADTs allow that to be expressed in the type of the corresponding constructors.

In logic programming you don't need to know the dimension of an array (or a list)! Deduction figures it out.

Andres Loh shows an embedded DSL for contracts in Haskell using GADTs in Typed Contracts for Functional Programming.

Dynamic Optimization for Functional Reactive Programming using Generalized Algebraic Data Types by Henrik Nilsson

A limited form of dependent types, called Generalized Algebraic Data Types (GADTs), has recently been added to the list of Haskell extensions supported by the Glasgow Haskell Compiler. Despite not being full-fledged dependent types, GADTs still offer considerably enlarged scope for enforcing important code and data invariants statically. Moreover, GADTs offer the tantalizing possibility of writing more efficient programs since capturing invariants statically through the type system sometimes obviates entire layers of dynamic tests and associated data markup. This paper is a case study on the applications of GADTs in the context of Yampa, a domainspecific language for Functional Reactive Programming in the form of a self-optimizing, arrow-based Haskell combinator library. The paper has two aims. Firstly, to explore what kind of optimizations GADTs make possible in this context. Much of that should also be relevant for other domain-specific embedded language implementations, in particular arrow-based ones. Secondly, as the actual performance impact of the GADT-based optimizations is not obvious, to quantify this impact, both on tailored micro benchmarks, to establish the effectiveness of individual optimizations, and on two fairly large, realistic applications, to gauge the overall impact. The performance gains for the micro benchmarks are substantial. This implies that the Yampa API could be simplified as a number of “pre-composed” primitives that were there mainly for performance reasons are no longer needed. As to the applications, a worthwhile performance gain was obtained in one case whereas the performance was more or less unchanged in the other.

GADTs are very useful for deriving combinator libraries in the style of John Hughes. His paper The design of a pretty-printing library is a good example of the methodology although it doesn't use GADTs. A paper which could have used GADTs, had they been available at the point of writing is Koen Claessen's Parallel Parsing Processes. In section 5 he needs to do a hack with the Symbol constructor because he didn't have GADTs available. Using GADTs we can instead write:

data P s a where
  Symbol :: P s s
  Fail   :: P s a
  (:+++) :: P s a -> P s a -> P s a
  (:>>=) :: P s a -> (a -> P s b) -> P s b
  Return :: a -> P s a

In my experience the use of GADTs pops up quite frequently when using this design methodology.