CODEWITHSUNDEEP
haskelllambdatypesexpressiontype-inference
bobaxs31
bobaxs31

Reputation: 53

Inferring type of lambda expression

Given a function a with the following type:
a :: x -> Bool
and another function b of the following type:
b :: Bool -> y
I am trying to figure out the steps to infer the type of the following function:
c = \d -> d a b
Could someone please help with help explaining how to do it not just by putting it through ghc's :type function? Thanks

Upvotes: 3

Views: 637

Answers (2)

MCH
MCH

Reputation: 2204

Another approach I would take to make sure I am getting the type signature I expect for a particular lambda expression while avoiding :t is to use type signatures.

In this case, x is unrestricted.

idFunction = \x -> x

If we want to restrict to a particular type, we can annotate x directly. (This requires :set -XScopedTypeVariables in GHCi or {-# LANGUAGE ScopedTypeVariables #-} in a file).

idFunction = \(x :: Int) -> x

or we can add a type signature

idFunction :: Int -> Int
idFunction = \x -> x

In your example you only have type signatures, but no function bodies. Let's add some simple function bodies so we can do something with the compiler, then we will try adding a type signature to c confirm our belief of what the type should be. We will start with an incorrect type signature.

a :: Int -> Bool
a x = x > 0

b :: Bool -> String
b y = show y

c :: ((Bool -> Bool) -> (Bool -> Bool) -> t) -> t
c = \d -> d a b

The compiler will find some errors in c:

<interactive>:10:17: error:
    • Couldn't match type ‘Bool’ with ‘Int’
      Expected type: Bool -> Bool
        Actual type: Int -> Bool
    • In the first argument of ‘d’, namely ‘a’
      In the expression: d a b
      In the expression: \ d -> d a b

<interactive>:10:19: error:
    • Couldn't match type ‘[Char]’ with ‘Bool’
      Expected type: Bool -> Bool
        Actual type: Bool -> String
    • In the second argument of ‘d’, namely ‘b’
      In the expression: d a b
      In the expression: \ d -> d a b

Now if we give c the correct type signature it will compile

c :: ((Int -> Bool) -> (Bool -> String) -> t) -> t
c = \d -> d a b

Generally there isn't any reason to avoid :t. It's it perfectly good tool when you are working in GHCi, but when you are building complex functions in a library, you don't necessarily have access to :t, so an alternative is to test different type signatures and see how the compiler reacts.

Upvotes: 2

ktzr
ktzr

Reputation: 1645

the type of c = \d -> d a b will be c :: ((x -> Bool) -> (Bool -> y) -> t) -> t

Where d is a fuction that takes in a (x -> Bool) and a (Bool -> y) and returns a value of type t.

So c is a function that takes in function of type d and returns a value of type t

If you mean c = \d -> d (a b) the type will be c :: (Bool -> y) -> y

Some extra explanation.

To know c we must first know what ddo so we look at c = \d -> d a b

We see \d -> d a b so we know d's first argument is the function a with type (x -> Bool). We also know d's second argument, it is the function b with type (Bool -> y). But we don't know what it returns, as this is Haskell it must return something, so I'm just going to write t as an unknow type. So d is d :: a -> b -> t.

Substitute in the type of a and b and we get d :: (x -> Bool) -> (Bool -> y) -> t.

Now for c, c is a lambda that takes in a value we can infer is of type d, and returns its output. So we get c :: d -> (d's output).

Substitute in the type of d and we get c :: ((x -> Bool) -> (Bool -> y) -> t) -> t

Upvotes: 3

Related Questions