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

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

threaded - newest