Defeating Return Type Polymorphism

Introduction

"Make illegal states unrepresentable!" is the war cry of any programmer practicing type-driven design.¹ If the compiler can verify that most state configurations our program can run into are correct, we have a much higher certainty that our executable will not behave in unexpected ways. As Haskell programmers, we have a fairly advanced type system at our fingertips that allows us to realize this principle effectively. I would argue that it is powerful enough to not just make illegal states unrepresentable but to actively get the compiler to help us figure out not just what is “legal” but what is “correct”.

However, one aspect of this type-system that always confused me greatly was return type polymorphism. How can I model my problems correctly when the call site decides how a polymorphic type should be resolved? Does this lead to problems? If it does, can we get around it? In this post, I want to delve into what return type polymorphism is and what kind of problems it can create for us. Then I will cover generalized algebraic data types (GADTs) and existential quantification and how to use both concepts to effectively circumvent return type polymorphism while still retaining type-safety.

Return Type Polymorphism

Let’s first take a quick look at parametric polymorphism and return type polymorphism. As we know, we can define Haskell functions with universally quantified type variables. These variables are parameters for types that need to be refined to a concrete type for the function (or term) to make sense in our program.

Here is an example:

first :: (a -> b) -> (a, c) -> (b, c)
first f (x, y) = (f x, y)

A notable property of this function is that some universally quantified variables occur in the return type of the function. What happens when this function is used in an expression where these types are already known?

(1 :: Int) + fst (first f t)

What is the type of f in this case? That’s where Haskell’s type inference kicks in. As we know that (+) is of type Num a => a -> a -> a, we know that the result of fst has to be Int (since the first argument of (+) is fixed as an Int). Therefore, the return type of first f t has to be (Int, a) and since the type of first is (a -> b) -> (a, c) -> (b, c), we know that the type of the function f is (a -> Int). Note that type variables a can be different for each term.

See what happened here? The caller of the function decides what kind of type it needs to return and by extension, it also decides what types the arguments should be. This is return type polymorphism!

Ad-hoc Polymorphism

Why is this helpful? Using type classes, we can use this to implement ad-hoc polymorphism, using different implementations based on the used types in a certain context. In other words, we can map types to terms. Let’s look at the read function as an example.

read :: Read a => String -> a

This function is used to parse a String into another Haskell value. It has a polymorphic return type, which is constrained by Read a meaning that an instance of the Read type class has to exist for a specific a we want to use read on.

ghci> read "1" :: Int
1
ghci> read "1" :: Float
1.0
ghci> read "1" :: Bool
*** Exception: Prelude.read: no parse

But how does Haskell know how to parse the value? Since the caller decides the type to be used it also decides which type class instance to use! Therefore, the caller decides which function decides the parsing.

Wait, what? The caller decides? How does the caller know what is being parsed? Well, they don’t always know… And that’s a problem.

Missing Function Autonomy

Imagine we want to parse an image file of some imaginary format that specifies the pixel bit depth in its header. The pixels are either encoded with 8 or 16 bits. Here is how we could model the type for our images.

import Data.Word

data Pixel8Bit = Pixel8Bit Word8 Word8 Word8

data Pixel16Bit = Pixel16Bit Word16 Word16 Word16

data Image = Image
  { width :: Int,
    height :: Int,
    pixels :: Either [Pixel8Bit] [Pixel16Bit]
  }

This is fine, but not entirely practical. Imagine if there were many more bit depths or encodings, such that a simple Either wouldn’t work anymore and we needed a custom sum type that was able to hold our different types of pixels.

data ArbitraryPixels
  = Pixels8Bit [Pixel8Bit]
  | Pixels16Bit [Pixel16Bit]
  ...

data Image = Image
  { width :: Int,
    height :: Int,
    pixels :: ArbitraryPixels
  }

Every time we want to work with our pixels we would need to perform a match on the constructors, so working with the pixel data is not generic. Since the type is not parametrized over the pixel type it is impossible to write polymorphic functions for it or to declare functionality for single pixel types.

So let’s fix this by parametrizing the Image type. Here is what this would look like:

data Image px = Image
  { width :: Int,
    height :: Int,
    pixels :: [px]
  }

So far, so good. Let’s say we want to write a function that parses said image format. The function’s signature for that might look like this:

parseImage :: ByteString -> Either String (Image px)

Since this function features return type polymorphism, we have to deal with a problem. The caller cannot know what the type of px is. Nevertheless, when calling the parseImage function the caller needs to decide the type of px, but that type should be decided by the parse function itself. How do we rectify this? One possibility on how to still perform this would be to call the function with one type and if parsing fails, just call it with the other type. That way, the information about the bit width gathered by the parseImage function is passed down to the caller.

parseAnyImage :: ByteString -> Either String (Either (Image Pixel8Bit) (Image Pixel16Bit))
parseAnyImage bs =
  case parseImage bs of
    Right (image8bit :: Image Pixel8Bit) -> Right $ Left image8bit
    Left msg1 ->
      case parseImage bs of
        Right (image16bit :: Image Pixel16Bit) -> Right $ Right image16bit
        Left msg2 -> Left $ "Failed to parse: " <> msg1 <> "\n" <> msg2

However, as we have already covered, this solution is highly impractical, not just because of the performance considerations of running a full parse twice. If we want to add more types of pixels we will have to copy and change a lot of code.

Maybe, adding the type parameter wasn’t that clever after all. Can we roll that back? Let’s try this by removing the type variable from our type and adding constructors for the different kinds of pixels. The type then might look like this:

data Image
  = Image8Bit
      { width :: Int,
        height :: Int,
        pixels :: [Pixel8Bit]
      }
  | Image16Bit
      { width :: Int,
        height :: Int,
        pixels :: [Pixel16Bit]
      }

Sadly, this type is impossible as the type of pixels cannot be [Pixel8Bit] and [Pixel16Bit] simultaneously. Not even removing the record syntax fixes the problem, as constructing a function to retrieve the pixel data from the image is impossible as it would need to return different types based on the image’s constructor.

One way of solving it would be to create a type to construct pixels of arbitrary bit depth and then use that in the image type. But wait… We already did that…

We somehow need to be able to parametrize the Image type but allow the parse function to set a fixed type parameter. But how is that possible? If we are really trying to “make illegal states unrepresentable” we need to be more creative.

Refining types with GADTs

Let’s analyze our problem. The caller has no way of deciding the type of the parse function before parsing has happened, so its type should be polymorphic. However, when we want to work with the parsing result we need a way of refining the type. That means taking the polymorphic type (Image px) and somehow resolving the type to something more concrete (e.g. Image Pixel8Bit).

Is something like this even possible in Haskell? As it turns out, there is a concept that does exactly that!

Generalized Algebraic Data Types

Let’s take a look at a fascinating concept: Generalized Algebraic Data Types (GADTs). As their name suggests they are an extension to normal ADTs. We can enable them with one language extension pragma.

{-# LANGUAGE GADTs #-}

Now we can write GADTs with a new kind of syntax. The following definitions for an ADT and GADT are equivalent.

data MyADT a
  = AdtCons1 Int Float String
  | AdtCons2 Bool a

data MyGADT a where
  GadtCons1 :: Int -> Float -> String -> MyGADT a
  GadtCons2 :: Bool -> a -> MyGADT a

As we can see, they behave exactly the same.

ghci> :t AdtCons1 1 1.0 "Hi!"
AdtCons1 1 1.0 "Hi!" :: MyADT a
ghci> :t AdtCons2 True (1 :: Int)
AdtCons2 True (1 :: Int) :: MyADT Int
ghci> :t GadtCons1 1 1.0 "Hi!"
GadtCons1 1 1.0 "Hi!" :: MyGADT a
ghci> :t GadtCons2 True (1 :: Int)
GadtCons2 True (1 :: Int) :: MyGADT Int

We can also match on the constructors of a GADT, just like with ADTs. However, what is the meaning of ending the definitions with MyGADT a? Isn’t that redundant?

The answer is no, as this is the big difference between ADTs and GADTs. While the ADT will always be MyAdt a, no matter the constructor, the GADT is allowed to change its type freely based on the used constructor. This allows for a definition like this.

data MyGADT a where
  GadtCons1 :: Int -> Float -> String -> MyGADT Bool
  GadtCons2 :: Bool -> a -> MyGADT String

Now, the constructor decides what a will be.

ghci> :t GadtCons1 1 1.0 "Hi!"
GadtCons1 1 1.0 "Hi!" :: MyGADT Bool
ghci> :t GadtCons2 True (1 :: Int)
GadtCons2 True (1 :: Int) :: MyGADT [Char]

How is this helpful? Well, it allows for a definition like this.

data GiveMe a where
  SomeString :: GiveMe String
  SomeInt :: GiveMe Int

giveMe :: GiveMe a -> a
giveMe SomeString = "Hello"
giveMe SomeInt = 1

The definition for giveMe is completely legal, even though it returns different types based on the matched constructor. This is possible because of the type of GiveMe. Since SomeString is of type GiveMe String that means that giveMe SomeString must be of type String, as the a of GiveMe a is replaced by the String from GiveMe String. Haskell is smart enough to statically figure out the needed type based on the matched constructor. That’s why the definition type checks and works as expected.

ghci> giveMe SomeString
"Hello"
ghci> giveMe SomeInt
1

Another classic example for GADTs is the encoding of type safe domain specific languages, representing the syntax tree as a GADT. This example is explained here and here. For us, it’s important to realize and learn that while type classes can be used to map types to terms, GADTs are able to map terms to types.

Example: Requests & Responses

As another example: We can encode requests and responses as GADTs. Let’s say we have a general function that processes requests to generate responses for some kind of service. The function might look like this:

processRequest :: Request -> Response

Let’s say we want to process different kinds of requests and get fitting responses for them, meaning we want to get an HTTP response from an HTTP request and we want to get an FTP response from an FTP request. Using simple ADTs, we could theoretically return an FTP response on an HTTP request, which makes no sense.

However, we can model this correctly with a GADT:

data HttpRequest = ...

data HttpResponse = ...

data FtpRequest = ...

data FtpResponse = ...

...

data RequestWithResponse response where
  Http :: HttpRequest -> RequestWithResponse HttpResponse
  Ftp :: FtpRequest -> RequestWithResponse FtpResponse
  ...

Now our function becomes parametrized over the polymorphic type of RequestWithResponse, which determines the request with its constructor and the response with its polymorphic type.

processRequest :: RequestWithResponse response -> response

Inside the function, we can match on the request type and produce fitting responses, all while retaining full type safety. The great thing is that adding another constructor to the RequestWithResponse type will produce compiler warnings on unmatched constructors, letting us know where we need to add more case distinctions.

Working with GADTs

Now we can remodel our image type as a GADT. In essence, we are creating the same ADT as before but we explicitly set the pixel type, depending on what kind of pixels we are using. We are still not allowed to use record syntax for the same reason explored earlier. However, we now can create the function to retrieve pixels from an image.

data Image px where
  Image8Bit :: Int -> Int -> [Pixel8Bit] -> Image Pixel8Bit
  Image16Bit :: Int -> Int -> [Pixel16Bit] -> Image Pixel16Bit

width :: Image px -> Int
width (Image8Bit w _ _) = w
width (Image16Bit w _ _) = w

height :: Image px -> Int
height (Image8Bit _ h _) = h
height (Image16Bit _ h _) = h

pixels :: Image px -> [px]
pixels (Image8Bit _ _ pxs) = pxs
pixels (Image16Bit _ _ pxs) = pxs

This function would have been impossible with a simple ADT. The reason this works is that matching on a GADT’s constructor refines its polymorphic type. That is exactly, what we wanted to achieve with our parsing function. It can return a polymorphic Image px and give the caller a chance to refine that px by matching on the constructor.

So the parsing function might look like this:

parseImage :: ByteString -> Either String (Image px)
parseImage bs =
  let width = ...
      height = ...
   in if ...
        then
          let pixels = ...
           in Right $ Image8Bit width height pixels
        else
          let pixels = ...
            in Right $ Image16Bit width height pixels

But sadly, this still does not work, because of our arch enemy: Return type polymorphism. The caller still decides what the type of px should be, so the then and else branches are not valid as they have a type that might be different from the rigid type variable px. How can we fix this issue?

Existential Quantification

At the end of the day, our problem comes from the type variable px in the return type. What we need is to get rid of it. This means that we need a new type that can encode our Image type but hide away any type variable.

An ace up a Haskeller’s sleeve when it comes to this problem is another language extension called ExistentialQuantification, which might be one of my favorite extensions to Haskell’s type system. Let’s take a look at it!

Heterogenous Data

When a file has the language extension turned on, the forall keyword in a data type is allowed to be introduced on the right side of a definition. This means that we can introduce a new data type that is not parametrically polymorphic but still has polymorphism for its constructor.

{-# LANGUAGE ExistentialQuantification #-}

data SomeData = forall a. SomeData a

What can we do with this?

ghci> :t SomeData (1 :: Int)
SomeData (1 :: Int) :: SomeData
ghci> :t SomeData (True :: Bool)
SomeData (True :: Bool) :: SomeData

As we can see no matter what we put into the constructor we get the same type each time. It is always SomeData! So could we build a list of SomeData?

ghci> :t [SomeData (1 :: Int), SomeData (True :: Bool)]
[SomeData (1 :: Int), SomeData (True :: Bool)] :: [SomeData]

Here, we created a heterogenous list!² We can freely put values into our constructor and chuck them into the list (or any other polymorphic data structure) without causing any type errors. But now we have a problem. How do we access values in our SomeData constructor? We have effectively lost all type information once a value is wrapped inside it.

The solution is to retain information on the type by using a constrained type variable in the data type definition.

data ShowData = forall a. (Show a) => ShowMe a

instance Show ShowData where
  show (ShowMe x) = show x

Forgive me for using an illegal instance for Show ShowData here, but I want to demonstrate the power of existential quantification.³ Here, the possible values we can put into the ShowMe constructor are being constrained by the type constraint Show. That’s why the instance Show ShowData can be defined. We match on the constructor of ShowData and we can call show on its argument since we know that no matter what x is, its type must satisfy the Show constraint.

ghci> [ShowMe (1 :: Int), ShowMe (True :: Bool), ShowMe ((1, "Hello") :: (Int, String))]
[1,True,(1,"Hello")]

Encoding arbitrary values

We can now use this technique to fix our problem. Our parse function should not return an Image px but some new type with existential quantification. That might look like this:

data AnyImage = forall px. AnyImage (Image px)

Don’t we need a type constraint here? No! As we have established, matching on a GADT’s constructors refines its type. So by wrapping our GADT inside an existentially quantified type, we can return a value that is not decided by return type polymorphism and still allows the caller to have access to the correct type information.

Our parseImage function now looks like this.

parseImage :: ByteString -> Either String AnyImage
parseImage bs =
  let width = ...
      height = ...
   in if ...
        then
          let pixels = ...
           in Right . AnyImage $ Image8Bit width height pixels
        else
          let pixels = ...
            in Right . AnyImage $ Image16Bit width height pixels

Note that the type of pixels is statically checked based on the constructor we are using. That means that we cannot use Pixel16Bit with the Image8Bit constructor without getting an appropriate type error.

If we now want to use the result of this function we can do that like so:

something :: ByteString -> ...
something bs =
  let img = parseImage bs
   in case img of
        Right (AnyImage (Image8Bit _ _ pxs)) -> ... -- pxs is of type [Pixel8Bit]
        Right (AnyImage (Image16Bit _ _ pxs)) -> ... -- pxs is of type [Pixel16Bit]
        Left msg -> ...

The magic is in the case matching. Based on the constructor, the type of pxs is determined and refined! The caller does not determine the type anymore, it is determined by whatever the parsing function produced. Even better: If we extend the Image type by more constructors, the compiler will correctly warn us of non-exhaustive matches. This enables us to program in a way, that would be impossible in dynamic programming languages, as our AnyImage type can be considered a restricted dynamic value. It is dynamic in its polymorphic type, but only as far as the Image type allows.

Conclusion

We have successfully, transparently and safely bypassed return type polymorphism in Haskell, using the following technique: First, we define a GADT as our polymorphic type. This GADT is then wrapped inside an existentially quantified type to remove the polymorphic return type from functions returning said GADT. Since matching on a GADT’s constructors refines type information we can effectively pass dynamic types from function to function and retrieve the actual type information at the call site.

This technique can be used in any Haskell program. It can be used whenever you need to ensure that a function can decide which data must be returned from it. This is helpful for parsing data that possibly has no static form, data validation and communication with external sources, just to name a few.

If anything, this post aims to highlight that Haskell’s very strict type system is not as rigid as it might seem at first. As Haskellers, we have a multitude of techniques and opportunities to solve problems practically, without the need to sacrifice type safety.