Denotational Programming and Real Life

I just watched a pretty interesting lecture called "Inventing on Principle", http://vimeo.com/36579366. The lecturer presents the idea that inventors should have a principal in their work, something like what artists may develop for their work. The principal of the speaker is that ideas are important, and that the creative process requires immediate interaction with their work- without which ideas often die. As example he shows some nicely interactive programs where things that are interacted with in the static medium of text are given an image to play with in the form of an image in one program, a game in another, and a bunch of variable assignments for a binary search. One of the cool ones was investigating a circuit an seeing its properties change in "real-time".

One thing that strikes me about this is the particular implementation is that it seems to rely on state. Certainly, there is a notion of state in animation and games, there is a notion of state in imperative programming, and even the physical experience of the computer (its changing state in time). This brings up a possible weakness of the denotational/declarative programming that I love so much. This is similar to my post "A Case for Imperative Reasoning". In that case, his objection was that denotational programming gives up the sometimes vital ability to specify certain aspects of the execution of a program (see "Lazy Functional State Threads" however). Here we have a different problem, which is that declarative programs are in a certain sense static or finished. The reason this is a problem is that we can't interact with it or easily see the steps between the starting program and the result.

It is interesting that the fundamental problem here is one of reasoning. The whole point of declarative programming is that we have well understood principals with which to reason so we can understand ours programs in a way that is impossible in certain languages. One way to look at this problem is that we want to provide at least the tools for reasoning about our programs that we expect in imperative languages without giving up the awesomeness of the declarative tradition.

One thing I want to mention is that in a language like Haskell, we can definitely interact with the environment, and we can create stateful programs, and we can create reactive programs. However, the language may reorder statements in any way, and it is not easy to predict (for me at least) what statements will be evaluated and when. This is also true of something like the type checker, which is similarly opaque. There has been work trying to remove this difficulty, see "Compositional Explanations of Types and Algorithm Debugging of Type Errors", and to adding debugging capabilities to Haskell or at least doing post-mordem traces. In some sense this isn't as much a problem as it is in other languages- in a pure language a piece of functional code never acts strangely or misbehaves- if it works in isolation then it works everywhere for all time. Also, algebraic data structures are normally easy to visualize, and there are programs for drawing them.

Despite the existence of these tools in particular and what seems to be a generally improving exosystem of tools for functional languages in general, this lecturer's ideas may be applicable in some way to pure functional language, and I expect that it would manifest itself differently in Haskell then in, for example, Javascript. Perhaps a term reducer could show a reduction sequence as a tree, or a heap-visualizer (these already exist, btw), or something like the speaker showed, but with the values of bound variables instead of the state of assigned variables, or maybe something much more exotic? I like visualizations of complex things like programs, but for large scale things they are often just pretty pictures- maybe there is a form for something like a stack trace (in languages where you get actually get such a thing) or the heap that is meaningful and could be inspected on a sample input to get feedback on, for example, performance and memory usage?

Spaces in Genetic Algorithms

There are many spaces involved in a Genetic Algorithm- the space of solutions we want to search, the space of representations that are our individuals, the space of values that make up the individuals (the space {0, 1} for bit vector representations), the population as a space (normally a set), the space of populations (the set of all possible populations), and the space of fitnesses (usually R+). Some of the spaces can be ordered in different ways, and often given different distance metrics. Their shape and the mappings between them have complex effect on the run of a GA.

I've been trying to describe Genetic Algorithms in terms of these spaces, so that a GA is a collection of movements in them. Since it is also stochastic, and some movements must be more likely then other in some situations, it seems like movement and sampling from (usually discrete) probability distributions is all there is to a GA. If we can describe GAs this way we may get two nice things: a way of describing and unifying our treatment of different variations (although some may be easier to describe this way), and possibly some obvious generalizations that suggest modifications to GA. There may also have properties that aren't obvious otherwise, although I don't know much about the literature on the formal study of GAs except vaguely that Markov Chains have been used to represent them, so I don't really know how to proceed there.

If nothing else, I like the idea of visualizations of GAs, and this suggests some ways to make them approachable by intuitive descriptions. Its common to talk about the solution space as a landscape with mountains and valleys, but this doesn't really give the whole story at all. This is especially true when the solutions and the individuals are not the same, which is actually very common.

Books Have

I just got some books in the mail: "Categories of Types", "Category Theory", "Types and Programming Languages", "Advanced Topics in Types and Programming Languages". Each one seems pretty amazing, and they cover types from practical implementation to to advanced type systems with lots of nice features, to their category theory interpretations, to pure category theory.

I have a lot to read.

Turing's Cathedral

I've just watched a google talk called Turing's Cathedral, and there was a part I thought was cool enough to record here. The speaker mentions the possibility of different types of computation besides the sequential access of instructions that perform actions.
The problem he mentioned with this approach is that the machines are so fast we need techniques like recursion just to provide enough instructions for them. I never thought about it that way.

Evolutionary Algorithm Framework

I've been trying to come up with some satisfying framework/library for doing evolutionary algorithms and possibly other types of stochastic optimization for a while now. Part of the problem is that the space of possible algorithms is huge and diverse, and its easy to see how any design decision restricts the ability to express certain types of EAs. Another problem is that I've not been very organized about this. To combat the second problem I've decided to record some of my ideas before I forget them.

First off is the structure of the program. Should it be a library, like a set of combinators with which one constructs the desired algorithm? This would be nice, but I think ultimately it would be a bunch of individual libraries of functions to build different types of algorithms. The problem is that there is so much diversity in possible structures that one might use that to be truly general we can't say much at all about the stochastic operators and what structure they require of the population or individuals.

This leads to the second possibility, which is some definition of EAs in particular as a series of constraints. This would mean a class of some sort describing operations necessary to describe an EA. Part of the problem there is that it is hard to see what these really are, and how they are used to build an EA. This is true for two reasons that I've seen, the main one being state. Its hard to say what state will be necessary, and every algorithm might need slightly more or less than any other. The other reason is that even within GAs its hard to exactly specify the general concept of mutation, for example. It can mean several different things in different techniques, and the more general the definition the less it really says. This line of thinking always leads me to ideas that don't really help the user at all. They say the more abstract you go the more work you need to do to get something concrete, and I agree.

The other idea is to be more explicit about what I want, rather then getting caught up in generality. This would mean defining what I believe an EA really is, and then working on that problem instead, where hopefully the extra structure gives some inspiration. So what does an EA consist of? I'm my ponderings I have often thought that it is important to separate the parts out as much as possible to prevent unnecessary couplings between them. For example, the individuals should not "know" how to mutate themselves, in the sense that it shouldn't be part of their structure. One problem with that sort of coupling is when you go from, say, a regular GA to a GEP, where there are several mutation operators. Perhaps you could say mutation is the composition of each of the several operators, but this still doesn't help much when you want the same structure to mutate in different ways in different algorithms or different times in an algorithm.

Starting with the notion of a population, what sort of thing do we have? It would be easy to say that a population is a *set* of *lists* (or fixed length vectors) of *symbols*, but there are situations in which all of these things do not necessarily hold. It would be nice to include linear or grid populations, individuals with multiple "domains", and things like number or arbitrary structures rather then just symbols. Instead we might say that populations and individuals are combinatorial species, which is very generic, that they satisfy some predicate (are members of some classes) that describe "enough" structure to do EAs, or that they are members of some specific data type which should be defined to have as many possible structures as possible.

The last idea requires some single type, recursively defined, that covers enough ground to express the usual sort of EAs (I don't expect to cover all possibilities- I'm not sure thats really possible in a single library without generalizing to the point of uselessness). This would be something like "data Structure = R Double | Integer Int | Str String | Linear [Structure] | Pair Structure Structure | None", or something like that.

The idea of doing this with species is always intriguing, but I don't know enough about them to know if this is useful or approachable. This gets at the main problem here, which is that EAs are so general that we really need a general theory of container types to work within. The reason that this is a problem is that such a theory is a subject of study in its own right, and I don't know much about it.

Okay, I guess thats enough of that for now. Sorry about the rambling and aimless post, but I want this to go somewhere eventually, and I need to start researching and organizing my thoughts.

Some Combinatory Logic

I've been very much into combinatory logic recently- both the Illative Combinatory Logic iXi and SKI. This post just records some things I've been thinking about.

First off, the church encoding of natural numbers in SKI. In the lambda calculus 0 = (\f.\x.x) and 1 = (\f.\x.fx). Translated to SKI these are 0 = KI and 1 = S(S(KS)(S(KK)I))(KI). It seems strange that 1 is so complex and 0 so simple, but even though I did the translation from lambda terms to SKI by hand, checking it with an online reducing program (http://pages.cpsc.ucalgary.ca/~nicholss/research/cl_web/cl_web.php) shows that it is correct. I remember from using this translation (the one given on the wikipedia page on combinatory logic) that the terms resulting from these translations will be pretty long. In this case, lets find a term that does the same thing, but is shorter.

To start off, lets look at numbers as a specification. This is often how I start out when trying to define a combinator. For 0 we have 0fx = x, which KI definitely fulfills, and for 1 we have 1fx = fx. It should be pretty clear that I is just as good as S(S(KS)(S(KK)I))(KI) as the term representing 1 as application associates to the left, so Ifx can be written (If)x and reduce to fx. I'm not sure that this generalizes in any way (to give simple terms to each natural), but it is cool that the naturals start out so nicely with KI and I.

I've also been reading more on ""Systems of Illative Combinatory Logic Complete for First-Order Propositional and Predicate Calculus" and I've understood several more pieces. First off, I can see how the G combinator defined as (\x.\y.\z.Zx(Syz)) (I'm writing Z for the letter Xi) is a dependent product. It says that for some types x and y and some term z it gives the type of things that give for all things "a" of type x, the thing za in the dependent type ya. In other words, it points out elements of a dependent type depending on the given term.

I'm still struggling with a couple of things. One is exactly what types are and when they are inhabited, as the notion seems looser than that of a usual type theory. Another thing is the assertive interpretation of terms. For example, implication is given by (\x.\y.Z(Kx)(Ky)). This says that for all "a", if Kxa then Kya. Since Kxa reduces to x and Kya reduces to y, this says that if x then y. The problem I have is that it also seems to say that all true propositions are inhabited by all objects. I can understand this when the type is T (true), the unit type, but it seems odd for an arbitrary proposition. What I have to guess is that this is saying that propositions are truth-valued (possibly related to proof irrelevance?). Then all true statements are the same as the proposition T, which very well may be the case. Unless I'm completely lost, we should be able to take some inhabited type p and say Kp, saying that it is true as an inhabited type is a true proposition. This points out some of my confusion with this system, as my intuitions about what is what don't seem to apply.

I still haven't read through and understood the whole thing, but I'm actually making progress with every reread.

Composition and Concatenative Languages

Two of the most basic things one might do with a function is to apply is to an argument and compose it with another function. Application is a function app:(a->b)->a->b, while composition is compose:(a->b)->(b->c)->a->c.

In Haskell the whitespace character indicates application, so "f a" is f applied to a, and "f a b" is f applied to a, and "f a" applied to b. This works since functions are automatically curried, so if f may have the type A->B->C with a:A and b:B then f a b : C. In a concatenative language, whitespace indicates composition, and arguments such as constants are considered functions, so for example the number 1 is a functions ()->N, a function of no arguments returning a single number. Then an expression "a f" has type ()->A composed with (A->B)->B, resulting in a function of type ()->B.

Interestingly, a concatenative expression can be translated to applicative form very easily- by translating it into a series of compositions of functions that take continuations. I imagine that this would make it pretty easy to typecheck them by translating them to lambda terms and type checking the resulting term. I'm not sure it works out nicely in all cases or in the presence of more complex expressions, so this is an investigation of the concept. The reason I'm skeptical is that I've seen some people discussing the difficulties in typing such languages, so I doubt that putting them in continuation passing style is enough to solve these problems.

I'm particularly interested in either pure functional concatenative language and simple ones that can easily be used to generate code for, say, a microcontroller. The syntax makes it easy to do lexical analysis, the semantics are particularly easy to implement in a forth-style runtime, and more complex runtime systems are possible.

A simple example of a program in a concatenative language would be " 1 2 +" which evaluates to 3. Translating that to a lambda term (using feature like numbers we assume are either added or translate into lambda terms) we could get "(\f.f 1) o (\f.f 2) o (\f.\y.\x.f (x+y))" with "o" as function composition. This expands to "(\z.(\f.f1)((\f'.f'2)(\f''.\x.\y.f''(y+x))z))" if we alpha-convert the symbols "f" to f' and f'' in the second and third term to make them distinct. We could have expanded it differently, but it would have reduced to this. Reducing further requires we give a function as the continuation of this new term. To get it to reduce the best term is one that add the least new informations. As application of lambda terms has a left identity, the identity function (\x.x), this is the term to apply, giving "(\z.(\f.f1)((\f'.f'2)(\f''.\y.\x.f''(x+y))z))(\x.x)" => "(\f.f1)((\f'.f'2)(\f''.\y.\x.(\x.x)(x+y))" => "(\f.f1)((\f'.f'2)(\f''.\y.\x.x+y)" => "(\f.f1)((\f''.\y.\x.x+y)2)" => "(((\y.\x.x+y)2)1)" => "2+1" => "3", which is the intended result.

This translation seems to deal nicely with functions that do not result in single results. A term that is only partially applied like "1 +" results in a function requiring an extra argument. Going the other way, terms like "1 2" result in something that requires something to reduce them, nicely dealing with what is usual implemented as a stack by a function requiring a function to reduce the extra arguments. This only works out so nicely if we curry all functions, which we can do without loss of generality.

To flesh this out, lets define some of the usual terms in these types of languages- terms like dup, drop, swap, tuck, nip, rot. Okay- drop is (\f.\x.f), or K, dup is (\f.\x.(fx)x), swap is (\f.\x.\y.(fy)x), tuck is (\f.\x.\y.((fx)y)x), nip is (\f.\x.\y.fx), and rot is (\f.\x.\y.\z.((fy)z)x).

I'm not sure that this works for some complex terms, but it does seem to deal correctly with things like "quoted" terms, usually written as "'+" indicating the function + as an object to be placed on the stack. Such terms are just like other constants, in this example (\f.f(\y.\x.f(x+y))). This is exactly the "return" or the unit of the continuation monad, which takes an arbitrary term turns it into a continuation, which is of type a->(a->r)->r for a continuation of type r.

Maybe more on this later, especially if it turns out to not work in some situations. The application I'm thinking of here is to either translate such terms into lambda terms and allow Haskell to type check them, or to use them as an exercise in type inference in the nicely familiar setting of the (polymorphic) lambda calculus.