Whole Haskell Use of GADTs

For some reason GADTs are a particular sticking point for many advocates of Simple Haskell. But sometimes GADTs are the natural form of expressing a concept.

By way of example, here’s a snippet of API I’ve borrowed from JuicyPixels:

data Image a = Image {
    imageWidth :: !Int,
    imageHeight :: !Int,
    imageData :: Vector (PixelBaseComponent a)
    }

data DynamicImage =
    ImageY8 (Image Pixel8) |
    ImageY16 (Image Pixel16) |
    ImageY32 (Image Pixel32) |
    ImageYF (Image PixelF) |
    ImageYA8 (Image PixelYA8) |
    ImageYA16 (Image PixelYA16) |
    ImageRGB8 (Image PixelRGB8) |
    ImageRGB16 (Image PixelRGB16) |
    ImageRGBF (Image PixelRGBF) |
    ImageRGBA8 (Image PixelRGBA8) |
    ImageRGBA16 (Image PixelRGBA16) |
    ImageYCbCr8 (Image PixelYCbCr8) |
    ImageCMYK8 (Image PixelCMYK8) |
    ImageCMYK16 (Image PixelCMYK16)

promoteImage :: ColorConvertible a b => Image a -> Image b 

JuicyPixels was originally released in 2012, and there’s always a good presumption against changing an API, so we can’t blame the developers for not making use of GADTs. But if we were starting a project like this from scratch today, how would we write such code, using the whole language?

The way DynamicImage has been defined makes it a bit difficult to work with. For example, if you want to get the width or height of a dynamic image, you’ll have to write cases for each constructor. And the convertibility from one pixel type to another is encoded at the type level (with ColorConvertible), but there’s no clean way to do it at the value level, if we wanted to provide that functionality dynamically.

We can make this code more expressive, and more elegant, by using a GADT that represents the pixel type of a dynamic image:

data PixelType a where
    PixelType8 :: PixelType Pixel8
    PixelType16 :: PixelType Pixel16
    PixelType32 :: PixelType Pixel32
    PixelTypeF :: PixelType PixelF
    PixelTypeYA8 :: PixelType PixelYA8
    PixelTypeYA16 :: PixelType PixelYA16
    PixelTypeRGB8 :: PixelType PixelRGB8
    PixelTypeRGB16 :: PixelType PixelRGB16
    PixelTypeRGBF :: PixelType PixelRGBF
    PixelTypeRGBA8 :: PixelType PixelRGBA8
    PixelTypeRGBA16 :: PixelType PixelRGBA16
    PixelTypeYCbCr8 :: PixelType PixelYCbCr8
    PixelTypeCMYK8 :: PixelType PixelCMYK8
    PixelTypeCMYK16 :: PixelType PixelCMYK16

data DynamicImage = forall a. DynamicImage (PixelType a) (Image a)

Any code to get properties of the contained Image is now much simpler:

dynamicImageSize :: DynamicImage -> (Int, Int)
dynamicImageSize (DynamicImage _ img) = (imageWidth img, imageHeight img)

We can also express convertibility dynamically, if we want to add that:

canPromotePixel :: PixelType a -> PixelType b -> Maybe (Dict (ColorConvertible a b))
-- provided as appropriate

promoteDynamicImage :: DynamicImage -> PixelType b -> Maybe (Image b)
promoteDynamicImage (DynamicImage pta img) ptb = do
    Dict <- canPromotePixel pta ptb
    return $ promoteImage img

You can see how with Haskell’s fancy shiny GADT feature, the code is now more expressive, and easier to understand for anyone who knows the language.

GADTs are actually not a particularly difficult concept to learn, for someone who already understands rank-n types and existential quantification. And in many situations, they provide a huge benefit in expressibility.

— Ashley Yakeley

Leave a Reply