When I find something interesting and new, I post it here - that's mostly programming, of course, not everything.

Thursday, April 28, 2011

Church Numerals in Scala

As everyone knows (see http://en.wikipedia.org/wiki/Church_encoding), in pure lambda one can define natural numbers out of nothing, like this:

0 ≡ λ f λ x . x
1 ≡ λ f λ x . f x
2 ≡ λ f λ x . f (f x)
3 ≡ λ f λ x . f (f (f x))
etc.

At our BACAT meeting yesterday, there was a question, for typed lambda, how can one express natural numbers, and also how can one interpret them in a Cartesian-closed category?

The answer to this question turned out to be trivial, but we also had managed to express it in Scala:
class TypedLambda[T] {
type TT = T => T
type Church = TT => TT
val cero: Church = f => x => x
def succ(n: Church) = f => n(f) compose f
val uno = succ(cero)
val dos = succ(uno)
val tres = succ(dos)
}


Looks neat, eh?

The alternative approach can be found in Jim McBeath's post.

Sunday, January 02, 2011

Notes on my relations with CT

Zaki suggested me to write something on this topic...

So, what happened to me... In several stages.

1. I'm 19, a student in Leningrad University (that's USSR, now called Russia), and I attend a special course on homological algebra. Professor Yakovlev starts it with a short intro into category theory, a topic nobody heard of. I was overwhelmed. The thing that generalizes groups and sets and whatever. Diagrams, wow. Commutative diagrams, diagram chasing, wow. The rest was not so interesting; abelian categories, exact diagrams, hom, tensor product, ext and tor... oh whatever. In a couple of years I decided not to go into algebra.

2. I am 24, working as a programmer, trying to pick up some "science". Somewhere (where?) I see a title of a paper, "Applying Category Theory to Computer Science". Wow. My eyes are open. Here it is; database structures, they are just pullbacks. Programs, they are diagrams, are no they? Okay, nobody hears me; and more, there's no way I can get the paper. So just have to guess.

3. I am 27; me and my friends are camping somewhere in the forests of Novgorod region. Vodka, talks... I mention category theory as a good tool for perceiving comp. sci. Andrey responds by inviting me to a category seminar that they have at Technological Institute in Leningrad. Wow! I join them.

4. Several years of studying categories and toposes; MacLane's Categories for the Working Mathematician - I get the microfilm, and print it, samizdat style, in tinest possible print, for the participants. It costs 10 roubles each (like 3 bottles of vodka, if you know what I mean).

5. Andrey's friend is married to a relative of Vonnegut. So this friend, he is an otkaznik, and his American wife stays with him for several years, raising a kid, painting, just being patient. Meanwhile, after one of her trips back to US she brings Johnstone's Topos Theory... and on another trip she brings "Lolita". I devour both books. Have made hand copies of Topos Theory. Twice.

6. Andrey suggests to try to calculate topologies (and, of course, logics), over some specific finite categories; he is specifically interested in Delta3, the initial segment of simplicial category. I write code first in Basic, then figure out that the calculation for delta3 would take 2 weeks. Rewrite it into Fortran; now it's just a couple of days. So I rewrite the core parts (like enumerating subsets, calculating cones and limits) into Assembler. We have the list of 31 Grothendieck topologies over delta3 in just four hours. Meanwhile we calculate topologies for simple categories, like linear segments, commutative squares... a strange thing is discovered, on many occasions the number of topologies is 2^n, where n is the number of objects. That's for posets.

7. I prove it that for finite posets this is the case, and a little bit more. Then I spend months trying to find a typewriter with English letters (KGB is watching); used one in Hungarian trade mission, and one in the Institute of Hydrology (where global warming was then starting). Then I spend some time figuring out how to send the paper, then a KGB colonel suggests a solution, and I use it. It's published in Cah.Topo.Geom.Diff. The hardest part was deciphering French written notes on proofs.

8. I meet Yakovlev; for him, it is all a) "abstract nonsense", and b) it can't be that the result is not known yet.

9. I generalize this stuff to Karoubian categories over Boolean toposes (Booleanness is necessary) and send it to Johnstone. Johnstone, it turned out, was working on a similar problem, from the other end. So I spend the next 15 years trying to get the proof in the opposite direction - that if... then the category is Karoubian. That's how I did not do anything else. At least I tried.

10. The seminar meanwhile had died out - the guy, Stepanov (can I call him professor? something like that... he was not), had married and moved to Novorossiysk, a pretty criminal place; there he died in strange circumstances.

11. Now here in California, the word "monad" rings the bell. So I honesty try to put it in the proper perspective, writing some kind of "tutorials" and "talks", writing again the code that calculates stuff, opening presheaf.com, and ready to talk to anybody willing to listen.

12. And now we have BACAT, a category seminar where we can discuss things. And this is great.

Saturday, October 16, 2010

Sunday, September 19, 2010

Running with SBT

So, you are tired of your slow and half-dumb ides, ok, what can you do to make your scala dev cycle more agile? Use sbt.

First go to that website, and download the jar. Store it somewhere. Write a shell script or a bat file with the only command:

java -Xmx512M -jar wherever you store the jar/sbt-launch-0.7.4.jar


Go to your project directory and run your sbt there. It will ask you some questions regarding what version of Scala you want to order, the name of your project, the like. Then it will create an sbt project in that directory. Now the project expects the directory structure to follow maven rules of the game. You don't have to. Go to the directory named project, create a directory named build, and within that directory create a scala file Project.scala, that looks something like this:

import sbt._

class CategoriesProject(info: ProjectInfo) extends DefaultProject(info)
{
// lazy val hi = task { println("Categories in Scala"); None } // that's for fun
override def mainScalaSourcePath = "src" // your source directory
override def mainResourcesPath = "resources" // fiik what is this for

override def testScalaSourcePath = "tests" // your tests directory
override def testResourcesPath = "test-resources" // fiik what is this for
override def outputDirectoryName = "bin" // your output directory
}


Additionally, check out lib directory in your project; it probably contains already some stuff that sbt believes it needs - that is, scala-compiler.jar, and scala-library. Copy over there the other jars you believe you need. There should be a way to reference them where they are, but I have not figured it out yet.

Now start sbt again.

If you give it a command ~test, it will cycle through compiling the code and running the tests, automatically detecting what to compile and guessing what tests to run. As soon as you save a source file, sbt wakes up and does the job.

So... I love it... as do many other scala people.

Sunday, September 12, 2010

Dealing with Infinities in Your Code - 3

Here I had introduced countable sets, and here I had demonstrated how we can build a union of two countable sets. Now is time for Cartesian products.

Suppose we have two sets, {'A', 'B'} and {1, 2, 3}. Their product will look like this: {('A',1), ('A',2), ('A',3), ('B',1), ('B',2), ('B',3)}. It is pretty easy to build: iterate over the first set, and for each element iterate over the second set. In Scala it is pretty easy:

for (a <- setA;
b <- setB) yield (a, b)


The problem is that if the second component (setB) is infinite, we will never be able to iterate over all elements. Let setB be, for instance, the set of all natural numbers, N. In this case the product setA x setB will be yielding ('A',0), ('A',1), ('A',2),..., and will never switch to pairs like ('B',i). We have to do something about it.

Say, in the case when only one component is infinite, we could think about changing the order of the loop, first iterating over the infinite component.

That won't work actually. We cannot always know for sure if a set is finite or not. Halting problem, you know. So we have to figure out how to do it in a general way, without losing common-sense efficiency for the finite case.

The solution has been known for over 100 years, and is called Kantor Pairing Function.
In this picture: you see this function enumerating pairs of natural numbers in the following order: (0,0), (1,0), (0,1), (2,0), (1,1), (0,2), (3,0)... - you got it.

In our case we have two essential differences: first, the sets we have are not necessarily finite, and second, elements are not retrievable by their "sequential numbers"... meaning, it's possible, but it is horribly ineffecient: to reach element #1000, we need to rescan all the elements from #1 (or rather #0, since natural numbers and array indexes start with 0). So we also do not need a fancy formula for Kantor Pairing Function (see link above), the formula that calculates product elements by their sequential numbers. All we need is a way to iterate over elements in the right order.

Okay, let's first write the factory method for Cartesian products:

def product[X, Y](xs: Set[X], ys: Set[Y]): Set[(X, Y)] = {
val predicate = (p: (X, Y)) => xs.contains(p._1) && ys.(p._2)
setOf(
kantorIterator(xs, ys),
xs.size * ys.size,
predicate
)
}


The predicate definition is extracted just for readability purposes. What's important here is kantorIterator that is supposed to work with any combination of finite and infinite countable sets.

Since we do not have direct access to the elements of the sets by their indexes, we will, instead, keep the rows in iterators. Note that we can build a queue of such iterators. Let's call them rows. What the algorithm does is this:
- push row0 to the iterator queue
- yield (row0.next, y0)
- push row1 to the iterator queue
- yield (row0.next, y0) (first iterator from iterator queue)
- yield (row1.next, y1) (second (last) iterator from iterator queue)
- push row2 to the iterator queue
- yield (row0.next, y0) (that is, (x2,y0))
- yield (row1.next, y1) (that is, (x1,y1))
- yield (row2.next, y2) (that is, (x0,y2))

and so on: every time we reach the end of the queue, we push the next row iterator into the queue, reset the vertical iterator, and start all over.

The problem arises when one of the iterators is out of elements.

We have two possible cases.

Case 1. The vertical iterator halts. In this case we stop pushing new iterators into the queue, so that the size of the queue is the size of the vertical component.
Case 2. the horizontal iterator halts. The vertical one may be infinite or not, we have to shift it. E.g. if we build {'A', 'B','C'} x N, we will be producing ('A',0), ('B',0), ('A',1), ('C',0), ('B',1), ('A',2), ('C',1), ('B',2), ('A',3).... Note that after ('C',1) row0 is out of elements, and this row should be dropped from the queue. At the same time the beginning element of the vertical iterator should be shifted, so that the next loop will be not 0,1,2, but 1,2,3. In such a way we go all along the vertical iterator.

Here's the code:
def kantorIterator[X, Y](xs: Iterable[X], ys: Iterable[Y]): Iterator[(X, Y)] =
new Iterator[(X, Y)] {
var iterators: Queue[Iterator[Y]] = Queue()
var xi = xs.iterator
var yi: Iterator[Iterator[Y]] = Iterator.empty
var shift = 0

def next = {
if (!yi.hasNext) {
if (xi.hasNext) {
iterators enqueue ys.iterator
}
yi = iterators.iterator
xi = xs.iterator.drop(shift)
}

val yii = yi.next
val y = yii.next
val res = (xi.next, y)

if (!iterators.isEmpty && yii.isEmpty) {
iterators.dequeue
shift += 1
}

res
}

def hasNext = !xs.isEmpty && !ys.isEmpty &&
(xi.hasNext || (!iterators.isEmpty && iterators(0).hasNext))
}


hasNext covers all the cases of empty components.

I probably have to mention that you won't be always able to iterate over all the subsets of a countable set. If the set is finite, it's okay, its powerset is finite; but if it is not, here you can find Kantor's proof that the powerset of an infinite countable set is not countable.

Dealing with Infinities in Your Code - 2

In this post I had introduced the idea of having countable sets in your code. Next I want to show how we can combine countable sets producing new countable sets.

We have two operations, union and Cartesian product. Let's start with disjoint union - the union of non-intersecting sets.

If we expect our sets to be both finite, there's nothing special here. The predicate checks whether an element belongs to one set or another; the iterator iterates over the first set, then the second.

What if one or both of our sets is/are infinite? The predicate seems to be still okay: we just check whether the element belongs to one of the sets. But the iterator... if the first set is infinite, our naive iterator will never reach the second set. I mean, not in this universe; we will need transfinite numbers readily available, which is well beyond the power of modern computers or most of modern humans. What can we do then? Well, we can alternate over two iterables.

Let's look at the code:
def union[X, X1 <: X, X2 <: X](set1: Set[X1], set2: Set[X2]): Set[X] = {
lazy val parIterable = new ParallelIterable(set1, set2)
lazy val size = if (set1.size == Integer.MAX_VALUE ||
set2.size == Integer.MAX_VALUE) {
Integer.MAX_VALUE
} else {
set1.size + set2.size
}
setOf(parIterable,
size,
(x: X) => (x.isInstanceOf[X1] && (set1 contains x.asInstanceOf[X1]))||
(x.isInstanceOf[X2] && (set2 contains x.asInstanceOf[X2]))
)
}


What we have here? A new iterable, a new size evaluator, a new predicate. We can ignore the size evaluator; nothing is calculated here until someone requests it. The predicate is obvious; the only new thing is ParallelIterable. We need it to iterate over the union of two countable sets (rather, over two iterables) in a smart way:

class ParallelIterator[X, X1 <: X, X2 <: X](
iterator1: Iterator[X1],
iterator2: Iterator[X2]) extends Iterator[X] {
var i2 : (Iterator[X], Iterator[X]) = (iterator1, iterator2)
def hasNext = iterator1.hasNext || iterator2.hasNext
def next = {
i2 = (i2._2, i2._1)
if (i2._1.hasNext) i2._1.next else i2._2.next
}
}


Note that we flip i2, so it changes from (iterator1, iterator2) to (iterator2, iterator1) and back every cycle.

As a result, in the output we just interleave members from the first component with the members of the second component. What is important here is that we do not make any assumptions regarding which iterator is finite and which is infinite; if one component does not have more elements, fine, we continue scanning the other one.

This was probably pretty simple; now we have to deal with Cartesian products, that is, the set of all pairs (x: A, y: B) where x is from the first set and y is from the second set; with no assumptions regarding the finiteness of the said sets.

That would be the next part.

Thursday, September 09, 2010

Dealing with Infinities in Your Code - 1

These days it is not unusual to have an infinite sequence in a computer system. The idea is that while the sequence grows, the system upgrades, and there's no limit unless we make certain assumptions like accepting non-standard arithmetics. Then even sequences that we expect to be finite may turn out to be infinite - like Goodstein's sequence.

Still, it seems like in a foreseeable future we will only encounter countable sets. They are not necessarily infinite; any finite set is traditionally considered countable, that is, equal in size to a subset N, the set of natural numbers. The set of all real numbers, R, is a typical example of an uncountable set (it is a continuum). (Whether there is a set of intermediate size, between N and R, depends on what axiom we assume. If we assume it exists, it exists; if we assume it does not exist, it does not. Quite an eye-opener for people that use to treat Mathematics as a provider of absolute truths, right?)

What's good in a countable set is that (assuming set-theoretical axioms) one can list its element in such a way that any arbitrary element may be eventually reached. (That's due to another axiom, the Axiom of Choice - it says that we can introduce linear order in any set. If we don't assume this axiom - then we cannot.)

When I worked in Google, one of my favorite interview questions was "given an alphabet, write a code that would produce all words that сan be built based on this alphabet". Then I had to explain that when words are built out of alphabet, it does not mean each letter is used at most once. It does not. Then I had to explain that by "producing all words" I mean writing a code that could reach any word that can be built out of the alphabet. For instance, given {A,B}, the sequence "A", "AA", "AAA", etc would be infinite, but it won't constitute a solution: it will never reach letter 'B'.

In my work I limit myself with sets as they are presented in Java or Scala.

One particular problem is that, usually, an implementation of Set is supposed to have a method that returns the set's size. Not sure I know why. Probably it has something to do with array reallocations... some technical stuff. Because see, if you know that your set is infinite, you are safe, you can always return, by the rules of Java, Integer.MAX_VALUE; but what if you do not know? Say you have a function that takes another function, calls it subsequently until it halts (e.g. fails), and records the times it takes each call. What would be the size? We have to solve Halting Problem to know the answer.

On the other hand, isEmpty is a pretty decent method; it could easily belong to Iterable: to check if an Iterable is empty, one has to just get its Iterator and call its hasNext.

Also, it would be good to supply a set with a predicate, similar to what they do in Zermelo-Fraenkel Set Theory: according to the Extensionality Axiom, two sets are equal iff they consist of the same elements. Not having to count to infinity (or futher) to check if an element belongs would be a good advantage. E.g. for the set of all odds the predicate would not have to scan through all odd numbers from 1 to the given one; just check its last bit.

So that's why I came with a set that is defined by its

  • iterable that enumerates the elements;

  • predicate that "efficiently" checks if a value belongs to the set

  • size evaluator that, when called, tries to evaluate the size of the set
  • .

I use Scala for coding these days; hope it is reasonably pretty:

private def setForIterator[X](sourceIterator: => Iterator[X], sizeEvaluator: => Int, predicate: X => Boolean): Set[X] = {
new Set[X] {
override def contains(x: X) = predicate(x)
override def size = sizeEvaluator
override def iterator = sourceIterator filter predicate
override def isEmpty = !iterator.hasNext
override def -(x:X) = requireImmutability
override def +(x:X) = requireImmutability
def map[Y] (f: Functions.Injection[X,Y]) : Set[Y] = f.applyTo(this)
def map[Y] (f: Functions.Bijection[X,Y]) : Set[Y] = f.applyTo(this)
override def filter(p: X => Boolean) = filteredSet(sourceIterator, (x: X) => predicate(x) && p(x))
}
}

def setOf[X](source: Iterable[X], sizeEvaluator: => Int, predicate: X => Boolean) =
setForIterator(source.iterator, sizeEvaluator, predicate)


Had to override a bunch of methods declared in trait Set, to avoid any immediate calls of size evaluator or assuming that the size is known.

Here's how, using this class, we can define the set of natural numbers:
val N = setOf(new Iterable[Int] {
def iterator = new Iterator[Int] {
private var i: Int = -1
def hasNext = true
def next = {i += 1; i}
}
},
Integer.MAX_VALUE,
(x: Any) => x.isInstanceOf[Int] && x.asInstanceOf[Int] >= 0)


That's it for now. In the next part I'll talk about how to combine two countable sets. It is an old fact that a union and a product of two countable sets are countable; we will need a code that behaves according to this knowledge.

Tuesday, July 20, 2010

iterable, tree, monad, foundation axiom

Everybody knows now that linear data are bad for performance. But in Java everything is based on Iterable, with the idea, deeply rooted in math, that we can only visit the content of X if we iterate over it (enumerable sets etc), that is, have an epimorphism from N to that X.

Well, that's stupid. All we need is foundation axiom to hold.

In plain words, a tree is good as well, but a tree can be scanned in parallel.

But programmers of the world were trained to write a loop every time they see a plurality of something.

But the loop does not actually mean it should be interpreted sequentially.

If you write

for (x <- container) {
}

it only means that the job is done inside a monad.

That's why you should think monad, eh. That's why enumerables are XX century. Foundation axiom is way more powerful.

I actually can even prove it, but only for a Boolean base topos.

(oneof the sources)

Sunday, April 18, 2010

How I Installed a TV Antenna

I live in South San Jose; recently we have discovered that now that we have fast Internet, WII and Netflix, we already have access to hundreds of movies, so what do we need a tv for? Local news. Okay, but they are being broadcast for free, in hdtv, just install an antenna on the roof and go.


Started with looking up our area on antennaweb: entered my address and it gave me directions and this map.

The site also say that frequency ranges have colors, and that I have to choose an antenna that has the right colors.







Since there's over 60 miles from my home to San Francisco, the only reasonable choice was ChannelMaster 4228D - they sell it at Fry's.


Turned out that to install it I need more than just this box. I need a pole and the stuff to attach the pole to the roof. Below I explain what I did.

I bought a 5-foot piece of "black pipe" at Lowe's (here on the picture the end of the pipe), a cap for the pipe and the piece which I want to attach to the roof.




You need a cap on top so that rain won't penetrate the pipe.
Before attaching the bottom piece to the roof, I had patched the area below with roof coating, to avoid leaks:


Now we need these things from OSH (electric department and bolts and nuts department) to attach to the pole the guy wire that will hold it.




This is how the top of the pole looks like with all the stuff attached:



I have attached two eye screws to the sides of my roof, and two went straight into the roof:


After I drilled the hole for the screw, I patched it so the rain won't get in:



Now I have to attach the guy wire to the pole and to the eye screws; for this I use clams:




The guy wire does not go all the way through from the top of the pole to the screws. I cut the wire and attached turnbuckles that allow me to tighten the wires later:


This is how it looks with antenna attached to the pole using brackets, and the guy wires tightened with turnbuckles.



Now it's time to get the cable into the house. I bought a 25-foot white coaxial cable, connected it to the antenna's amplifier, got it along the roof and the wall.




I had measured the position of an existing tv socket inside the room, and used a long drill to drill through the wall to get to the socket as close as possible.




I used this bushing for the cable to get through. Bought it at Lowe's.



Had to cut the bushing, or else how would I get the cable through?




When I got the cable through the wall, I applied a good amount of clear caulk to make sure no water gets through.




I was lucky, the cable got exactly where I wanted it.






So all I had to do is connect my tv, scan the 56 channel it found and enjoy the show.

And you know what? It sucks. I don't have a dvr on those channels, so there's no way I can pause it, or get any information regarding what is it about... no recording. And the channels... what nonsense people watch, omg.

So, was it all worth it? Probably. I had fun with my antenna.

Here's a photo I took from a digital channel:

Monday, March 29, 2010

Hidden Monads in Scala

Actually, not monads, just functorial stuff. But programmers seems to be unaware of the fact that a monad is a special kind of functor, so...

In Scala, one can define a functor something like this:

  trait Functor[X] { 
def map[Y](f: X => Y): Functor[Y]
}


All we need here is map. Lists have map, Options have map... The natural use of a map is to apply it to a function. Like this:


def loop[X,Y](f: Functor[X], a: X=>Y) = f.map(a)


In Scala, loops can work as maps. And if you are a Haskell programmer, you'll immediately recognize your monadic notation:

  
def loop[X,Y](f: Functor[X], a: X=>Y) = for (x <- f) yield a(x)



These two are exactly the same.

Praise Scala!

Update: see recent blog entry on monads by Luc Duponchel for a lot more details.

Wednesday, March 24, 2010

Topics in Coding Style

While at Google, I believed in two things: peer code review and unacceptability of ascii art in the code.

Peer code review means you are supposed to show your stuff to somebody in your team before submitting it. So, when you want to submit the stuff in the end of the day (yes, all unittests pass), you are supposed to hold on, wait for half a day (the next day), not touching the code, get into a discussion, and then, eventually get through with it. Which means the code should be pretty solid. No way you would go ahead submitting something working but halfway through, or something that is in the process of being formed, in transition, work in progress.

That's bad. I found myself spending several days forming my ideas regarding how I can possibly specify binary output format in JSON, so that the format can be sent From Above to the client when requirements change (say, a new format is eventually implemented by busy/lazy server guys). If I had to submit a fully-implemented, fully thought-out, neat-looking code, it would take a couple of weeks. Thinking, prototyping, discussing, including three days of explaining how the stuff works and what JSON is, and why it is okay to use strings as keys, etc.

That's about pair programming too. Imagine pair theorem proving. Two guys are placed together by a senior mathematician, say, Grisha and Misha, and told to prove a theorem by the end of the week.

What I want to say: get the fuck off programmers' backs. If they want to work together, let them work together. If they want to work alone, let them work alone. If they want to be agile, let them be agile; if they want to be locally-convex, let them be locally-convex. On the other hand, if you, the manager, know better how to write code, how come you cannot produce in a week anything comparable to what a junior programmer can easily concoct in 30 minutes? Just kidding.

Now ascii art. Programming is art. Ascii art is a part of programming art. If a programmer thinks that his or her code reads better formatted the way the programmer formatted it, challenge this, the fact that it is, not the fact that it does not follow Coding Style Guide Laws.

Monday, March 08, 2010

A Brief History Of Single Exit

Many many years ago people were writing their code mostly in FORTRAN, but also in PL/I. They were told by their teachers not to use too many functions or subroutines, because each call and return is very expensive, compared to plain goto statement.

So the brave programmers managed to write functions or subroutines several thousand lines long; these people were considered smart and very important, compared to the junior kind who only could write a hundred or two lines in one function or subroutine.

Then something bad started happening: the code did not work. Or it did work until you start changing it. As a result, two philosophies were born:
1. Do not change anything;
2. Write structured code.

Structured programming consisted of using functions of reasonable sizes with reasonable structures. No jumps into the middle of a loop, no jumps out of loops into another loop or into a conditional statement; no exits out of the middle of your subroutine.

Then, later, it was discovered that it is just goto statement that should be blamed. So people started setting limitations, depending on their taste and creativity.

- do not goto inside another subroutine;
- do not goto into a loop or a condition;
- do not goto upstream.

The idea of totally abandoning goto was considered too extremist: how else can we make sure that we have only one exit out of a subroutine or a function?

Well then, why do we need just one exit? There were two reasons:
- it was really hard to set breakpoints on all the exits scattered over half a thousand lines;
- how about releasing resources, like closing files, etc?

So it was decided, more or less unanimously, that we have to a) maintain some kind of "response" or "result" code, and b) goto the bottom of our subroutine and exit from there, using the "result code" to decide whether we should do something to close up our activity.

Since later goto was more and more discouraged (although you can find a goto in Java libraries source code), the kosher solution was suggested that was keeping some kind of integer shitLevel flag; everywhere in your code you are supposed to check the level, and if it is close to the fan, you should proceed without doing anything.

This ideology penetrated into Pascal, C, C++, and, later, Java. And only later people started thinking about structuring their code better.

Like making it smaller.

Besides, some languages have finally block that can be used to neatly close all the streams that may remain open.

These two changes, much smaller code and finally block make "single exit" ideology meaningless. Why does one need a specific variable to pass around if we can just return it? If the whole method is half a screen, is it really hard to find other exit points? Is not it safer to use finally that will release your resources in any case, as opposed to that bottom of the method that may never be reached. Just look at this:

public final static void doit() {
try {
throw new NullPointerException("npe");
} finally {
System.out.println("Finally!");
}
}

Here is basically the same argument, specifically for Java.

Wednesday, January 20, 2010

Dispatch by Return Type: Haskell vs Java

If you are a Haskell programmer, this is all trivial for you; but if you are a Java programmer, you would ask yourself two questions:
  • is it possible?!
  • is it safe?!
Let's start with Java. In Java, we have pretty nice polymorphism which includes method overloading: using the same method name with different lists of parameters:

  • int length(Iterable i);
  • int length(Collection c);
  • int length(String s);
  • int length(T[] array);


Not that we need these specific methods, but for the sake of argument. What happens when compiler/JVM finds the right method to call: it finds the method that matches best the list of parameters, and in the case of confusion will either show an error message or (during runtime) throws an exception.

One thing is impossible, though: defining two methods that differ only in return type, something like

  • int parse(String source);
  • long parse(String source);
  • boolean parse(String source);

In principle, we could, in most cases, deduce which method we want, by the context: if we write

int n = parse("123");

the compiler could guess, of course, what exactly we mean... but no, it is not allowed.

So, a Java programmer, given a method name, expects to always get the same return type (even if signatures are different, we are used to expecting the same return type anyway).

Now, how about generics? What if we define
interface Ubiq {
T parse(String s);
}

then implement the interface and apply it to the strings?

Now we have a problem. If we define

class UbiqInt implements Ubiq<Integer> {
...
}

then we explicitly specify the type, and will be forced to write

int n = ubiqInt.parse("12345");

then all the polymorphisms is gone now.

What if we define a class that is still parameterized by T?

class UbiqImpl<T> implements Ubiq<T> {
...
}

Then the question is, how exactly can we have several different implementation of parse(String) in one class? We cannot, and we are stuck.

Now, what is different in Haskell that makes it possible? Let's take a look at Haskell code:

class Ubiq a where
parse :: String → a

instance Ubiq Bool where
parse ('T':cs) = True
parse _ = False

instance Ubiq Integer where
parse ('0':cs) = 2 * parse(cs)
parse ('1':cs) = 2 * parse(cs) + 1
parse _ = 0

check :: Bool → Integer → String
check b n = if b then show n else "no nothing"

tryme = check (parse "Tautology") (parse "1001")


What happens here? We defined a typeclass Ubiq, which is a vague analog of Java interface; and then we have a couple of implementations. But both implementations define known types, Integer and Bool to be implementing Ubiq. So that, from now on, if we have an expression parse(String) in a position where is expected to have an Integer type, then the compiler finds the appropriate implementation and "calls" it when needed. How does it happen? We just know the expected return type, so it is not hard to figure out. In cases when the compiler is confused, like in an expression show(parse("something")), the compiler will need a hint:
*Main> let x = parse("T")

:1:8:
Ambiguous type variable `a' in the constraint:
`Ubiq a' arising from a use of `parse' at :1:8-17
Probable fix: add a type signature that fixes these type variable(s)


(please do not hesitate to write your comments, questions, objections)

Monday, November 30, 2009

Subclass and Subtype in Java

Here I just want to get together a pretty much widely-known information; somehow it escapes you if you just read Java books or google the internets. And what I was looking for was an example (hence a proof) that subclassing in Java is not always subtyping, or some kind of proof that it is.

I am talking specifically about the state of affairs in Java. We may try to do the same trick in Scala; my point here though was to have a real-life, although contrived, example of how subclassing is different from subtyping, and Java is a easy target.

First, definitions (informal, as well as the rest of this post).

Types in Java.
Java has the following kinds of types:
  • primitive (e.g. char)
  • null
  • interfaces (declared with interface keyword)
  • classes (declared with class keyword)
  • array (declared with [square brackets])
  • type variables (used in generics)

Subclassing: declaring one class to be a subclass of another (class ... extends ...) - this allows a subclass to inherit functionality from its superclass

Subtyping: A is a subtype of B if an instance of A can be legally placed in a context where an instance of B is required. The understanding of "legally" may vary.

Many sources state firmly that in Java, a subclass is always a subtype. Opinions that a subclass is not always a subtype are also widespread; and that's obviously true for some languages: Self type is a good source of subclass not being a subtype confusion; we do not have Self type in Java.


In Java 5 a covariant return type inheritance was added: if class A has a method that returns X, and its subclass B declares a method with the same name and parameter list (meaning, parameter types), and returning a subclass of X, then this method overrides the method in A.

In addition to this, arrays are also covariant: if A is a subtype of B, then A[], in Java, is a subtype of B[].

This last feature allows us to create an example showing that no! Subclasses in Java are not always subtypes! See:





public class Subtyping
{
interface A
{
A[] m();
void accept(A a);
}

interface B extends A // subtype of A
{}

public static void main(String[] args) {
A a = new AImpl(); // see AImpl below
B b = new BImpl(); // see BImpl below
// now note that B is a subtype of A.
a.accept(a); // this works; substitution is trivial
b.accept(a); // this works too (substitution is trivial too)
a.accept(b); // oops, this fails! b, being a subtype of a, is not accepted at runtime
}

static class AImpl implements A {
public A[] m()
{
return new A[]{this};
}

public void accept(A a)
{
a.m()[0] = this;
}
}

static class BImpl extends AImpl implements B{
public B[] m()
{
return new B[]{this};
}
}
}


So there, this code demonstrates a subclass that is not legally a subtype. By 'legally' here I mean that the code always throws a Java runtime exception without adding any client precondition predicates.



Here's a good discussion of this issue:

public boolean lspHolds(Object o) {
return o.toString().contains("@");
}

Monday, November 16, 2009

Not Just Subtyping



I've been trying to figure out how come the only relationship between types we use to encounter is "sub". Type a is a subtype of type b. Validated by subsitution principle.

If we limit ourselves with "sub", we'll have infinite arguments on whether a square can be considered as a subtype of rectangle; whether a colored-point can be considered a subtype of point; whether an int can be considered, under certain conditions, as a subtype of float; whether, in Java, if A implements B, A is a subtype of B. Opinions differ.

I think we should look deeper and maybe consider this case by case.

  1. Is square a rectangle? Seems so; the objection being that when we start stretching the rectangle, not every square remains a rectangle. Modification is a weird thing. Even in simple cases, i = 1, then (i == 1) becomes true; but it is not actually true, because next moment i = 2, and the expression is false. No temporal logic transforms true into false, there's something wrong there. But if we discard modification, we can state this: each square 'is a' rectangle. We have an injection. Two different squares treated as rectangles remain different.
  2. Is colored-point a point? This is a totally different case. The world of colored-points is different from the world of points: it is bigger. Yes, a colored-point can be used instead of a point in a substitution. So, in a sense, it 'is a' point. But two different colored-points can become the same point if we forget about their color. Each point 'is a' projection of a colored-point, and eachcolored-point can be treated as a point. So what we have here is a projection here.
  3. Let's try to implement an unordered-pair. We can do it by taking a pair type and then defining equality in such a way that (a, b) == (b, a). Again, we have a projection, but in this case we went the other way around: not building a new type by adding a dimension, but discovered a new type by defining an equivalence relationship between pairs. So what we have here is a factorization.
  4. In the case of int -> float, we have a more general case. Not all operations are preserved; not all floats come from ints, and not all two different ints map to two different floats. Still, it is a legal type transformation, done usually by default, called coercion.
  5. In Java-like languages, if a class implements an interface, it thus declares that it can be used in any context where the interface is required. It projects itself into the realm of the given interface, and that's all we know; the "true nature" of the class implementing an interface remains obscure.
  6. In the context of 5., the Java keyword "extends" is meaningless. That is, in reality it has many meanings: "borrows the functionality", "implements the same set of interfaces", "has access to internal namespace". Non of this has anything to do with types relationships.
  7. 'is a' actually has many meanings too. We probably never can be sure whether A 'is a' B: we should always ask: "in which contexts" (that is, "what do you mean?"). If we look at this:
the pyramid here is neither a square nor a triangle. But when projected, it can be percieved as one. If we say "he's a soldier", it does not mean that's all the person is; what we mean is just a projection.




So, how about substitution? We can substitute A with B if we know the mapping that maps B into the context where A should be present. If we are talking about coercion (and we know that an int is not a subtype of float), for instance, we can substitute a float with an int value if coercion is legal. In this and other cases, our ability to substitute means we know a canonical mapping.

Now examples.

  1. Injection. Take types A and B; build A+B, a union. Some languages support unions, some don't. Some support them implicitly, like Scala with its case classes. By definition, there are canonical inclusions from A and B into A+B; so it would be logical to call A and B subtypes of A+B.
  2. Projection. Take types A and B, and their product, A×B. One can represent A×B as the type of pairs (a, b), with a of type A and b of type B. There are two projections from A×B to A and B. Neither A nor B can be seriously called a subtype of A×B, of course. They can be considered as a special case of factor-types. Below is another example of factor-type.
  3. Surjection. Given A×A, a type of pairs (a1, a2), we can build a type of unordered pairs by equalizing (a1, a2) with (a2, a1). This gives us an equivalence relationship, and a projection from A×A to A×A /2, the type of unordered pairs.
  4. Enum surjection. Suppose we build an enum class for Rainbow. It turns out in different cultures the number of colors is different. In China, Japan, Russia, there are seven colors, while in some other countries (US for instance) there are 6. Two colors, light-blue and dark-blue, in Asian rainbow, both map to just blue in US rainbow. So every time we pass a US rainbow instance to a function, we can as well coerce an Asian rainbow ("substitute") into US version, using the standard mapping. It is similar to projection, where the receiving side has no clue about the hidden multiplicity of possible parameter values.


In computer science there is a variety of terms that are supposed to denote this variety of "-typing", but somehow they either are all called kinds of subtyping or declared not to belong to the "-typing" realm. I suggest to apply pretty simple categorical notions, so that things just look simpler and more manageable.

Monday, August 31, 2009

a sample comonad

Comonads still look a little bit enigmatic to programmers; I'm going to show a practical example from which one can start perceiving the notion.

First, definition. A comonad is dual to monad; which may or may not be a good explanation. So, okay, a formal definition.

A comonad is a functor T: AA

εx: T(x) → x

and

Δx: T(x) → T(T(x))

together with three conditions similar to monadic conditions:

a) For Δx: T(x) → T(T(x)) and εT(x): T(T(x)) → T(x) we should have εT(x) ° Δx = IdT(x)

b) For Δx: T(x) → T(T(x)) and T(εx): T(T(x)) → T(x) we should have T(εx) ° Δx = IdT(x)

c) For Δx: T(x) → T(T(x)), ΔT(x): T(T(x)) → T(T(T(x))), T(Δx): T(T(x)) → T(T(T(x))) we should have T(Δx) ° Δx = ΔT(x) ° Δx

Here's a nice compact comonad implementation in Haskell; I hope the author won't mind my quoting the code:

class Functor w => Comonad w where
extract :: w a -> a
duplicate :: w a -> w (w a)
extend :: (w a -> b) -> w a -> w b


So, in this notation, the axioms will look like this:

extract . duplicate == id
fmap extract . duplicate == id
duplicate . duplicate == fmap duplicate . duplicate


The author of the code also specifies axioms for extend, but I find it superfluous; it is enough to have functoriality and the comonad laws actually.

I wanted to bring a good example of comonad. Here how one could be produced.

If we have a monoid M, we can have a comonad of functions from a given M to sets. A monoid is a... okay, a set that has associative multiplication and unit defined: 1: → M, m: M×M → M, such that m(a, 1) = m(1, a) = a.

So, let's take the functor which to each set X maps a set of functions from a given monoid M to X. It is known to be a functor; now, how come functions from a monoid to a set form a comonad? I would not go into details here, and will just demonstrate how we have a comonadic structure for one specific monoid, ℕ, the monoid of natural numbers: [0..∞).

So what we have is a functor that, given a set X, builds the set of all sequences in X. I plan to demonstrate that this functor is a comonad.

X ↦ {(x0, x1, ...)}

We need to define εX (extract and Δx (duplicate).

εX can be defined like this: εX(x0,...) is x0;

Why so? A general definition of extract for the case of monoid is taking f(0) for a function f: M → X (a composition 1 → M → X ).

and Δx can be defined like this: Δx(xi,j) = xi+j

Again, this is because T(T(X)) in our case is the set of functions M → M → X, which is equivalent to the set of functions from M×M → X. For each f: M → X we can define M×M → M → X by composing the monoid multiplication (which is addition if we are talking about natural numbers) and f.

Or, in other words, duplicate (x0, x1, ...} == ((x0, x1, ...), (x1, x2, ...), ...); (extract . duplicate) (x0, x1, ...) will return the first element, (x0, x1, ...), that is, it is the same as id.

If we apply fmap extract to ((x0, x1, ...), (x1, x2, ...), ...), we will get a sequence of first elements of each sequence, that is, again, (x0, x1, ...).

Conclusion

In my view, Haskell community, probably for the sake of being closer to the people, oversimplifies IO.

In my view, while output is a monad, input can be interpreted as a comonad. When a machine is taking input, it has no control over external environment, it just consumes; the input acts on the machine. To make the input comonad look like a monad, the authors use tricks, forcing the whole evaluation happen inside not the main Haskell category, but its image under a certain functor... but I don't think this is the right place and time to discuss adjoint functors here.


Tuesday, June 23, 2009

Why Monoids?

I sincerely plan to explain in simple terms what's all this fuss about monoids, why we suddenly need these primitive structures, and how to make them available in Java.

A monoid is one of the simplest notions of algebra. Slightly oversimplifying, it consists of elements that have a multiplication operation a*b defined on them, and a neutral element e, such that e*a == a*e. Multiplication should be associative (a*b)*c == a*(b*c), but not necessarily commutative (a*b != b*a). If you can't imagine non-commutative multiplication, think of matrices... or of spatial rotations. The order counts.

A simpler example would consist of integer numbers and addition playing the role of multiplication. 0 is the neutral element with respect to addition, so there.

Now why would we need this structure? It turned out that if you have to add up a billion, or a quadrillion of integers, you may be interested in doing it by distributing the operation over several (or ~700 000, in the case of Google) machines. Adding up a quadrillion of integers may be not that interesting; but multiplying a billion of matrices is a different, and more challenging, story.

And why can we distribute it among the thousands of computers? We can do it all thanks to the associativity. (m1*m2*...*mk1*mk1+1*mk1+2..*mk2*...*mn) is the same as
(m1*m2*...*mk1)*(mk1+1*mk1+2..*mk2)*(...*mn), and we can calculate intermediate results (shown in parentheses here) on different machines, then aggregating them together; we can do it in cascade, whatever we choose. The strategy does not influence the result.



The following Java class defines, or rather declares the necessary functionality:
public abstract class Monoid<X>
{
abstract X unit();
abstract X m(X x, X y);

public X fold(Iterable<X> source) {
X result = unit();
for (X x : source) {
result = m(result, x);
}
return result;
}

public X fold(X[] source) {
X result = unit();
for (X x : source) {
result = m(result, x);
}
return result;
}
}
We can use it to add numbers, strings, matrices; to multiply numbers or matrices; to concatenate lists and join sets.
Monoid<Set<T>> setMonoid = new Monoid<Set<T>> {
public Set<T> unit() {
return Set<T>.EMPTY;
}

public Set<T> m(Set<T> a, Set<T> b) {
Set<T> c = a.clone();
c.addAll(b);
return c;
}
Of course using all this for the data that we have in memory of one single machine. But, as I said before, we can actually delegate the monoid's fold operation to the computing cloud, and have the list deployed somewhere in the big file system, and let the cloud partition it. The result will be the same; and all this due to the monoidal properties of our concrete classes and operations.

Followers

Subscribe To My Podcast

whos.amung.us