Can someone explain the meaning of ((.)$(.)) (==) 1 (1+) 0

Question

On haskell.org I came across this point free style function, dubbed "the owl".

((.)$(.))

Its type signature is (a -> b -> c) -> a -> (a1 -> b) -> a1 -> c.

It's equivalent to f a b c d = a b (c d) and apparently, ((.)$(.)) (==) 1 (1+) 0 returns True.

So my questions are:

1. What does the a1 in the type signature mean? Is it related to a?
2. Is (==) some kind of function equality operator? Because 0 (==) 0 throws an error in GHCi.
3. What does 1 (1+) 0 mean in this context? I don't see how this is even a valid expression.
4. Why does the expression return True?

Answer 1

1. The a1 is "just another type variable". It could mean anything, including a, but doesn't necessarily mean anything. Most likely it is different from a.

2. (==) is the "forced prefix" form of == the regular equality operator form the Eq type class. Normally you'd write a == b, but that's just syntax sugar for (==) a b, the prefix application of ==.

3. 1 (1+) 0 doesn't mean anything in particular in this context, each of the three subexpressions is an independent argument to "the owl", which ultimately takes four arguments.

4. We can walk through the reduction.

   ((.)$(.)) (==) 1 (1+) 0
   ===                          [ apply ]
   ((.)(.)) (==) 1 (1+) 0
   ===                          [ implicit association ]
   ((.)(.)(==)) 1 (1+) 0
   ===                          [ apply the definition: (f.g) x = f (g x) ]
   ((.) (1 ==)) (1+) 0
   ===                          [ implicit association ]
   ((.) (1 ==) (1+))  0
   ===                          [ apply the definition: (f.g) x = f (g x) ]
   1 == (1+0)
   ===                          [addition]
   1 == 1
   ===                          [equality]
   True
   

---

As this page mentions, the owl is equivalent to a function f

f a b c d = a b (c d)

which is to say it applies its first argument, a function of two arguments, to its second argument and the result of applying its third argument to its fourth. For the example given ((.)$(.)) (==) 1 (1+) 0 that means you first apply (+1) to 0, then combine the 1 and the (1+0) using (==) which is what happened in our reduction.

More broadly, you might think of it as a function which modifies a binary operation a to take a slight variation on its second argument.

Answer 2

First, let's write _B f g x = f (g x) = (f . g) x.

Since f $ x = f x, we have (.)$(.) = _B $ _B = _B _B. Its type is derived mechanically, as

0. (.) :: (    b      ->             c             ) -> ((a -> b) -> (a -> c))

1. (.) ::  (b1 -> c1) -> ((a1 -> b1) -> (a1 -> c1))

2. (.) (.) :: {b ~ b1 -> c1, c ~ (a1 -> b1) -> (a1 -> c1)} (a -> b) -> (a -> c)

           :: (a -> b1 -> c1) -> a -> (a1 -> b1) -> (a1 -> c1)
           :: (a -> b  -> c ) -> a -> (a1 -> b ) ->  a1 -> c  

a and a1 are two distinct type variables, just like b and b1. But since there's no b or c in the final type, we can rename b1 and c1 back to just b and c, to simplify. But not a1.

We can read this type, actually: it get f :: a -> b -> c a binary function; x :: a an argument value, g :: a1 -> b a unary function, and another value y :: a1, and combines them in the only possible way so that the types fit:

    f x       :: b -> c
    g y       :: b
    f x (g y) ::      c

The rest is already answered. Reductions are usually easier to follow in combinatory equations, like _B _B f x g y = _B (f x) g y = f x (g y), just by two applications of _B's definition (we can always add as many arguments as we need there).