The type and definition of a function that is formed from two given functions

user_14301045 0
Viewed 272

I was asked to write the most simple definition of the result of s k k, where

s = \ f g x -> f x (g x)
s :: (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3
k = \ x y -> x
k :: p1 -> p2 -> p1

Writing :t s k k in the terminal gives: t -> t.

I think s takes two functions - f and g. where f takes t1 and t2 as inputs and returns t3. function g takes t1 as input and returns t2, and x is t1. Why is t3 the return type?

I think I understand function k, where you take x and y as inputs and the type of x is output. Is there a common approach when it comes to understanding how these two functions will work together forming s k k.

I also tried going step by step typing :t s k, which gives (t3 -> t2) -> t3 -> t3, however, that didn't help me too much :) Can someone explain this to someone new to Haskell?

haskell
2 Answers

If fun :: a1 -> b and arg :: a2, then the application fun arg :: b and a1 ~ a2 (a1 is equal to a2).

s k k is the same as (s k) k because function application associates to the left. So we have an application s k:

s   :: (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3
k   :: (p1 -> p2 -> p1)

s k ::                     (t1 -> t2) -> t1 -> t3

p1 ~ t1
p2 ~ t2
p1 ~ t3

Note that p1 ~ t1 and p1 ~ t3, therefore t1 ~ t3:

s k ::                     (t1 -> t2) -> t1 -> t1

In the application (s k) k, a similar thing happens; I’ll rename the type variables with a prime ' to indicate that this is a different instantiation of k’s type:

(s k)   :: (t1  -> t2        ) -> t1 -> t1
      k :: (p1' -> p2' -> p1')

(s k) k ::                        t1 -> t1

t1 ~ p1'
t2 ~ p2' -> p1'

Notice that when t1 -> t2 is unified with p1' -> p2' -> p1', which is equal to p1' -> (p2' -> p1') because function types are right-associative, t2 is equated with the function type p2' -> p1'.

As a result, the type of the whole expression is t1 -> t1, or forall t1. t1 -> t1 with ExplicitForAll. Even without knowing the term here, there is only one function (which is total) of the type forall a. a -> a, and that is id. Indeed s k k is just a roundabout way of implementing the identity function, because for any X we give it, it returns X:

s k k X
(\ f g x -> f x (g x)) k k X
(\ g x -> k x (g x)) k X
(\ x -> k x (k x)) X
k X (k X)
(\ x y -> x) X (k X)
(\ y -> X) (k X)
X

The first k selects X, and the second application of k is ignored. That’s why neither of the type variables from the second use of k (p1' and p2') appear in the resulting type.

user_2468860

Well we know from their definitions that

s k k x = k x (k x) = x 

-- s = \f g x -> f x (g x)
-- s    k k x =  k x (k x)

-- k = \ x  y    -> x
-- k     x  y    =  x
-- k     x (k x) =  x

so that

s k k = \ x -> x

and thus its type is

a -> a

GHCi concurs (as you've already noted):

> :t s k k
s k k :: t3 -> t3

As to the types in s you ask about,

s :: (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3
s = \ f g x -> f x (g x)
s     f g x =  f x (g x)
--
--         x  :: t1
--       g    :: t1 -> t2
--       g x  ::       t2
--    x       :: t1
--  f         :: t1 -> t2 -> t3
--  f x (g x) ::             t3

just follow from the most basic rule of type inference in application,

        x  ::  A                          x :: a
      f    ::  A -> B                   f   :: b -> c
    -------------------                --------------
      f x  ::       B                   f x ::      c  , a ~ b

This is analogous to Modus Ponens in logic, "if we have A, and A implies B, then B holds as well".

If you wanted to get this from the types of s and k a.o.t. their definitions, a similar kind of diagram works for that as well:

s     :: (a -> b -> c) -> (a ->     b    ) -> a -> c
  k   ::  x -> y -> x
-------  a~x, b~y, c~x  => c~x~a  -------------------
s k   ::                  (a  ->    b    ) -> a -> a
    k ::                   x2 -> y2 -> x2
----------------------  a~x2, b~(y2 -> x2)  ---------
s k k ::                                      a -> a

(you can see the type you asked about, s k :: (a->b)->a->a, there). Here you can see the type unifications done "step by step" but the two unifications could well have been done together,

s     :: (a -> b -> c) -> (a ->     b    ) -> a -> c
  k   ::  x -> y -> x
    k ::                   x2 -> y2 -> x2
-------  a~x, b~y, c~x  => c~x~a  -------------------
----------------------  a~x2, b~(y2 -> x2)  ---------
s k k ::                                      a -> a

The end result is of course the same. Whether we read the above diagram at once or in stages, it's the same diagram. Currying is nice, and it works. And since it works, when you've already applied a thing to two other things you needn't concern yourself with the partial application in stages. Except maybe as a mental exercise.

There's nothing much to say about all these interim types really. You just write them one under the other, being careful to rename the variables consistently at different invocations to avoid capture, noting the resulting equivalences and using them to simplify the resulting types.

Last thing to notice is that s k s and s k (s k) etc. could also be used for the same purpose. Almost, just like ($) is almost the same as id.

user_8498910
Related