Effective Haskell

GADTs: Functions from Terms to Types

GADTs are a new way to define data types that give us more flexibility in the ways we express our data types, and which remove some limitations in how we can define constructors that help us combine term and type level programming. They also give us a brand new syntax for defining data types. We can enable GADTs with the GADTs extension. In this section, we’ll look at how to use GADTs to define some types you’re already familiar with, and how they can be used to handle features like existential types more easily. After that, we’ll look at how GADTs fit in with type level programming, and you’ll see how to use GADTs to represent data types that couldn’t be written with traditional types.

GADTs
	The GADTs ...