Mont is a Category

I've had a lot of thought about Mont. (Sorry for the rhymes.) Mont, recall, is the set of all Monte objects. I have a couple interesting thoughts on Mont that I'd like to share, but the compelling result I hope to convince readers of is this: Mont is a simple and easy-to-think-about category once we define an appropriate sort of morphism. By "category" I mean the fundamental building block of category theory, and most of the maths I'm going to use in this post is centered around that field. In particular, "morphism" is used in the sense of categories.

I'd like to put out a little lemma from the other day, first. Let us say that the Monte == operator is defined as follows: For any two objects in Mont, x and y, x == y if and only if x is y, or for any message [verb, args] sendable to these objects, M.send(x, verb, args) == M.send(y, verb, args). In other words, x == y if it is not possible to distinguish x and y by any chain of sent messages. This turns out to relate to the category definition I give below. It also happens to correlate nicely with the idea of equivalence, in that == is an equivalence relation on Mont! The proof:

  • Reflexivity: For any object x, x == x. The first branch of the definition handles this.
  • Symmetry: For any objects x and y, x == y iff y == x. Identity is symmetric, and the second branch is covered by recursion.
  • Transitivity: For any objects x, y, and z, x == y and y == z implies x == z. Yes, if x and y can't be told apart, then if y and z also can't be told apart it immediately follows that x and z are likewise indistinguishable.

Now, obviously, since objects can do whatever computation they like, the actual implementation of == has to be conservative. We generally choose to be sound and incomplete; thus, x == y sometimes has false negatives when implemented in software. We can't really work around this without weakening the language considerably. Thus, when I talk about Mont/==, please be assured that I'm talking more about the ideal than the reality. I'll try to address spots where this matters.

Back to categories. What makes a category? Well, we need a set, some morphisms, and a couple proofs about the behavior of those morphisms. First, the set. I'll use Mont-DF for starters, but eventually we want to use Mont. Not up on my posts? Mont-DF is the subset of Mont where objects are transitively immutable; this is extremely helpful to us since we do not have to worry about mutable state nor any other side effect. (We do have to worry about identity, but most of my results are going to be stated as holding up to equivalence. I am not really concerned with whether there are two 42 objects in Mont right now.)

My first (and, spoiler alert, failed) attempt at defining a category was to use messages as morphisms; that is, to go from one object to another in Mont-DF, send a message to the first object and receive the second object. Clear, clean, direct, simple, and corresponds wonderfully to Monte's semantics. However, there's a problem. The first requirement of a category is that, for any object in the set, there exists an identity morphism, usually called 1, from that object to itself. This is a problem in Monte. We can come up with a message like that for some objects, like good old 42, which responds to ["add", [0]] with 42. (Up to equivalence, of course!) However, for some other objects, like object o as DeepFrozen {}, there's no obvious methods to use.

The answer is to add a new Miranda method which is not overrideable called _magic/0. (Yes, if this approach would have worked, I would have picked a better name.) Starting from Mont-DF, we could amend all objects to get a new set, Mont-DF+Magic, in which the identity morphism is always ["_magic", []]. This neatly wraps up the identity morphism problem.

Next, we have to figure out how to compose messages. At first blush, this is simple; if we start from x and send it some message to get y, and then send another message to y to get z, then we obviously can get to x from z. However, here's the rub: There might not be any message directly from x to z! We're stuck here. Unlike with other composition operators, there's no hand-wavey way to compose messages like with functions. So this is bunk.

However, we can cheat gently and use the free monoid a.k.a. the humble list. A list of messages will work just fine: To compose them, simply catenate the lists, and the identity morphism is the empty list. Putting it all together, a morphism from 6 to 42 might be [["multiply", [7]]], and we could compose that with [["asString", []]] to get [["multiply", [7]], ["asString", []]], a morphism from 6 to "42". Not shabby at all!

There we go. Now Mont-DF is a category up to equivalence. The (very informally defined) set of representatives of equivalence classes via ==, which I'll call Mont-DF/==, is definitely a category here as well, since it encapsulates the equivalence question. We could alternatively insist that objects in Mont-DF are unique (or that equivalent definitions of objects are those same objects), but I'm not willing to take up that sword this time around, mostly because I don't think that it's true.

"Hold up," you might say; "you didn't prove that Mont is a category, only Mont-DF." Curses! I didn't fool you at all, did I? Yes, you're right. We can't extend this result to Mont wholesale, since objects in Mont can mutate themselves. In fact, Mont doesn't really make sense to discuss in this way, since objects in sets aren't supposed to be mutable. I'm probably going to have to extend/alter my definition of Mont in order to get anywhere with that.

~ C.

Last modified on 2015-07-21 14:33:00

Monte: Types

In type-theoretic terms, Monte has a very boring type system. All objects expressible in Monte form a set, Mont, which has some properties, but not anything interesting from a theoretical point of view. I plan to talk about Mont later, but for now we'll just consider it to be a way for me to make existential or universal claims about Monte's object model.

Let's start with guards. Guards are one of the most important parts of writing idiomatic Monte, and they're also definitely an integral part of Monte's safety and security guarantees. They look like types, but are they actually useful as part of a type system?

Let's consider the following switch expression:

switch (x):
    match c :Char:
        "It's a character"
    match i :Int:
        "It's an integer"
    match _:
        "I don't know what it is!"

The two guards, Char and Int, perform what amounts to a type discrimination. We might have an intuition that if x were to pass Char, then it would not pass Int, and vice versa; we might also have an intuition that the order of checking Char and Int does not matter. I'm going to formalize these and show how strong they can be in Monte.

When a coercion happens, the object being coerced is called the specimen. The result of the coercion is called the prize. You've already been introduced to the guard, the object which is performing the coercion.

It happens that a specimen might override a Miranda method, _conformTo/1, in order to pass guards that it cannot normally pass. We call all such specimens conforming. All specimens that pass a guard also conform to it, but some non-passing specimens might still be able to conform by yielding a prize to the guard.

Here's an axiom of guards: For all objects in Mont, if some object specimen conforms to a guard G, and def prize := G.coerce(specimen, _), then prize passes G. This cannot be proven by any sort of runtime assertion (yet?), but any guard that does not obey this axiom is faulty. One expects that a prize returned from a coercion passes the guard that was performing the coercion; without this assumption, it would be quite foolhardy to trust any guard at all!

With that in mind, let's talk about properties of guards. One useful property is idempotence. An idempotent guard G is one that, for all objects in Mont which pass G, any such object specimen has the equality G.coerce(specimen, _) == specimen. (Monte's equality, if you're unfamiliar with it, considers two objects to be equal if they cannot be distinguished by any response to any message sent at them. I could probably craft equivalency classes out of that rule at some point in the future.)

Why is idempotency good? Well, it formalizes the intuition that objects aren't altered when coerced if they're already "of the right type of object." I expect that if I pass 42 to a function that has the pattern x :Int, I might reasonably expect that x will get 42 bound to it, and not 420 or some other wrong number.

Monte's handling of state is impure. This complicates things. Since an object's internal state can vary, its willingness to respond to messages can vary. Let's be more precise in our definition of passing coercion. An object specimen passes coercion by a guard G if, for some combination of specimen and G internal states, G.coerce(specimen, _) == specimen. If specimen passes for all possible combinations of specimen and G internal states, then we say that specimen always passes coercion by G. (And if specimen cannot pass coercion with any possible combination of states, then it never passes.)

Now we can get to retractability. A idempotent guard G is unretractable if, for all objects in Mont which pass coercion by G, those objects always pass coercion by G. The converse property, that it's possible for some object to pass but not always pass coercion, would make G retractable.

An unretractable guard provides a very comfortable improvement over an idempotent one, similar to dipping your objects in DeepFrozen. I think that most of the interesting possibilities for guards come from unretractable guards. Most of the builtin guards are unretractable, too; data guards like Double and Str are good examples.

Theorem: An unretractable guard G partitions Mont into two disjoint subsets whose members always pass or never pass coercion by G, respectively. The proof is pretty trivial. This theorem lets us formalize the notion of a guard as protecting a section of code from unacceptable values; if Char is unretractable (and it is!), then a value guarded by Char is always going to be a character and never anything else. This theorem also gives us our first stab at a type declaration, where we might say something like "An object is of type Char if it passes Char."

Now let's go back to the beginning. We want to know how Char and Int interact. So, let's define some operations analagous to set union and intersection. The union of two unretractable guards G and H is written Any[G, H] and is defined as an unretractable guard that partitions Mont into the union of the two sets of objects that always pass G or H respectively, and all other objects. A similar definition can be created for the intersection of G and H, written All[G, H] and creating a similar partition with the intersection of the always-passing sets.

Both union and intersection are semigroups on the set of unretractable guards. (I haven't picked a name for this set yet. Maybe Mont-UG?) We can add in identity elements to get monoids. For union, we can use the hypothetical guard None, which refuses to pass any object in Mont, and for intersection, the completely real guard Any can be used.

object None:
    to coerce(_, ej):
        throw(ej, "None shall pass")

It gets better. The operations are also closed over Mont-UG, and it's possible to construct an inverse of any unretractable guard which is also an unretractable guard:

def invertUG(ug):
    return object invertedUG:
        to coerce(specimen, ej):
            escape innerEj:
                ug.coerce(specimen, innerEj)
                throw(ej, "Inverted")
            catch _:
                return specimen

This means that we have groups! Two lovely groups. They're both Abelian, too. Exciting stuff. And, in the big payoff of the day, we get two rings on Mont-UG, depending on whether you want to have union or intersection as your addition or multiplication.

This empowers a programmer, informally, to intuit that if Char and Int are disjoint (and, in this case, they are), then it might not matter in which order they are placed into the switch expression.

That's all for now!

~ C.

Last modified on 2015-07-04 18:20:00

Communication on Dictionaries

This post is a reaction to and I could not think of a better title.

Before I get into my thoughts, I'd like to quickly recap two arguments presented by two different studiers of communication, as they are essential to my premise.

The first argument is known as "the medium is the message," from Marshall McLuhan. It is, in essence, the concept that the medium in which a message is conveyed is part of the message. "Medium" here is the singular of "media."

The key realization from McLuhan is the idea that, since the message is inalienably embedded in its medium, the process of interpreting the medium is intertwined with interpreting the message. A message restated in a different medium is necessarily a different message from the original. It also means that the ability of a consumer to understand the message is connected to their ability to understand the medium.

The second argument has no nifty name that I know of. It is Hofstadter's assertion, from GEB, that messages are decomposable into (at least) three pieces, which he calls the frame, outer message, and inner message. The frame indicates that a message is a message. The outer message explains how the inner message is structured. The inner message is freeform or formless.

What I'm taking from Hofstadter's model is the idea that, although the frame can identify a message, neither the frame nor the outer message can actually explain how the inner message is to be understood. The GEB examples are all linguistic and describe how no part of a message can explain which language was used to craft it without using the language in question. The outer message is the recognition that the inner message exists and is in a certain language.

I can unify these two ideas. I bet that you can, too. McLuhan's medium is Hofstadter's frame and outer message. A message is not just data, but also the metadata which surrounds it.

Can we talk about Lisp? Not quite. I have one more thing. Consider two people speaking English to each other. We have a medium of speech, a frame of rhythmic audio, and an outer message of English speech. They can understand each other, right? Well, not quite. They might not speak exactly the same dialect of English. They have different life experiences, which means that their internal dictionaries, idioms, figures of speech, and so forth might not line up precisely. As an example, our two speakers might disagree on whether "raspberry" refers to fruit or flatulence. Worse, they might disagree on whether "raspberry" refers to berries! These differences constantly occur as people exchange messages.

Our speakers can certainly negotiate, word by word, any contention, as long as they have some basic words in common. However, this might not be sufficient, in the case of some extremely different English dialects like American English and Scottish English. It also might not be necessary; consider the trope of two foreigners without a common language coming together to barter or trade, or the still-not-understood process of linguistic bootstrapping which an infant performs. Even if the inner message isn't decodable, the outer message and frame can still carry some of the content of the message (since the medium is the message!) and communication can still happen in some limited fashion.

I'll now point out that the idea that "normal" communication is not "limited" is illusory; this sort of impedance mismatch occurs during transmission and receipt of every message, since the precise concepts that a person carries with them are ever-changing. A person might not even be able to communicate effectively with themselves; many people have the surreal, uncanny experience of reading a note which they have written to themselves only a day or two ago, and not understanding what the note was trying to convey.

I would like to now postulate an idea. Since the medium is the message and the deciphering and grokking of messages is imperfect, communication is not just about deciphering messages, but also about discovering the meaning of the message via knowledge of the medium and messenger. To put it shortly and informally, communication is about discovering how others talk, not just about talking.

Okay! Now we're ready to tackle Lisp. What does Lisp source look like? Well, it's lots of lists, which contain other lists, and some atoms, and some numbers. Or, at least, that's what a Lisper sees. Most non-Lispers see parentheses. Lots of parentheses. Lispers like to talk about how the parentheses eventually fade away, leaving pure syntax, metasyntax, metapatterns, and so forth. The language has a simple core, and is readily extended by macros, which are also Lisp code.

I'll get to macros in a second. First, I want to deal with something from the original article. "Think about it: to represent hierarchical data you need two syntactic elements: a token separator and a block delimiter. In S expressions, whitespace is the token separator and parens are the block delimiters. That's it. You can't get more minimal than that." I am obligated to disagree. English, the language of the article, has conventions for semantic blocks, but they are often ignored, omitted, etc. I speak Lojban, which at its most formal has no delimiters nor token separators which are readable to the human eye. Placing spaces in Lojban text is a courtesy to human readers but not needed by computers. Another programming language, Forth, has no block delimiters. It also lacks blocks. Also the token separator is, again, a courtesy; Forth's lexer often reinterprets or ignores whitespace when asked.

In fact, Lisp's syntax is, well, syntax. While relatively simple when compared to many languages, Lisp is still structured and retains syntax that would be completely superfluous were one to speak in the language of digital logic which computers normally use. To use the language from earlier in this post, Lisp's syntax is part of its framing; we identify Lisp code precisely by the preponderance of parentheses. The opening parenthesis signals to both humans and computers alike that a Lisp list is starting.

The article talks about the power to interleave data and code. Code operates on data. Code which is also data can be operated on by metacode, which is also code. A strange loop forms. This is not unlike Hofstadter's suggestion that an inner message could itself contain another outer and inner message. English provides us with ample opportunities to form and observe such loops. Consider this quote: "Within these quotation marks, a new message is possible, which can extend beyond its limits and be interpreted differently from the rest of the message: 'Within these quotation marks, a new message is possible.'" I've decided to not put any nasty logic puzzles into this post, but if I had done so, this would be the spot. Mixing metalevels can be hard.

I won't talk about quoting any longer, other than to note that it's not especially interesting if a system supports quoting. There is a proof that quines are possible in any sufficiently complex (Turing complete, for example) language.

Macros are a kind of code-as-data system which involves reflection and reification, transforming code into data and operating on it before turning the data back into code. In particular, this permits code to generate code. This isn't a good or bad thing. In fact, similar systems are seen across the wider programming ecosystem. C has macros, C++ has templates, Haskell has Template Haskell, object-based systems like Python, Ruby, and JS have metaclass or metaprototype faculties.

Lispers loudly proclaim that macros benefit the expressive power of their code. By adding macros to Lisp code, the code becomes more expressive as it takes on deeper metalevels. This is not unlike the expressive power that code gains as it is factored and changed to be more generic. However, it comes at a cost; macros create dialects.

This "dialect" label could be borrowed from the first part of this post, where I used it to talk about spoken languages. Lispers use it to talk about different Lisps which have different macros, different builtin special forms, etc. Dialects create specialization, both for the code and for those reading and writing the code. This specialization is a direct result of the macros that are incorporated into the dialect.

I should stress that I am not saying that macros are bad. This metapower is neither Good nor Bad, in terms of Quality; it is merely different. Lisp is an environment where macros are accepted. Forth is another such environment; the creator of Forth anticipated that most Forth code would not be ANS FORTH but instead be customized heavily for "the task at hand." A Forth machine's dictionary should be full of words which were created by the programmer specifically for the programmer's needs and desires.

Dialects are evident in many other environments. Besides Forth and Lisp, dialects can be seen in large C++ and Java codebases, where tooling and support libraries make up non-trivial portions of applications. Haskellers are often heard complaining about lenses and Template Haskell magic. Pythonistas tell horror stories of Django, web2py, and Twisted. It's not enough to know a language to be effective in these codebases; it's often necessary to know the precise dialect being used. Without the dialect, a programmer has to infer more meaning from the message; they have to put more effort into deciphering and grokking.

"Surely macros and functions are alike in this regard," you might say, if you were my inner voice. And you would be somewhat right, in that macros and functions are both code. The difference is that a macro is metacode; it is code which operates on code-as-data. This necessarily means that usage of a macro makes every reader of the code change how they interpret the code; a reader must either internalize the macro, adding it to their dictionary, or else reinterpret every usage of the macro in terms of concepts that they already know. (I am expecting a sage nod from you, reader, as you reflect upon instances in your past when you first learned a new word or phrase!) Or, to put it in the terms of yore, the medium is the message, and macros are part of the medium of the inner message. The level of understanding of the reader is improved when they know the macros already!

How can we apply this to improve readability of code? For starters, consider writing code in such a way that quotations and macro applications are explicit, and that it is obvious which macros are being applied to quotations. To quote a great programmer, "Namespaces are one honking great idea." Anything that helps isolate and clarify metacode is good for readability.

Since I'm obligated to mention Monte, I'm going to point out that Monte has a very clever and simple way to write metacode: Monte requires metacode to be called with special quotation marks, and also to be annotated with the name of the dialect to use. This applies to regular expressions, parser generators, XML and JSON, etc.; if a new message is to be embedded inside Monte code, and it should be recognized as such, then Monte provides a metacode system for doing precisely that action. In Monte, this system is called the quasiliteral system, and it is very much like quasiliteral quoting within Lisp, with the two differences I just mentioned: Special quotation marks and a dialect annotation.

I think that that's about the end of this particular ramble. Thanks.

~ C.

Last modified on 2015-05-07 14:46:00

Valid CSS!