Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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

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?
like image 807
Senjougahara Hitagi Avatar asked Jul 12 '13 05:07

Senjougahara Hitagi


People also ask

What is the meaning of this symbol ≤?

The symbol ≤ means less than or equal to. The symbol ≥ means greater than or equal to.

How do you explain integers?

An integer (pronounced IN-tuh-jer) is a whole number (not a fractional number) that can be positive, negative, or zero. Examples of integers are: -5, 1, 5, 8, 97, and 3,043. Examples of numbers that are not integers are: -1.43, 1 3/4, 3.14, . 09, and 5,643.1.

What does the (:) mean in math?

The colon is the symbol ":". It is used in a number of different ways in mathematics. 1. To denote ratio or odds, as in 2:1 (voiced "two to one"). 2.

How do you understand a function?

A function is a rule that maps a number to another unique number. The input to the function is called the independent variable, and is also called the argument of the function. The output of the function is called the dependent variable.


2 Answers

  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.

like image 183
J. Abrahamson Avatar answered Oct 09 '22 09:10

J. Abrahamson


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).

like image 30
Will Ness Avatar answered Oct 09 '22 10:10

Will Ness