What the heck is Typeable !?


I used to find the Typeable typeclass in Haskell particularly confusing and even more, pointless. Pointless because, we are talking about a statically typed language where all the types are known at compile time. What is the point of having a separate Typeable typeclass when everything is already "Typeable"!

Even though Haskell is statically typed, and types are known at compile time, Haskell allows sections of code where values can be polymorphic, and when writing Haskell code, quite often we find ourselves dealing with values of unknown types. With that in mind, let us see what Typeable makes it possible with in the Haskell's type system.

Consider the following snippet with a polymorphic function fn.


  module Main where
  -- -
  strLen :: String -> Int
  strLen x = length x
  -- -
  fn :: a -> Int
  fn m = strLen m  -- <- Type errorrrr!
  -- -
  main :: IO ()
  main = putStrLn $ show $ fn "string who's length ll be printed"

Warning: The above code is non-sensical. There is no reason for the argument of fn to be polymorphic. It is just meant to show what Typeable can do, and not to show how it can be useful.

This won't type check. Even though we are calling fn with a string argument, there is nothing in the type signature of fn that guarantees that the first argument will be always a String. So long as there is no such guarantee, GHC won't allow to pass that argument to a function that always requires it to be a String. Thus the type error.

Normally, there is no way you can convince the compiler that m is, in fact, a String, rightly so. I mean, a simple type annotation like this won't work, either.


  module Main where
  -- -
  strLen :: String -> Int
  strLen x = length x
  -- -
  fn :: a -> Int
  fn m = strLen (m :: String)  -- • Couldn't match expected type ‘String’ with actual type ‘a’
  -- -
  main :: IO ()
  main = putStrLn $ show $ fn "string who's length ll be printed"

Now, let us make a typeclass that enables us to ask a value what type it really is.


  module Main where
  -- -
  strLen :: String -> Int
  strLen x = length x
  -- -
  class WhatAreYou a where
    whatAreYou :: a -> String
  -- -
  instance WhatAreYou String where
    whatAreYou _ = "String"
  -- -
  instance WhatAreYou Int where
    whatAreYou _ = "Int"
  -- -
  fn :: (WhatAreYou a) => a -> Int
  fn m = case whatAreYou m of
      "String" -> strLen m  -- We get the same error here where ghc couldn't match expected type ‘String’ with actual type ‘a’
      _ -> error "Not a string"
  -- -
  main :: IO ()
  main = putStrLn $ show $ fn "string who's length ll be printed"

With this type class, it appears that we have enough stuff in place to dynamically check the type of a polymorphic value. But even though it appears enough for the programmer, it is not enough to convince the compiler, simply because GHC cannot trust arbitrary user defined functions to do the right thing, and it is not smart (or dumb, depending on how you want to look at it) enough to look into functions and infer what they are doing.

And for these reasons, the type error stays lit.

Enter Typeable

Typeable is a built in typeclass, similar to the WhatAreYou typeclass we saw above. It is similar to WhatAreYou in the sense that it encodes the type information in the typeclass instances, that can be queried at run time. In the GHCI session below you can see how the typeOf function returns the actual type of the value that is passed to it.


  > typeOf 10
  Integer
  > typeOf (10 ::Float)
  Float
  > typeOf "Abc"
  [Char]

But unlike WhatAreYou typeclass, the GHC trusts the Typeable instances (which GHC derives automatically for all types and does not allows user to implement them, hence the trust). Thus, we can use it to convince GHC that the polymorphic value m in the above example is indeed a String. We use the cast function from the Data.Typeable module to do that in the snippet below.


  module Main where
  -- -
  import Data.Typeable (cast, Typeable)
  -- -
  strLen :: String -> Int
  strLen x = length x
  -- -
  fn :: (Typeable a) => a -> Int
  fn m =
    case (cast m :: Maybe String) of
      Just mi -> strLen mi -- --> In this branch of the case statement, GHC will consider `mi` to be String,
                           --     and this whole program becomes well typed.
      Nothing -> error "Not a string"
  -- -
  main :: IO ()
  main = putStrLn $ show $ fn "string who's length ll be printed"

The magic happens with the cast function, from Data.Typeable module. It's signature is,


  cast :: (Typeable a, Typeable b) => a -> Maybe b

As we can see from the type signature, cast function deals with a source type, and a target type, both expected to have an instance of Typeable. In the above code, the cast function uses the Typeable instance to check that a is indeed a String value and indicate the result using a Maybe value. If it finds that a is indeed a String, we get a Just String type in return. Otherwise we get Nothing. What this means that we have converted a polymorphic type into a concrete type, which GHC will accept as a concrete type in the Just branch of the case statement. And that is why we were able to call the strLen function with mi as an argument, because at that point GHC has accepted that mi is a String.

Typeclass dictionaries and how they are attached to values at run time.

You might be wondering how a typeclass is able to persist information regarding a type, at run time, when all type information has been erased from the values. I will just refer to this post which I think does a good job explaining how typeclasses really work in Haskell, and thus answering this question as well.

Use cases that might make a little more sense.

Warning: Following cases are not trying to suggest the use of Typeable in similar situations.

To easily follow these examples some amount of familiarity with data type promotion, Data.Proxy and DataKinds extension is required.

Serializing type level currency

Imagine that you are implementing some software that deals with money in different currencies. In order to prevent mixing up money values in different currencies, you decide to put the currency in the type system. So you enable DataKinds extension and do something like this.


  data Currency = INR | USD | AUD | YEN
  data Money (currency :: Currency) = Money Int -- Hurray! We have currency in type!

Now, at some point, you have to display the money value, along with the currency, to the user. So you set out to implement Show instances for the Money type. But since we have currency only in type level, and not as a field in the Money value, it will appear that we should implement Show instance for each and every currency we want to support. It feels quite tedious and error prone. But with typeable, you will be able to do something like the following, and can get away with only having to implementing a single instance.


  instance Show (Money currency) where
    show (Money a) =
      (show a) ++
      (show $ typeOf (Proxy :: Proxy currency))

Bring back types hidden behind existentially quantified constructors

Let us continue the example from above. Say you find yourselves having to read a bunch of money values from a file. One problem with that is that the money values can have different currencies. Since your money type is having the currency in type level, you cannot read all of them into a list. Because all elements of a list needs to be of same type.

To solve this, you wrap the Money values in a wrapper type, that does not have currency as a type parameter. We use an existential quantifier to do this.


  data MoneyEx = forall x. MoneyEx (Money x)

Now you can read mixed currency into a list of MoneyEx. But now there is yet another problem. Say, you want to add two money values from the list and the function to add two money values have the signature


  moneyAdd :: Money c -> Money c -> Money c
  moneyAdd (Money a) (Money b) = Money (a + b)

Because right now, we only want to add money values that have same currency.

Since we have a list of MoneyEx values, we proceed to write a function to add two MoneyEx values.


  moneyExAdd :: MoneyEx -> MoneyEx -> MoneyEx
  moneyExAdd (MoneyEx a) (MoneyEx b) = MoneyEx $ moneyAdd a b

And GHC screams at you with something like...

      Expected type: Money x
        Actual type: Money x1

This actually means that GHC have no way of knowing that a and b (in the function body) have the same currency, but the call to moneyAdd demands them to be. Hence the type error.

We can solve this by adding a Typeable constraint to the data definition of MoneyEx and using cast function as follows.


  data MoneyEx = forall x. (Typeable x) => MoneyEx (Money x)
  -- -
  moneyExAdd :: MoneyEx -> MoneyEx -> MoneyEx
  moneyExAdd (MoneyEx a) (MoneyEx b) = case cast a of
    Just a1 -> MoneyEx $ moneyAdd a1 b
    Nothing -> error ""

Some of you might be thinking now. What is the point of the type if you are going to have to do run time checks and throw errors during run time. Well, I think the point is GHC prevented you from adding two money values of with possibly different currencies, and you were forced to prove ghc that a run time check is done, before the Money values are added. As I see it, that is a net win and what we originally wanted to accomplish with the currency in type level anyway!

Data.Dynamic

In the earlier example, we defined MoneyEx as


  data MoneyEx = forall x. (Typeable x) => MoneyEx (Money x)

The Dynamic from Data.Dynamic is a built in type that you can use for this purpose. So if you ever find yourselves in a situation where you want to smuggle some types without GHC noticing, you don't have to define a new data type. You can just use the Dynamic type. (Thanks to 'hexagoxel' in #haskell for pointing this out). So if you find the stuff in this post interesting, you should definitely proceed to documentation of Data.Dynamic and give it a look.

© 2018-08-01 Sandeep.C.R <sandeepcr2@gmail.com>