I was reading the GADTs for dummies page on the Haskell Wiki, and I still don't understand how and why they should be used. The author provided a motivating example:
data T a where
D1 :: Int -> T String
D2 :: T Bool
D3 :: (a,a) -> T [a]
What exactly does this code do and why is it useful?
If this question is a little too vague, perhaps a related question is: can GADTs be used to implement member functions?
In functional programming, a generalized algebraic data type (GADT, also first-class phantom type, guarded recursive datatype, or equality-qualified type) is a generalization of parametric algebraic data types.
This is a type where we specify the shape of each of the elements. Wikipedia has a thorough discussion. "Algebraic" refers to the property that an Algebraic Data Type is created by "algebraic" operations. The "algebra" here is "sums" and "products": "sum" is alternation ( A | B , meaning A or B but not both)
Lets say you want to model a Fruit bag. This bag can have apple or oranges. So as a good haskeller you define:
data Bag = Oranges Int | Apples Int
That looks nice. Let's see that Bag
type alone without looking at the data constructors. Does Bag
type alone gives you any indication whether it is orange bag or apple bag. Well not statically, I mean at runtime a function could pattern match on value of Bag
type to detect whether it is oranges or apples but won't it be nice to enforce this at compile time / type check time itself, So that a function that only works with Bag of apples cannot be passed bag of oranges at all.
This is where GADTs can help us, basically allows us to be more precise about our types:
data Orange = ...
data Apple = ....
data Bag a where
OrangeBag :: [Orange] -> Bag [Orange]
AppleBag :: [Apple] -> Bag [Apple]
Now I can define a function which only works with bag of apples.
giveMeApples :: Bag [Apple] -> ...
GADTs allow you to have your types to contain more information about the values they represent. They do this by stretching Haskell data
declarations a little bit of the way to the inductive type families in a dependently typed language.
The quintessential example is typed Higher Order Abstract Syntax represented as a GADT.
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-} -- Not needed, just for convenience of (:@) below
module HOAS where
data Exp a where
Lam :: (Exp s -> Exp t) -> Exp (s -> t)
(:@) :: Exp (s -> t) -> Exp s -> Exp t
Con :: a -> Exp a
intp :: Exp a -> a
intp (Con a) = a
intp (Lam f) = intp . f . Con
intp (fun :@ arg) = intp fun (intp arg)
In this example, Exp
is a GADT. Note that the Con
constructor is very normal, but the App
and Lam
constructors introduce new type variables quite freely. These are existentially quantified type variables and they represent rather complex relationships between the different arguments to Lam
and App
.
In particular, they ensure that any Exp
can be interpreted as a well-typed Haskell expression. Without using GADTs we'd need to use sum types to represent the values in our terms and handle type errors.
>>> intp $ Con (+1) :@ Con 1
2
>>> Con (+1) :@ Con 'a'
<interactive>:1:11: Warning:
No instance for (Num Char) arising from a use of `+'
Possible fix: add an instance declaration for (Num Char)
In the first argument of `Con', namely `(+ 1)'
In the first argument of `App', namely `(Con (+ 1))'
In the expression: App (Con (+ 1)) (Con 'a')
>>> let konst = Lam $ \x -> Lam $ \y -> x
>>> :t konst
konst :: Exp (t -> s -> t)
>>> :t intp $ konst :@ Con "first"
intp $ konst :@ Con "first" :: s -> [Char]
>>> intp $ konst :@ Con "first" :@ Con "second"
"first"
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With