0

I'm pretty good at inferring the type of a lambda expression as long as it does not have any weird functions such as map, filter, foldr or any compositions in it. However, as soon as I have something like

\x y -> map x (y (. x))

I get totally lost and can't for the life of me figure out how to find out the type without using ghci.

Any help would be much appreciated

Thank you

Willem Van Onsem
  • 443,496
  • 30
  • 428
  • 555
Highness
  • 333
  • 4
  • 11
  • By doing the type inference yourself. Can you share your attempt? – Willem Van Onsem Jul 31 '18 at 12:18
  • I try to rewrite the expression like so : \x y z -> map x (y (x.z)) then \x y z -> map x (y ( (.) x z)) then I try to infer the type of the expression inside the parenthesis but I fail at that. – Highness Jul 31 '18 at 12:29
  • 1
    Well you can not perform such rewrpite, since it is `(. x)`, which is short for `\z -> (.) z x`, so the rewrite is `\x y -> map x (y (\z -> (.) z x))`. – Willem Van Onsem Jul 31 '18 at 12:54
  • 1
    Well, start from the outermost function which is `map`. Its type is `(a -> b) -> [a] -> [b]` and you know that `x` has type of `a -> b` and `y (. x)` has type of `[a]`. Then repeat with `y`. – Dannyu NDos Jul 31 '18 at 14:31
  • could you please elaborate some more? The (. x) gives me the most trouble. I think I should figure the type of y out after that? – Highness Jul 31 '18 at 14:49
  • 1
    What part of [Hindley-Milner](https://i.stack.imgur.com/xkKgE.png) don't you understand? ([Tongue firmly in cheek.](https://stackoverflow.com/q/12532552/791604)) – Daniel Wagner Jul 31 '18 at 15:19

2 Answers2

2

I take it by "weird" you pretty much mean higher order functions. This expression contains two: map :: (a -> b) -> [a] -> [b] and (.) :: (b -> c) -> (a -> b) -> a -> c. It is also a lambda, so likely a higher order function itself. Each parenthesized arrow here is the type of a function parameter.

map reveals that y must return a list of items that x accepts as an argument. So they have the partial signatures x :: _yitem -> _outeritem and y :: _yarg -> [_yitem], where the return value of this map is of type [_outeritem]. Note that we don't know yet how many arrows fit in these wildcards.

(. x) translates to \l -> l . x which translates to \l r -> l (x r). This entire lambda is an argument that fits y, so y is a higher order function. l must accept the return value from x. That has a name, so l :: _outeritem -> _lret, and (. x) :: (_outeritem -> _lret) -> _xarg -> _lret, since r is used as the argument for x. Oh, and _xarg is known because of the map to be _yitem.

Okay, that was a bunch of confusing steps in their own right, so let's line up the results:

type OuterLambda = _xtype -> _ytype -> MapRet
x :: _yitem -> _outeritem
type MapRet = [_outeritem]
y :: YArg -> [_yitem]
type YArg = (_outeritem -> _lret) -> _yitem -> _lret
y :: ((_outeritem -> _lret) -> _yitem -> _lret) -> [_yitem]

Progress! This has names for every type to and from x and y. But our expression is a lambda, so we must accept those two:

(_yitem -> _outeritem) -> 
(((_outeritem -> _lret) -> _yitem -> _lret) -> [_yitem]) ->
[_outeritem]

That's one very long type. Let's compare it to the compiler inferred type that Yuji Yamamoto showed us:

(a0 -> b0) -> 
(((b0 -> c0) -> a0 -> c0) -> [a0]) -> 
[b0]

It matches. We have here quite a few orders of function: the expression expects functions x and y, and y expects a function that itself takes a l function. And all of the types we do have names for may in turn be arbitrarily complex.

Yann Vernier
  • 15,414
  • 2
  • 28
  • 26
0

Annotating intentionally wrong type (often ()) would help you.
For example:

> (\x y -> map x (y (. x))) :: ()

<interactive>:1:2: error:
    • Couldn't match expected type ‘()’
                  with actual type ‘(a0 -> b0)
                                    -> (((b0 -> c0) -> a0 -> c0) -> [a0]) -> [b0]’
    • The lambda expression ‘\ x y -> map x (y (. x))’
      has two arguments,
      but its type ‘()’ has none
      In the expression: (\ x y -> map x (y (. x))) :: ()
      In an equation for ‘it’: it = (\ x y -> map x (y (. x))) :: ()

This tip is introduced in this post: http://www.parsonsmatt.org/2018/05/19/ghcid_for_the_win.html

YAMAMOTO Yuji
  • 1,364
  • 9
  • 17