Somewhere I read that writing programs is much like writing mathematical proofs.
Let’s try to understand what’s meant by that, by playing with Prolog.

Consider the following Prolog facts, that is, given definitions:

bigger(cat, mouse).
bigger(mouse, bug).

Now, we can ask Prolog what’s smaller than a cat?

?- bigger(cat, X).
X = mouse.

It of course responds that a mouse is smaller than a cat.
But what about a bug? Why didn’t it report that a bug is smaller than a cat?
This is so because Prolog doesn’t know much about this relation. Other than what is supplied to it, it assumes everything else is untrue. So, for instance, if we did:

?- bigger(cat, bug).
false.

We would get a negative answer.

To fix this, we need to implement a transitive relation of bigger. What this means is that if we have that A·B and B·C, then A·C holds as well, that is, ∀a, b, c ∈ X : (a·b ∧ b·c) ⇒ a·c. Do you see the mathematical similarity here?

In this case, · would be bigger. Let’s call this relation is_bigger.

This is how it looks:

is_bigger(A, B) :- bigger(A, B).
is_bigger(A, B) :- bigger(A, C), is_bigger(C, B).

Doing a couple of tests:

?- is_bigger(cat, mouse).
true .

?- is_bigger(mouse, bug).
true .

?- is_bigger(cat, bug).
true .

It seems to be working fine!

Now let’s try to explain the definition.

The :- operator here is like mathematical if, that is, if we did a :- b, and then ask for the truth value of a, it would report true if b were true as well. So by is_bigger :- bigger, we say that the former is true if the latter.

When you define multiple definitions in Prolog, it tries to find which one of them is true. In this case, it’s acting kind of an OR, it tries the first definition, then the second, and if all of them fail the result would be false, but even one of them succeeds and the result is true. Note that, we could also rewrite the definition like:

is_bigger(A, B) :- bigger(A, B); bigger(A, C), is_bigger(C, B).

That is, rewrite it using the ; operator as an OR. This is also valid, but much less readable.

In contrast, when you do a, b, c. in Prolog (i.e. comma operator), it does an AND, i.e. it first tries to prove a, then b, then c. If one of them fails, the result is false. Otherwise, it’s true.

One could easily notice that this definition is a recursive one, and the first one should be the base case of the recursion. This is correct.

So, calling is_bigger(cat, bug) would fail for the first definition, and then proceeds to the second (recursive) one to see if it can find a true match. So it tries to prove bigger(A, C), is_bigger(C, B), that is, it tries to find a C such that these 2 terms are logically true. But does there exist such C? Let’s try to further expand.

is_bigger(C, B) would first attempt to prove bigger(C, B), that is, bigger(C, bug). C in this case (according to the given facts) would be mouse. This is a possible match. Let’s return to bigger(A, C) and see if we can also fit mouse to it, i.e. is it true that bigger(cat, mouse)? Of course, this is also in the definitions. So for C = mouse, we can prove that bigger(A, C), bigger(C, B) is true. From this, it follows also that is_bigger(cat, bug) is true.

Would you agree that we’ve just written a mathematical proof? Given a few definitions, using transitivity we were able to deduce some fact, using Prolog.

The gap between Prolog and Mathematics is too small, in contrast to other languages, say Python and Mathematics. This is why notation is important. It makes you think in a different way for tasks you likely already solved using other languages.

So, let’s turn to our everyday languages for a while. What we have to deal with is some trees, some equality checking and we should be able to easily implement this in another language. Let’s try Python.

We’re going to write a program that attempts to prove a given search tree, just what Prolog did. With this, I think we will be able to see how writing programs is actually much like writing mathematical proofs.

I won’t go through the details, but here’s how it could look:

class node(object):
    def __init__(self, value, children = []):
        self.value = value
        self.children = children

    def contains(self, value):
        for x in self.children:
            if x.value == value:
                return True

        return False

    def __repr__(self, level=0):
        ret = "  "*level+repr(self.value)+"\n"
        for child in self.children:
            ret += child.__repr__(level+1)
        return ret

# The relation tree to work with
tree = node("bigger", [
    node("cat", [node("mouse"), node("bug")]),
    node("mouse", [node("bug")]),
])

# This function would attempt to find a correct proof for the given task
# It parses the tree
def find_proof(tree, A, B):
    if tree.value == A and tree.contains(B):
        return True

    for node in tree.children:
        if find_proof(node, A, B):
            return True

    return False

# Try to find proof
print(find_proof(tree, 'cat', 'mouse'))
print(find_proof(tree, 'mouse', 'bug'))
print(find_proof(tree, 'cat', 'bug'))

It returns:

True
True
True

What would be more interesting is to write a function that would generate the proof tree instead of us manually supplying it 🙂

Given these definitions:
(.) :: (b -> c) -> (a -> b) -> a -> c
map :: (a -> b) -> [a] -> [b]
head :: [a] -> a

Find the type of (map . head)

1. (f . g) x = f (g x)
(map . head) x = map (head x)

2. If we set
x :: [a -> b]
then we have
head x :: a -> b

3. \x -> map (head x) :: [a -> b] -> [a] -> [b]
=>
map . head :: [a -> b] -> [a] -> [b]

Let’s now try to find a senseful definition of [a -> b] -> [a] -> [b] by using hole-driven approach (inspired by http://www.youtube.com/watch?v=52VsgyexS8Q):

In this example we are using a silent hole (i.e. undefined). We are also writing the types of each argument (xs and ys)

{-# LANGUAGE ScopedTypeVariables #-}

f :: forall a b. [a -> b] -> [a] -> [b]
f xs ys = undefined
    where
    _ = xs :: [a -> b]
    _ = ys :: [a]

It’s compiling. But it does nothing.

Let’s try to do the same with a noisy hole:

data Hole = Hole

f :: forall a b. [a -> b] -> [a] -> [b]
f xs ys = Hole
    where
    _ = xs :: [a -> b]
    _ = ys :: [a]

We get this error:
Couldn’t match expected type `[b]’ with actual type `Hole’

How do we get from Hole to [b]? We have xs :: [a -> b]. What if instead we tried map?

f :: forall a b. [a -> b] -> [a] -> [b]
f xs ys = map Hole Hole
    where
    _ = xs :: [a -> b]
    _ = ys :: [a]

We now get these errors:
Couldn’t match expected type `a0 -> b’ with actual type `Hole’
Couldn’t match expected type `[a0]’ with actual type `Hole’

The second hole is obviously just ys:

f :: forall a b. [a -> b] -> [a] -> [b]
f xs ys = map Hole ys
    where
    _ = xs :: [a -> b]
    _ = ys :: [a]

Now we get:
Couldn’t match expected type `a -> b’ with actual type `Hole’

What if we try to use just xs instead of Hole?

Couldn’t match expected type `a -> b’ with actual type `[a -> b]’

Now it wants just x, not xs.

One way to get to that is to use (head xs)

f :: forall a b. [a -> b] -> [a] -> [b]
f xs ys = map (head xs) ys
    where
    _ = xs :: [a -> b]
    _ = ys :: [a]

This makes it happy.

Conclusion:
The function of type [a -> b] -> [a] -> [b] is not unique, because we could use something else for map instead of just (head xs).

Bonus:
id’ :: forall a. a -> a
id’ x = Hole
    where
    _ = x :: a

Couldn’t match expected type `a’ with actual type `Hole’

id’ x = x

Today I was again playing with folds, but this time implementing them in PHP.
So, consider the list [a, b, c]:
foldr f z [a,b,c] = a `f` (b `f` (c `f` z))
foldl f z [a,b,c] = (((a `f` b) `f` c) `f` z) = z `f` (c `f` (a `f` b))

Note the bolded parts of foldr and foldl. They look pretty same, just that the elements are kind of reversed (e.g. (0 – 1 – 2 – 3) against (3 – 2 – 1 – 0)).

Now consider we use array_reduce in PHP like this:

<?php
var_dump(array_reduce(array(1,2,3), function($x, $y) { return $x - $y; } ));

This will print “-6” as a result. And in Haskell:

Prelude> foldl (-) 0 [1,2,3]
-6

So it turns out we’re using a left fold. What can we do to make it a right fold?
What if we try something like

<?php
var_dump(array_reduce(array(1,2,3), function($x, $y) { return $y - $x; } ));

This one will print “2” as a result. Haskell says:

Prelude> foldr (-) 0 [1,2,3]
2

And in Haskell we can also do something like

Prelude> let f x y = y - x
Prelude> foldr f 0 [1,2,3]
-6

So, it’s interesting to play around with associativity of binary operators 🙂
But we don’t want to do it in a “hacky” way by changing the operands in the function. So we want foldr.
Here’s the full PHP code with foldr and foldl implemented:

<?php
interface iBinaryOperator {
    public function calc($x, $y);
}

function foldr(iBinaryOperator $f, $z, array $xs) {
    try {
        $x = array_shift($xs);
        if ($x == null) {
            return $z;
        }
        return $f->calc($x, foldr($f, $z, $xs));
    } catch (Exception $e) {
        return "error";
    }
}

// Foldl is tail recursive
function foldl(iBinaryOperator $f, $z, array $xs) {
    try {
        $x = array_shift($xs);
        if ($x == null) {
            return $z;
        }
        return foldl($f, $f->calc($z, $x), $xs);
    } catch (Exception $e) {
        return "error";
    }
}

class Subtraction implements iBinaryOperator {
    public function calc($x, $y) {
        if (gettype($x) != "integer" || gettype($y) != "integer") {
            throw new Exception("MathException");
        }
        return $x - $y;
    }
/*
    public function partial_calc($x) {
        if (gettype($x) != "integer") {
            throw new Exception("MathException");
        }
        return function ($y) use ($x) {
            if (gettype($y) != "integer") {
                throw new Exception("MathException");
            }
            return $x - $y;
        };
    }
*/
}

$x = new Subtraction();
var_dump(foldr($x, 0, array(1,2,3)));
var_dump(foldl($x, 0, array(1,2,3)));

/*
> php test.php
int(2)
int(-6)
*/