The
a1
is "just another type variable". It could mean anything, includinga
, but doesn't necessarily mean anything. Most likely it is different froma
.(==)
is the "forced prefix" form of==
the regular equality operator form theEq
type class. Normally you'd writea == b
, but that's just syntax sugar for(==) a b
, the prefix application of==
.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.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.