What are GADTs and why do they make type inference sad? (blog.polybdenum.com)
from armchair_progamer@programming.dev to programming_languages@programming.dev on 04 Mar 2024 03:30
https://programming.dev/post/10951812

A Generalized Algebraic Data Type (GADT) is a generic ADT where some variants have specific type arguments, e.g.

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.

data StringToFrom =
  forall a. StringToFrom (a -> String) (String -> a)

These are often combined like

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.

#programming_languages