Type of anonymous functions in Haskell

1
votes

I have a problem with typing anonymous functions in Haskell. For example when we have:

\x -> x 5

The type checked in GHCI is Num t1 => (t1 -> t2) -> t2 while I was sure it is the opposite.Similarly type

\x -> a * x

is Num a => a -> a (I know we need to assume that a is an Integer as the type of (*) is Int -> Int -> Int (without typeclasses).
Another example would be

\f -> f x

And as far as I checked is sth like (a -> b) -> b

But I am totally concerned about typing anonymous function. What is the magic power to understand this? Maybe a way to rewrite this function to a "normal" one to see the type clearly?

SO MY QUESTION IS: How do we get these types? Where they come from and how to evaluate this?

3
haskell
I can't understand what is the issue here, apart from a generic "I don't understand how type inference works", which is too broad. Can you be more specific? – chi
@chi an issue are basically these examples given, their evaluation of their types so the given results will be computed – heisenberg7584
@heisenberg7584 You've given the types right there. What specific problem are you having in understanding why those types are correct? Please edit your question to add this information. – AJF
Possible duplicate: What part of Hindley-Milner do you not understand?. If not a duplicate, talk about why. – Daniel Wagner
There's nothing special here about the functions being anonymous. func x = x 5 is the exact same function as your first one, and therefore has the same type. – Robin Zigmond

3 Answers

5
votes

>> How do we get these types ?

These types are what the Haskell system can deduce from the only thing it has, that is the definition given by the user, such as "x 5".

The important thing is not that the function is anonymous. It is that the function is not explicitely typed, so the Haskell system has to "guess" the type from the expression.

Prelude> let a=4
Prelude> :t  \x -> a * x
\x -> a * x :: Num a => a -> a
Prelude> 
Prelude> let f1 x = a*x
Prelude> :t f1
f1 :: Num a => a -> a
Prelude>

So, exactly same type for anonymous and named versions.

Of course, you can be more specific:

Prelude> let f4 :: Double -> Double ; f4 x = 4*x
Prelude> :t f4
f4 :: Double -> Double
Prelude>

Haskell does not force you to explicitly type everything. It takes all explicit typing info (such as for f4), and implicit typing info produced by your definitions and your calls to library functions, as typing constraints.

If the constraints can be resolved unambiguously, fine; that's called type inference as mentioned by chi above. Otherwise, if the typing constraints are contradictory or ambiguous, execution aborts.

2
votes

The following are three equivalent ways to write your first function:

f :: Num t1 => (t1 -> t2) -> t2
f = \x -> x 5

g :: Num t1 => (t1 -> t2) -> t2
g x = x 5

h :: Num t1 => (t1 -> t2) -> t2
h = ($ 5)

Note that this function, no matter which syntax you use in its definition, is a second-order function. That means that its argument, x, is itself a function. That is, x must have a type of the form x :: Constraint1 t1, Constraint2 t2 => t1 -> t2. More specifically, x must accept 5 as its first (and possibly only) argument. But that's the only inherent constraint on its argument. 5 :: Num t1 => t1, so x :: Num t1, Constraint2 t2 => t1 -> t2. There is no inherent constraint on the return value of x, so the most general (permissive) type is x :: Num t1 => t1 -> t2.

So that gives us the type for the argument of your function: \x -> x 5 :: Num t1 => (t1 -> t2) -> ?. But what about the return type? Well, your function just applies x to 5 and evaluates to (returns) the result, so your function returns the same type as x. Assuming your function can accept any possible function x, its type is thus \x -> x 5 :: Num t1 => (t1 -> t2) -> t2.

Note also that you can use any lowercase names you want, both for the parameter and the type variables. Thus you could just as well have written \function -> function 5 :: Num five => (five -> result) -> result.

0
votes

I think you are complicating it in a way you don't have to. Basically when you have an anonymous function in Haskell and want to find type of it you need to find two types: first the one that is before -> symbol and then the type of whole expression on the right of the arrow ->. Base on your example:

\x -> x 5

We need to find the type of x which we know is a function that has one argument of some type belonging to the typeclass Num, and returns some unknown type - let's say t:

x :: Num a => a -> t

So x function returns something of type t:

x 5 :: t

And here's our answer:

\x -> x 5 :: Num a => (a -> t) -> t

The same situation is with the last one:

\f -> f x

f is again some function but this time we don't know the type of its argument

f :: a -> b

so a is type of x and the whole expression on the right returns b

f x :: b

And again - here it is, we have a type of the expression on the left of -> and on the right.

\f -> f x :: (a -> b) -> b