What are GADTs and why do they make type inference sad?
What are GADTs and why do they make type inference sad?
blog.polybdenum.com
What are GADTs and why do they make type inference sad?
A Generalized Algebraic Data Type (GADT) is a generic ADT where some variants have specific type arguments, e.g.
haskell
data Expr a where
EValue :: a -> Expr a
ELessThan :: Expr Int -> Expr Int -> Expr Bool
EIfElse :: Expr Bool -> Expr a -> Expr a -> Expr a
The post also mentions existential (existentially-quanitifed) types, which are types with a type variable in some variants which isn't in the type itself, e.g.
haskell
data StringToFrom =
forall a. StringToFrom (a -> String) (String -> a)
These are often combined like
haskell
data Expr a where
EValue :: a -> Expr a
ELessThan :: Expr Int -> Expr Int -> Expr Bool
EIfElse :: Expr Bool -> Expr a -> Expr a -> Expr a
EApply :: forall a. Expr (a -> b) -> Expr a -> Expr b
EEquals :: forall a. Expr a -> Expr a -> Expr Bool
and this breaks Hindley-Milner type inference, an algorithm which is guaranteed to infer every type in a simpler type system, but inferring every type in one with GADTs (specifically, polymorphic recursion) or existential types is undecidable.