From: "andrew cooke" <andrew@...>

Date: Tue, 20 Jun 2006 10:26:16 -0400 (CLT)

This looks very interesting: A limited form of dependent types, called
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.

http://www.cs.nott.ac.uk/~nhn/Publications/icfp2005.pdf

From http://lambda-the-ultimate.org/node/1293#comment-18853