Writing A Function Polymorphic In A Type Family

Question

I was experimenting with type families yesterday and ran into an obstacle with the following code:

  {-# LANGUAGE TypeFamilies #-}

  class C a where
      type A a
      myLength :: A a -> Int

  instance C String where
      type A String = [String]
      myLength = length

  instance C Int where
      type A Int = [Int]
      myLength = length

  main = let a1 = [1,2,3]
             a2 = ["hello","world"]
         in print (myLength a1)
            >> print (myLength a2)

Here I have a type associated with class C and a function that calculates the length of the associated type. However the above code gives me this error:

 /tmp/type-families.hs:18:30:
     Couldn't match type `A a1' with `[a]'
     In the first argument of `myLength', namely `a1'
     In the first argument of `print', namely `(myLength a1)'
     In the first argument of `(>>)', namely `print (myLength a1)'
 /tmp/type-families.hs:19:30:
     Couldn't match type `A a2' with `[[Char]]'
     In the first argument of `myLength', namely `a2'
     In the first argument of `print', namely `(myLength a2)'
     In the second argument of `(>>)', namely `print (myLength a2)'
 Failed, modules loaded: none.

If, however I change "type" to "data" the code compiles and works:

  {-# LANGUAGE TypeFamilies #-}

  class C a where
      data A a
      myLength :: A a -> Int

  instance C String where
      data A String = S [String]
      myLength (S a) = length a

  instance C Int where
      data A Int = I [Int]
      myLength (I a) = length a

  main = let a1 = I [1,2,3]
             a2 = S ["hello","world"]
             in
               print (myLength a1) >>
               print (myLength a2)

Why does "length" not work as expected in the first case? The lines "type A String ..." and "type A Int ..." specify that the type "A a" is a list so myLength should have the following types respectively : "myLength :: [String] -> Int" or "myLength :: [Int] -> Int".

Answer 1

Hm. Let's forget about types for a moment.

Let's say you have two functions:

import qualified Data.IntMap as IM

a :: Int -> Float
a x = fromInteger (x * x) / 2

l :: Int -> String
l x = fromMaybe "" $ IM.lookup x im
  where im = IM.fromList -- etc...

Say there exists some value n :: Int that you care about. Given only the value of a n, how do you find the value of l n? You don't, of course.

How is this relevant? Well, the type of myLength is A a -> Int, where A a is the result of applying the "type function" A to some type a. However, myLength being part of a type class, the class parameter a is used to select which implementation of myLength to use. So, given a value of some specific type B, applying myLength to it gives a type of B -> Int, where B ~ A a and you need to know the a in order to look up the implementation of myLength. Given only the value of A a, how do you find the value of a? You don't, of course.

You could reasonably object that in your code here, the function A is invertible, unlike the a function in my earlier example. This is true, but the compiler can't do anything with that because of the open world assumption where type classes are involved; your module could, in theory, be imported by another module that defines its own instance, e.g.:

instance C Bool where
    type A Bool = [String]

Silly? Yes. Valid code? Also yes.

In many cases, the use of constructors in Haskell serves to create trivially injective functions: The constructor introduces a new entity that is defined only and uniquely by the arguments it's given, making it simple to recover the original values. This is precisely the difference between the two versions of your code; the data family makes the type function invertible by defining a new, distinct type for each argument.