CODEWITHSUNDEEP
haskelllambdatype-inferencetypinglambda-calculus
Highness
Highness

Reputation: 353

How do I find out the type of a haskell expression without ghci?

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

Upvotes: 0

Views: 282

Answers (2)

Yann Vernier
Yann Vernier

Reputation: 15877

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.

Upvotes: 2

YAMAMOTO Yuji
YAMAMOTO Yuji

Reputation: 1434

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

Upvotes: 0

Related Questions