GADTs are weak approximations of inductive families from dependently typed languages—so let’s begin there instead. Inductive families are the core datatype introduction method in a dependently typed language. For instance, in Agda you define the natural numbers like this data Nat : Set where zero : Nat succ : Nat -> Nat which isn’t very … Read more
Author of the roles system here. I’m aware of no ideas that will move us forward in this direction. The problem is that we’d need to check a delicate property in order to ensure that the coercion is safe. Specifically, we want to be able to coerce e.g. HList [Age, Int, String] to HList [Int, … Read more
It defines a new type, the syntax is called generalized algebraic data type. It is more general than the normal syntax. You can write any normal type definition (ADT) using GADTs: data E a = A a | B Integer can be written as: data E a where A :: a -> E a B … Read more