popl2008 ** 1. GADTs are syntactic sugar. The real structures at work are existentially quantified types and the equality GADT. 2. Indexing by a set, rather than a category, as GADTs do means that really this is dependently typed programming faked in Haskell by using kind level proxies for types 3. As a result, Haskell ends up with a curious "logic programming" feel to its type level computation and functional programming feel to its term-level computation. PJohann and NGhani ** his main point (which worked with me) is that we should pay more attention Kan extensions. We already know and love (strong) functors, (co)monads, adjunctions and the Yoneda lemma.