5956fd49.md

title	date
GADT	2020-05-25

The key point about GADTs is that pattern matching causes type refinement.

-- GHC User Guide

An example GADT:

data Query result where 
  Query_NotesByTag :: Tag -> Query [Note]
  Query_AllTags :: Query [Tag]

Pattern matching on the GADT constructor causes type refinement. For example, pattern matching on the constructor Query_NotesByTag refines the type (of the query result) to [Note]. GADTs are extremely useful for this purpose, something that cannot be achieved with regular ADTs (algebraic data types).

<z:zettels?tag=gadt>