In the past, I've used them to eliminate and optimize branches with simple interpreters. That being said, I've had better luck with using things like Coq to wr

In the past, I've used them to eliminate and optimize branches with simple interpreters. That being said, I've had better luck with using things like Coq to write a certified interpreter and then outputing to OCaml. In any case, when we write a simple interpreter for a typed language, we normally run things through a type checker first and then evaluate it. After type checking, we know that certain errors can not occur, such as adding an integer to a boolean, but this information gets lost when passing everything to the evaluator. As far as the evaluator knows, all we have are expressions, so we still have to check for situations like adding an integer to a boolean in the evaluator. Again, this can not occur because we type checked everything, but these branches are necessary to have the OCaml compiler type check everything. What GADTs allow is for the type checker to translate an expression into a typed expression and then the evaluator translates a typed expression into a value. This eliminates these redundant branches. For some sample code, I wrote about this on StackOverflow some time back. The following link contains both a traditional implementation of an OCaml interpreter as well as one that uses GADTs. It differs some from the one in the article because I work out how to make this work with an environment, lambda functions, and closures: https://stackoverflow.com/questions/22676975/simple-lambda-calculus-dsl-using-gadts-in-ocaml https://stackoverflow.com/questions/22676975/simple-lambda-c...