2

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?

heisenberg7584
  • 563
  • 2
  • 10
  • 30
  • 4
    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 May 21 '19 at 15:23
  • @chi an issue are basically these examples given, their evaluation of their types so the given results will be computed – heisenberg7584 May 21 '19 at 15:25
  • 1
    @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 May 21 '19 at 15:29
  • @AJFarmar edit done – heisenberg7584 May 21 '19 at 15:31
  • 1
    Possible duplicate: [What part of Hindley-Milner do you not understand?](https://stackoverflow.com/q/12532552/791604). If not a duplicate, talk about why. – Daniel Wagner May 21 '19 at 15:32
  • 2
    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 May 21 '19 at 15:47
  • And that function takes its argument and applies it to 5, so that argument must be a function that takes a number, and then the overall function returns that function argument's return type. This is perfectly logical, and exactly what the type signature tells you - so please explain further which part you are struggling to understand. – Robin Zigmond May 21 '19 at 15:49

3 Answers3

5

>> 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.

jpmarinier
  • 4,427
  • 1
  • 10
  • 23
  • Okey, it helps a lot... But what if we have an expression like; `\x -> f x y`. As I understand this is the same as func x = x y right ? How can we type this one when y is not even an argument here... – heisenberg7584 May 22 '19 at 17:26
  • @heisenberg7584 Correct, the system refuses to give a type for \x -> f x y until you have defined f and y. In theory, maybe it could say something like (f:: t1->t2->t3) => t1-> t3 but cannot be bothered. Better safe than sorry I guess. – jpmarinier May 22 '19 at 19:06
  • 1
    so sorry, just last one. So am I right that when we have \y -> x + y the type is `Num a => a -> a` because on the left side of expression there is just y so as an x we put some constant for example x = 3. So we remove one part from (+) type because x is a constant here. In case our expression was \ x y -> x + y we have no constants here so the type would be `Num a => a -> a -> a` and on the other hand type of `g=x+y` is just Num a=>a whatever x and y are just assuming they are numbers right? – heisenberg7584 May 24 '19 at 15:41
  • 1
    @heisenberg7584 basically in a very simple way if you have expression like \x -> f x y the type result is A -> B where A is a type of x and B is the type of whole expression f x y – jake-ferguson May 24 '19 at 16:43
  • @heisenberg7584 If, under ghci, you ask for ":t 4" and then ":t (+)", you will see that 4 does not have a type, just a type constraint of _Num a_ ; the + sign has "Num a => a->a->a" which means that + forces its two operands and its result to have the same (numeric) type. So in an expression such as x+4, the + sign sort of extends the type constraint of 4, Num, to the other operand, x. So you cannot add an Int and a Double without using some explicit conversion operator. And "\x y ->x+y" has the same type constraint as + because it is essentially the same thing as +. Hope that helps. – jpmarinier May 24 '19 at 22:06
2

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.

Bjartur Thorlacius
  • 794
  • 7
  • 13
  • You can also choose more restrictive types. For example you could define the more specialized version of your function as: `\function -> function 5 :: (Float -> String) -> String` – Bjartur Thorlacius May 21 '19 at 16:10
0

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
Will Ness
  • 70,110
  • 9
  • 98
  • 181
jake-ferguson
  • 315
  • 3
  • 11
  • 32