Haskell GADT Idea
A generalized algebraic data type is a data type whose constructors can each choose their own result type. It is written with the data type where form.
Each constructor chooses a result type
TInt makes a Term Int value. TBool makes a Term Bool value.
{-# LANGUAGE GADTs #-}
data Term a where
TInt :: Int -> Term Int
TBool :: Bool -> Term Bool
termKind :: Term a -> String
termKind (TInt _) = "int"
termKind (TBool _) = "bool"
main :: IO ()
main = do
putStrLn (termKind (TInt 7))
putStrLn (termKind (TBool True))
The same name holds both result types
Term is one type name. Its two constructors build two different result types.
{-# LANGUAGE GADTs #-}
data Term a where
TInt :: Int -> Term Int
TBool :: Bool -> Term Bool
termShow :: Term a -> String
termShow (TInt n) = show n
termShow (TBool b) = show b
main :: IO ()
main = do
putStrLn (termShow (TInt 7))
putStrLn (termShow (TBool True))
A function can demand one result type
getInt accepts only a Term Int value. getBool accepts only a Term Bool value.
{-# LANGUAGE GADTs #-}
data Term a where
TInt :: Int -> Term Int
TBool :: Bool -> Term Bool
getInt :: Term Int -> Int
getInt (TInt n) = n
getBool :: Term Bool -> Bool
getBool (TBool b) = b
main :: IO ()
main = do
print (getInt (TInt 7))
print (getBool (TBool True))
Example
{-# LANGUAGE GADTs #-}
data Term a where
TInt :: Int -> Term Int
TBool :: Bool -> Term Bool
getInt :: Term Int -> Int
getInt (TInt n) = n
getBool :: Term Bool -> Bool
getBool (TBool b) = b
termKind :: Term a -> String
termKind (TInt _) = "int"
termKind (TBool _) = "bool"
main :: IO ()
main = do
putStrLn (termKind (TInt 7))
print (getInt (TInt 7))
putStrLn (termKind (TBool True))
print (getBool (TBool True))
Key points
- GADT: a data type where each constructor picks its own result type.
- Where form: write a GADT with data followed by where and one constructor per line.
- Extension: the GADTs extension enables the where form for data types.
- Constructor result: TInt builds a Term Int value and TBool builds a Term Bool value.
- Ordinary ADT: every constructor of an ordinary data type returns the same result type.
In this example, Term is the GADT, getInt and getBool demand one result type each, and termKind names the shape of each value. The main action first names the integer shape and prints its stored number, then names the boolean shape and prints its stored boolean.
Note
pattern matching on a GADT is covered in a later lesson and is where the precise type is used.
Try it Yourself
Edit the code, then press Run.
Running is simulated · Haskell Playground
Exercise
What can each constructor of a GADT choose?