Triples

Do you speak Prolog? When I first learned about it, what felt like the main idea was that every "function" was bidirectional. In another language you would write append(list1, list2), which would return the concatenation of list1 and list2. In Prolog you would write append(list1, list2, result), which would be a three-argument predicate about lists; it would be true if result was the concatenation of list1 and list2.

You could then ask, given list1 and list2, what is result? But you could also ask, given list1 and result, what is list2? Or, given just result, what are the possible combinations of list1 and list2 whose concatenation is result?

So in Prolog, you define a "function" in much the same way as you would in a functional programming language, but you get the inverse of that function for free. I find that cool :-)

Well, now take the framework of unary functions underlying the lambda calculus, which I talked about earlier. Here, every function has only a single parameter, so it's fn(arg). If you do the Prolog thing to that function, you get fn(arg, result), a binary predicate -- a world where everything is expressed in terms of binary predicates, does that sound familiar? :-)

Note that functions can be interpreted as Prolog predicates, but predicates cannot necessarily be interpreted as functions. Given a binary predicate p and an argument arg, p(arg, result) may be true for more than one result. However, p can be interpreted as a nondeterministic function, i.e. a function that returns zero, one, or any number of results. So one way we can look at RDF predicates is as nondeterministic unary functions.

It caused me some trouble to figure out how to map function/argument/result to the subject/predicate/object of RDF. It's clear that the function must be the predicate, but is the argument the subject or the object?

At first, I thought that the argument should be the subject, and the result should be the object. For example, the triple

    15 succ 16.

would say that (succ 15) = 16, i.e., that 16 is the successor of 15. For one thing, N3 uses this convention. For another, sin(0) = 1 seemed more like a statement about zero ("the sine of zero is one") than a statement about one ("one is the sine of zero"), so it seemed appropriate to have zero be the subject of the triple. Finally, triples are conventionally written in the order "subject predicate object," and I liked the correspondence to "input program output."

The only thing that "result function argument" had going for it was that it preserved the order (funcion argument) that is standard in functional programming. I thought the previous points were stronger than this one, and thought that "argument function result" was the better translation.

But then I noticed that an important use for terms is to be the way to write values; for example, the natural number 2 could be written as (succ (succ zero)). So the translation of this term would be the way to say "_:two is the natural number two" in RDF. And the conventions of RDF suggest strongly that _:two should be the subject of such a statement; compare

    _:l rdf:first "foo".
    _:l rdf:rest rdf:nil

It seems to me that the "natural" translation of (succ (succ zero)) to triples would, thus, be

    _:two x:succ _:one.
    _:one x:succ x:zero.

And these triples are in the order (result function argument). Therefore, I'm choosing that order.

In functional programming, the list above would be represented as (cons "foo" nil), which is an abbreviation for ((cons "foo") nil); this would translate to RDF as,

    _:l _:f rdf:nil.
    _:f x:cons "foo".

(Never mind now that the RDF spec does not allow blank nodes to be predicates; we'll just ignore that for the moment.) So in RDF, there are established conventions for multi-argument functions, which are different from those used in the lambda calculus, and which are more useful in the RDF setting, I think.

The two-argument function cons is translated to two functions rdf:first and rdf:next. These are non-deterministic functions, because there is more than one resource with a particular rdf:first and more than one resource with a particular rdf:rest. In a sense, we then take the intersection of the results of these two functions.

This translation doesn't work for every binary function. Consider plus. We have both

    (plus 1 3) = 4
    (plus 2 2) = 4

so we certainly can't write

    _:four x:plusLeft _:one.
    _:four x:plusRight _:three.

because then we'd also have

    _:four x:plusLeft _:two.
    _:four x:plusRight _:two.

and therefore also

    _:four x:plusLeft _:one.
    _:x:plusRight _:two.

which is not what we want.

The RDF community, however, already has a well-known convention to work around this, documented in "Defining N-ary Relations on the Semantic Web: Use With Individuals." Using this translation, we'd have,

    _:four x:plus _:rel1.
    _:rel1 x:left _:one.
    _:rel1 x:right _:three.

    _:four x:plus _:rel2.
    _:rel2 x:left _:two.
    _:rel2 x:right _:two.

So this is what we use for n-ary functions when the "simple" translation doesn't work.

Identity and extensibility

Okay, this is a hairy topic. I wrote something about it, ran into problems, discarded it, ran in circles for a weekend, and still haven't figured it out. Well, what the hell, I'll just write something about it anyway. :-)

What does extensibility mean in the context of RDF? What readily comes to mind is that if I have a FOAF description of a person, and I want to express something more about that person, then I can just create my own property -- foo:annualSalary, say -- and add it to the FOAF file. That's part of the story.

In my previous post, I made the distinction between real-world resources, mathematical objects, and virtual resources. The difference between these is how they come into existence:

• Real-world resources exist already before we talk about them in RDF. We just refer to them, and expect that there is general agreement about what they are. (That's a working illusion, of course: "What is art?") To know whether there is a real-world resource about which particular statements are true, you need to look in the real world. Same for knowing whether two real-world resources are the same.
  
• Virtual resources exist because someone created them in a computer. If a user has created a folder, the system knows that this folder exists. If a user has created a website, a computer can load it through HTTP and thus know that it exists. Knowing whether two virtual resources are the same can (often? always?) be decided inside the computer.
  
• Mathematical objects exist because someone defined what they are. In a sense, a class of mathematical objects (such as the natural numbers) is a virtual resource, because it exists because a user made it exist. Whether two mathematical objects are the same solely depends on their definition.

Now, half of extensibility is being able to add new properties about existing resources; the other half of extensibility is the ability to define new resources. Hmm, it's hard to phrase this generally; let me give you an example. Let's say that you want to write an implementation of a LISP dialect in Fencore, and you represent LISP lists as RDF lists, like this:

    _:a rdf:first "First element".
    _:a rdf:next _:b.
    _:b rdf:first "Second element".
    _:b rdf:next rdf:nil.

Now, some of these lists represent LISP programs that come from some source file, and when something goes wrong during execution, you want to be able to tell the user which source file the code came from in which a bug occurred. Did the list (pr x) come from foo.lisp or from bar.lisp?

    _:a rdf:first lisp:pr.
    _:a lisp:source <foo.lisp>.
    _:a rdf:next _:b.
    _:b rdf:first var:x.
    _:b rdf:next rdf:nil.

    _:x rdf:first lisp:pr.
    _:x lisp:source <bar.lisp>.
    _:x rdf:next _:y.
    _:y rdf:first var:x.
    _:y rdf:next rdf:nil.

But what if RDF lists are defined so that any two lists with the same rdf:first and the same rdf:next are considered to be the same list? Then _:a and _:x are the same list! And therefore, it is true that both

    _:a lisp:source <foo.lisp>.
    _:a lisp:source <bar.lisp>.

(In fact, the RDF and OWL specifications are silent on whether two lists are the same if they have the same rdf:first and rdf:next, I think.)

So an extensible definition of lists would say that for every resource _:f and list _:r, there is at least one list _:l such that _:l rdf:first _:f and _:l rdf:rest _:r, but it wouldn't say that there is only one such list. In fact, it would say that more than one such list may be defined to exist.

We would then usually be talking about "every list with this rdf:first and this rdf:rest," rather about "the one" such list.

But I find it difficult to come up with compelling use cases where this would be very important, so maybe this particular sort of extensibility isn't as important as I thought. I'm not sure yet.

Mathematical objects, real-world and virtual resources

I was writing something about extensible data structures, but then I started referring to this terminology and tried to write it up, but it grew, and this really deserves it's own entry. So in this post I classify resources that RDF can talk about in three kinds: mathematical objects, real-world resources, and virtual resources (stuff that only exists because someone created it in a computer: websites, folders, e-mail addresses).

By mathematical object, I mean something which exists because you define it -- natural numbers, lists, records, B-trees, whatnot. With mathematical objects, if you have the original definition, you can in theory conclude everything about them that can possibly be known about them[*], although it may be hard to find out in practice (such as whether there are infinitely many twin primes).

[*] Due to Goedel's incompleteness theorem, that's in fact not quite true depending on how you define things, but let's not go there.

By real-world resource, I mean something like a person, a country, or a programming language, where we can assume some general agreement about what it is and what is true about it. I.e., something which exists already before we start talking about it, and which we only refer to.

Contrast this to virtual resource, by which I mean something like a website, a folder, or an e-mail address, which exists only because somebody creates it in a computer.

Thinking about virtual resources as a separate category has a couple of important practical advantages. The most important one is that you can assign a unique URI to them, unique meaning that every resource only has one URI, so if two resources have different URIs, you know they're different resources.

You can't do that with real-world resources: who would assign the URIs? Having someone assign URIs to people such that one person wouldn't be identified by more than one URI, for example, would cause unacceptable centralization. So we just have to accept the fact that when Alice talks about person 1 and Bob talks about person 2, we don't automatically know that person 1 and person 2 are not the same person.

But with virtual resources, you can make assigning a unique URI part of creating the resource, and in that case, it is perfectly clear who is responsible for assigning the uniue URI, and there is no centralization. Atom's <id> element is based on this.

I expect that I'll talk more about the three kinds of resources later, e.g. when I get to talk about versioning and Fencore.

No primitive data types: Intuitions about how data is represented in Fencore

The original inspiration for Fencore came from the lambda calculus, combinatory logic, and functional programming. Fencore isn't based on any of these, exactly, and you don't have to understand them before you can understand Fencore, but it is in many ways similar to these systems. In this post, I'll use some concepts from these systems to give you some intuitions about how data is represented in Fenfire. (The reason Fenfire does not actually use these systems is that data structures formulated in them are not very extensible. I'll explain this further in a furture blog post.)

In combinatory logic, everything is described by terms, which are either constants or the application of one term (representing a one-argument function) to another term (representing the function's argument). For example, to represent the natural numbers, you could use two constants: zero and succ (the successor function, taking a natural number n and returning n+1). Application of a function to an argument is usually written (f a). Then, you have,

    0 = zero
    1 = (succ zero)
    2 = (succ (succ zero))

etc. A function F(a,b) with two arguments is represented as a one-argument function f such that (f a) is a function which takes b and returns F(a,b); so F(a,b) = ((f a) b). This is abbreviated as (f a b). So you could represent lists using nil and cons: the empty list is nil, and the list [a]+rest is (cons a rest).

Pure functional programming languages, like Haskell, use this technique for representing data structures, such as lists and trees, but not for natural numbers and characters.

If your programs represent data like this, it becomes much easier to use logic to prove things about these programs; you don't need to introduce special rules for every sort of data you want to represent. (For comparison, look at the formal semantics some researchers have created for languages like Java, if you want to see how much it takes to make your head explore.) As a simple example, you can define addition and multiplication in your language itself

    (add ?x zero)      = ?x
    (add ?x (succ ?y)) = (succ (add ?x ?y))
    (mul ?x zero)      = zero
    (mul ?x (succ ?y)) = (add ?x (mul ?x ?y))

and then prove

    (mul ?x (add ?y ?z)) = (add (mul ?x ?y) (mul ?x ?z))

In fact, using Haskell, you could in theory do that for datastructures like lists -- on paper. If you take a university course about functional programming, be prepared to do that for some examples about as complicated as the one above. The language and compiler don't include tools that would make this sort of thing useful in the real world, though. I'm told that internally, Haskell compilers make use of this sort of reasoning a lot, but it's not exposed at the user level.

So in Fencore, all data is by default stored in a way similar to this (the difference is that it's RDF triples rather than function applications); when that's too slow, you devise some other way to store it, and use the built-in logic that it does the right thing.

For example, when representing numbers in binary, you would first represent binary numbers as terms -- for example, add the constants zeroBit and oneBit, and define a binary number to be a cons/nil list bits. Second, you would tell the computer how the inefficient representation (succ/zero) is defined in terms of the efficient operation (list of bits). Third, you would do some implementation magic to cause the bit lists to be represented as actual blocks of memory, and to cause operations that are primitive in the underlying system (add and mul, say) to be implemented using these primitives.

(The above description ignores the fact that a machine word is limited size and that add wraps around. It would be this simple only if the underlying system supported arbitrarily large natural numbers already. If you wanted to map to int32, you'd first have to state explicitly that this only works for numbers smaller than 2^31.)

So why not just have numbers in the language definition from the beginning on? The most important reason is to keep the language and logic simple; if binary numbers look like they're terms, like everything else, you don't need special rules for them in the logic. Another important reason is to allow the user to add their own "native data types."

A not quite so important reason is that in my humble opinion, having this basic paradigm to unify everything and then breaking that paradigm for a couple of primitive data types is butt-ugly. I can understand doing it for pragmatic reasons, like in Java, but if your underlying paradigm allows you to avoid primitives and still be efficient, like in Fencore, then I see no point in having them.

Quick posts vs. concise posts

I spend a lot of time on my first post on this blog, and I think that's appropriate, because it explains why you should keep reading. I also posted it before I was really happy with it, and I think that's appropriate, too, because if I try to make everything perfect, I'll never get started. (And now don't play smart and tell me that applies to programming language design, too, I know that! ;-))

In particular, the first two paragraphs of the intro try to capture the two basic ideas behind Fencore, but fail to explain how Fencore actually works. I'll just have to say more about that later.

Part of making a good post is making a concise post (that still says what you want to say), and you have all heard the phase attributed to Goethe in the German-speaking world and to Blaise Pascal in the English-speaking one: "I apologize for writing such a long letter; I didn't have time to make it short."

My point being, I will try to make future posts here concise, but I won't let that get into the way of actually getting them posted; so I apologize in advance for writing such long posts.

About this blog (whetting your appetite)

This is a blog about designing a new programming language, Fencore. I tried hard yesterday to concisely write up the most important reasons why in my opinion, you want to be programming in Fencore, and it became a long list. ;-) That made it sounds like Ada, though ("take everything cool and put it into a single language"), which doesn't do the language justice: One of the two basic principles of Fencore is to be a conceptually very simple and pure system (like in the lambda calculus, say), and everything else follows from there.

The other basic principle is extensibility. Not only will the language be extensible at every level, but it will have support for extensible data structures. If you know the Semantic Web, you'll have some idea of what I'm talking about.

Fencore isn't here yet, but it's more than a thought experiment. I hope to have a version one by the end of this month. I have a tendency to understimate the time it takes to design something, though, so let's see. It will be free software when it's published. If you're not interested in hearing about vaporware, we would like to apologize for the inconvenience; please try again later.

Perhaps the main reason for Fencore is that part of it is a logic that allows you to prove things (and have the computer check those proofs) about the programs you're writing, but that it's designed as a comfortable language for hackers, not a framework for writing specification legalese. Why you would want to do such a thing? Here's one of the things I wrote yesterday:

When writing code, you want to make it as powerful as you can, but you also want it to be easy to understand and efficient enough. Fencore will let you write code without caring about efficiency at all. After you have done that, it will let you tell it how the parts that need to be efficient should actually be implemented, and prove that your efficient code actually does the same thing as the easy-to-understand code.

I've often felt in my own work that the simultaneous pressures of making my code powerful, easy to read and efficient have made it less powerful, less efficient, and more complicated than acceptable, really. Thus Fencore.

The weird thing about formal logic is that usually neither logicians nor computer geeks realize that formal logic on computers is both useful and fun. Formal logic allows you to write down why you think that your tree balancing algorithm should work, and have the computer tell you "yes, indeed" or "no, something is wrong with that explanation," making you realize the bug that would have eaten the user's data one in a thousand times. Unfortunately, both logicians and hackers generally believe that you have to write the proofs on a blackboard and check them yourself, leading to proofs that are more likely to be buggy than the programs they are supposed to prove correct.

That's sort of like using an assembler program to tell somebody how to multiply matrices and expect them to flawlessly work out all the register values, and if they make a mistake, conclude that programming languages are useless.

I also think that hackers' opinion of formal logic isn't helped by tools that feel more like Cobol than Python on first impressions.

Well, that's it for now. Fencore is a nice design, but this blog post is too short to contain it. I'll explain it in more detail over the next couple of days; stay tuned.

Fencore is influenced by ideas from mathematical logic, functional and logic programming. Don't be scared by that; I'll try to explain everything along the way that's necessary for understanding what I want to say. As noted above, Fencore is also influenced by and based on the Semantic Web. I hope you won't be scared by that either, but I'll assume some familiarity with RDF.

If you decide to keep reading anyway, welcome.