Search code examples
haskelltypestype-inferenceunification

Function with type a -> b in Haskell?


Is there any kind of function in Haskell that has type a -> b? That means, is it possible to write a function such that f :: a -> b? I don't think a function like that exists for the following reason: suppose that we found f where f :: a -> b, what would f 2 produce? a value of type b, but what is b since Haskell cannot infere (I think) it from the arguments I gave? Is this correct? Otherwise, can you give me an example of such a function?


Solution

  • Barring ⊥ (bottom valueundefined etc.), which is always possible but never useful, there can indeed be no such function. This is one of the simplest instances of the so-called free theorems that we get from polymorphic type signatures.

    You're on the right track with your intuitive explanation of why this is not possible, though it went off in the end. Yes, you can consider f (5 :: Int). The problem is not that the compiler “can't infer” what b would be – that would be the case for many realistic functions, e.g.

    fromIntegral :: (Num b, Integral a) => a -> b
    

    makes perfect sense; b will be inferred from the environment in which fromIntegral x is used. For instance, I might write

    average :: [Double] -> Double
    average l = sum l / fromIntegral (length l)
    

    In this case, length l :: a has the fixed type Int and fromIntegral (length l) :: b must have the fixed type Double to fit in the environment, and unlike in most other languages with type inference, information from the environment is available hereto in a Hindley-Milner based language.

    No, the problem with f :: a -> b is that you could instantiate a and b to any ridiculous combination of types, not just different number types. Because f is unconstrainedly polymorphic, it would have to be able to convert any type into any other type.

    In particular, it would be able to convert into the vacuous type Void.

    evil :: Int -> Void
    evil = f
    

    And then I could have

    muahar :: Void
    muahar = f 0
    

    But, by construction of Void, there cannot be a value of this type (save for ⊥ which you can't evaluate without either crashing or looping infinitely).


    It should be noted that this is by some standards not a very good way of computing the average.