Function with type a -> b in Haskell?

2019-07-19 04:36发布

问题:

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?

回答1:

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.



回答2:

In order to implement f :: a -> b, it means that f has to be able to return any possible type. Even types that don't exist today, but somebody could define in ten years' time. Without some kind of reflection feature, that's obviously impossible.

Well... "impossible" is a big word... As the other answers point out, it's impossible excluding bottom. In other words, f can never return a value of type b. It can throw an exception, or loop forever. But (arguably) neither of those things is really "returning a value".

f1 :: a -> b
f1 = error "f1"

f2 :: a -> b
f2 s = error "f2"

f3 :: a -> b
f3 x = f3 x

These functions are all subtly different, and they all compile just fine. And, of course, they're all useless! So yes, there is no useful function with type a -> b.

If you want to split hairs:

  • f1 throws an exception.
  • f1 'x' throws an exception.
  • f2 is a normal-looking function.
  • f2 'x' throws an exception.
  • f3 is a normal-looking function.
  • f3 'x' doesn't throw an exception, but it loops forever, so it never actually returns anything.

Basically any function you see that returns "any type" is a function that never actually returns. We can see this in unusual monads. For example:

f4 :: a -> Maybe b

It is perfectly possible to implement this function without throwing an exception or looping forever.

f4 x = Nothing

Again, we're not actually returning a b. We could similarly do

f5 :: a -> [b]
f5 x = []

f6 :: a -> Either String b
f6 x = Left "Not here"

f7 :: a -> Parser b
f7 x = fail "Not here"


回答3:

There is, I think, exactly one, but it is cheating a little bit:

> let f _ = undefined
> :t f
f:: t -> t1

This only exists because bottom is considered a value of every type.



回答4:

... but what is b since Haskell cannot infer it from the arguments I gave?

Depending on the context, Haskell can infer the return type; say:

{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

class Cast a b where
    cast :: a -> b

instance Cast a a where
    cast = id

instance Cast Int String where
    cast = show

instance Cast Int Double where
    cast = fromIntegral

then,

cast :: Cast a b => a -> b

and if given enough context, Haskell knows which function to use:

\> let a = 42 :: Int
\> let b = 100.0 :: Double

\> "string: " ++ cast a  -- Int -> String
"string: 42"

\> b * cast a            -- Int -> Double
4200.0