Oleg's Unusual Polymorphism

I was wandering the internet, and stumbled once again across Oleg's page of O'Caml and other wizardry. One fun example was that of polymorphic selection.

The idea is that we (for whatever reason) want to be able to select data from a heterogenous structure in a particular way. In O'Caml one of our tools for storing such data is a tuple, so we'll take as input a pair of pairs. We want to be able to select either both of the fst elements, or both of the snd, using some function poly along with the selection function (either fst or snd):

    let data = ((1, 2), (3, 4))
        val data : (int * int) * (int * int)
    
    poly fst data
        - : int * int = (1, 3)
    poly snd data
        - : int * int = (2, 4)

So, how do we write poly? Here's our first attempt:

    let poly selector (l, r) = (selector l, selector r)
        val poly : ('a -> 'b) -> 'a * 'a -> 'b * 'b

    poly fst data
        - : int * int = (1, 3)
    poly snd data
        - : int * int = (2, 4)

Success! Or so we hope... but take a look at the type of poly. Not exactly what we were looking for; consider:

    let data' = (("1", 2), (3, "4"))
    
    poly fst data' (* Type error! *)

The essential issue is that, in the definition of poly, we are trying to use selector polymorphically. In ML we can only apply selector monomorphically, that is, to arguments of a single type within the body of poly. We actually want the type of poly to be something like:

    val poly : (forall a. b. (a, b) -> c) -> ((d * e) * (f * g)) -> {d * f when a = c, e * g when b = c}

Or something crazy like that (as Oleg mentioned, even with "real" polymorphism a la System F we cannot type poly the way we would like)... But it turns out that, if we are willing to do a bit of hackery we can get what we want:

    let poly selector (l, r) =
        selector ((fst l, fst r), (snd l, snd r))
             
        val poly : (('a * 'b) * ('c * 'd) -> 'e) -> ('a * 'c) * ('b * 'd) -> 'e

What we've had to do is inline all possible projections that selector can make, so that we can apply it just once (at one type). Incidentally, if you don't like the idea of invoking both fst and snd each time you want just one or the other, you could thunk it:

    let poly selector (l, r) =
        selector (fun () -> (fst l, fst r), fun () -> (snd l, snd r))
             
        val poly : ((unit -> ('a * 'b) * (unit -> 'c * 'd)) -> 'e) -> ('a * 'c) * ('b * 'd) -> 'e

Here you'll have to invoke poly with an extra argument:

    poly fst data' ()
        - : string * int = ("1", 3)

So, that's all just a recap of what Oleg wrote, and which I found quite interesting. But as I looked a bit more, things seemed strange. First, take a look at the type of the first argument to poly:

    val selector : ('a * 'b) * ('c * 'd) -> 'e

What does this mean? It's basically saying that selector can return anything it wants; that is, it's a whole lot less restrictive than the "crazy" type we wanted to write above. So poly works as we'd like when selector is either fst or snd. But its not a whole lot more useful than just writing out the whole thing longhand, as below, because defining any more selectors will require us to understand the internals of how poly operates (and also how our heterogenous data is structured, of course).

    let fst' ((a,b),(c,d)) = (a, c)
        val fst' : (('a * 'b) * ('c * 'd)) -> ('a * 'c)
    let snd' ((a,b),(c,d)) = (b, d)
        val snd' : (('a * 'b) * ('c * 'd)) -> ('b * 'd)

Nevertheless, we have solved the problem that we set out to solve, by first inlining (and thunking) all of the possible projections of our heterogenous data structure, and then applying our selector to the result. Oleg points out that this demonstrates the relationship that inlining has to polymorphism: essentially inlining allows us to "outside" the restrictive type system and check types only after expansion, which means we can seemingly abstract over aspects of a type that the type system itself cannot allow. This is played out to good effect in F# with its notion of inlining and statically resolved type parameters, though of course there the language actually does the inlining for you, and has extended the type system to make sense of it.

So anyway, what happens when we want to apply this to larger structures, perhaps without as much built-in "symmetry"? Let's add some extra data to our structure.

    type 'a 'b 'c 'd 'e heterogenous = ('a * 'b) * ('c * 'd) * 'e
    let poly selector (l, r, extra) = selector ((fst l, fst r, extra), (snd l, snd r, extra))    

So that works, fair enough. But still, it feels like there's something funny about our examples. It's almost like our structure isn't so heterogenous after all. What about this?

    type 'a 'b 'c 'd 'e heterogenous = ('a * 'b * 'c) * ('d * 'e)

Well now, what kind of selectors could we use on this data structure? There really aren't any yet (though of course we can write some). In fact, the only reason that we ran into trouble before is that we didn't want to write selectors for the data at hand, instead opting to try to use existing selectors on different pieces of the structure. We were exploiting some uniformity, some homogeneity, in the structure (namely that there were several pairs in the structure), and in fact we were able to capture this homogeneity using the type system (in spite of it, perhaps) after a fashion. But I wonder: How often you might run into this problem, where you don't, for whatever reason, want to write your own selectors over the structure in its entirety? Consider:

    let fst'' ((a,_,_),(b,_)) = (a, b)
    let snd'' ((_,a,_),(_,b)) = (a, b)
    let thr'' ((_,_,a),(_,_)) = a
    
    let poly selector data = selector data

Here poly just becomes apply, and of course our selectors understand the entirety of the structure. There wasn't any ready-made uniformity in the structure, so we did it all by ourselves. Of course, if could abstract over the length of tuples we would be in business again... Well, enough of that.

Note: I had to run before I could proofread this... apologies.

SKI!

Note: I'm actually not much of a skier, being as I am more interested in sliding sideways...

So, a while ago I was wandering the halls of the internet and came across this fun post, an implementation of the SKI combinator calculus at the type level in Scala. So I asked myself, "would this work in Mix?" The answer is "yes", which causes me a bit of consternation given that I'd like to do type inference for Mix. But anyway, let's have a look.

First, what is SKI? It's a set of combinators S, K, and I, along with rules for evaluating or rewriting them, that happens to be equivalent, in some sense, to the untyped lambda calculus. Evaluating expressions composed of these combinators (and variables x, y, and so on) is pretty simple: I x evaluates to x, K x y evaluates to x, and S x y z evaluates to x z (y z). So, for instance, S K x y evaluates first to K y (x y) by the S rule, and then to y by the K rule. And S K I I evaluates to I by S and then K. Note that we can actually simulate I using, for example, S K K, so we can only consider S and K going forward.

The Scala encoding given in by Michid is fully at the type level. We define several classes: one for each combinator, and a few representing variables. Each class has a "member" type corresponding to application and evaluation. The former is parameterized by an "argument" type. So if we want to construct a type representing I x, and we have defined I and x, we simply access the "application" member type of I, parameterizing it with the type x: Ix = I#apply[x].

Next, if we want to evaluate it (and thereby get back x), we simply access the "evaluation" member type of Ix: x' = Ix#eval.

An important aspect of the implementation given is that it actually performs evaluation as it is possible. By this I mean that any time we try to apply a reducible term t to another s, as in t#apply[s], we first reduce t and only then access the member type of the result of the reduction. So all of the types that correspond to reducible terms have a definition for apply that looks like this:

    type apply[x <: Term] = eval#apply[x]

Apologies for the lack of Scala syntax highlighting.

It first evaluates itself by accessing its own eval, and then applys the argument by accessing apply member type of the result of evaluation, parameterized by x. And it results in types representing terms that, after construction, have only one thing left to reduce.

So, how does this play out in Mix? Quite nicely, in fact, because in Mix we don't need to lift all of our computation into the type level in the same way. In Scala we created part of a class hierarchy (Term, S, etc.) for implementing SKI, the same as we would have if we wanted to evaluate it at runtime. But we didn't write the revelant Apply and Evaluate methods; instead we reflected them as types. In Mix we will implement these methods as usual, and find that the inference algorithm will evaluate our code correctly at compile time. That is to say, we can reflect only our data as types, but implement our functions on that data as methods over instances of types:

    // Base term class with default implementations.
    class Term
    {
        Apply(z) { return new Application(this, z); }
        Eval() { return this; }
        operator+(z) { return this.Apply(z); }
    }
    
    // Applications
    class Application : Term
    {
        var x; var y;
        new(x, y){ this.x = x; this.y = y; }
        ToString() { return "(" + x + " " + y + ")"; }
    }
    
    // Our combinators: partial applications of combinators override
    // Apply; complete applications override Eval as well.
    class K : Term
    {
        Apply(x){ return new Kx(x); }
    }
    
    class Kx
    {
        var x;
        new(x){ this.x = x; }
        Apply(y){ return new Kxy(this.x, y)
        ToString(){ return "(K " + this.x + ")";
    }
    
    class Kxy
    {
        var x; var y;
        new(x, y){ this.x = x; this.y = y; }
        Apply(z){ return this.Eval().Apply(z); }
        Eval(){ return this.y; }
        ToString(){ return "(K " + this.x + " " + this.y + ")";
    }
    
    // And so on for S, Sx, Sxy, and Sxyz, as well as I and Ix.
        
    // Constants have a specialized ToString; we need separate
    // classes so we can distinguish between an Constant("C")
    // and Constant("D") at the type level.
    class Constant : Term
    {
        var name;
        new(name) { this.name = name; }
        ToString() { return this.name; }
    }
    
    class C : Constant
    {
        new() : Constant("C") {}
    }
    
    class D : Constant
    {
        new() : Constant("D") {}
    }

A few comments on the code itself. We use inheritance to build a term hierarchy, as you might find in C# or Java, giving default implementations of Eval and Apply, as well as of operator+ which is implemented in terms of the latter. We also define ToString for printing the results at runtime; note that we frequently make use of the fact that Mix.String.operator+ invokes ToString on its argument.

Next, a few comments on the intentions behind the code. The most important is that we must use a new class for each different constant we want to represent, so that the type of a term actually reflects the structure of the term. That is, when we write var x = new Application(new C(), new D()); we want that they type of x is something like Application<C, D>, written in a C#-like syntax. Next, we also ensure that instances of C and D are different at runtime in their value (that is, what is printed by ToString).

Now we can construct a combinator term and evaluate it. We'll evaluate S K I c to c. Unfortunately we need to ask Mix to print the type of the result of evaluating the term using some "internals", namely the as ? operator, which prints a term's inferred type. Then we print it out, demonstrating that we can evaluate at the type level, but we're also playing with value level data representations.

    var S = new S();
    var K = new K();
    var I = new I();
    var c = new C();
    var d = new D();
    
    Int main(String args)
    {
        var term = S + K + I + C;
        var result = term.Eval() as ?;
        IO.print(string(term) + " => " + result);
        return 0;
    }

When we compile it we would get something like this log message, if I had a prettier pretty-printer for types:

ski.mix(10) : Log : Expression 'term.Eval()' has type 'C'.

And there you have it: type inference (but not type checking, though that doesn't make much sense as we haven't a way to write down types with methods, classes, and so on) in Mix is undecidable. Should we care? Do you?

Note: I haven't actually tested this code in a while, as my current version of Mix is in the midst of a rewrite!

Apologies

Apologies are once again in order. Things have been interesting, but not in a way that you'd enjoy, dear Reader. I use "interesting" in the very loosest of senses. I shall, however, endeavor to provide some sort of commentary on something or other, sooner rather than later.

FLoC

I am presently at FLoC, the "Federated Logic Conference", and hope to post something relevant or interesting for your listening pleasure.

Travelling

I have just now returned from a month-long road trip with the lovely Molly Peppel. Check out her photographs of our trip and more. We now return to your regularly scheduled nerdery.

Infinite Types for Fun and Profit

I stumbled upon this fun post at Stack Overflow. Let me paraphrase the goal: write a function contraption that, when given another function (call this the operator) and an argument x, invokes operator(x), and returns a function that, when given yet another argument y, invokes operator(y), and returns a function that, when given yet another argument z, invokes operator(z), and returns a function that ...

That's kind of a gross definition. What we're looking to do, in ocaml, is the following:

let printer = contraption (print_endline)
printer "Hello" "World" "How" "Is" "It" "Going?"

Clearly this should print 6 lines, with the relevant text. Cool, right? You (kind of) get a function that takes an arbitrary number of parameters of the same type (sort of, because you have to do the same thing to each one). So, how do we write contraption? As follows:

let rec contraption op x =
    let _ = op x in
    fun y -> contraption op y

So, what type does contraption have? Well, this is where things get loose. Run this through ocaml and you get:

# let rec contraption op x =
      let _ = op x in
      fun y -> contraption op y;;
Characters 60-76:
      fun y -> contraption op y;;
               ^^^^^^^^^^^^^^^^
Error: This expression has type 'a -> 'b but is here used with type 'b

What? 'a -> 'b isn't the same as 'b? I guess not, but why not let 'a -> 'b equal 'b? Sure, it's an infinite type, but it seems like everything would work out. Indeed, if we run ocaml -rectypes instead we get the following type:

val contraption : ('a -> 'b) -> 'a -> ('a -> 'c as 'c)

What does this type mean? It says that, "if we give it a function from foo to bar, and a bar, then we get back something of an infinite type". And this infinite type is "if you give me a foo, I'll give you back an infinite type", indeed the same infinite type. And that's just what we want!

So, if everything works fine with -rectypes, why isn't it always turned on? Apparently leaving it on all of the time can get you even worse error messages than ocaml already gives you. Hard to believe, I know, but nevertheless there is indeed a deeper circle of Hell.

To bring it back to Mix, we might wonder if this craziness will work in Mix, and how it will look if it does. Here you go:

contraption(op, x)
{
  op(x);
  return function(y)
  {
    return contraption(op, y);
  };
};

Now, how do we use it?

Int main(String args)
{
  var printer = function(s){ return contraption(IO.print, s); };
  printer("Hello")("World")("This")("Is")("Bizarre");

  return 0;
};

Note that since we don't have currying in Mix we were obligated to build an "extra" anonymous function when creating printer; if we had the placeholder syntax "_" of Scala we could have written it as follows:

Int main(String args)
{
  var printer = contraption(IO.print, _);
  printer("This")("is")("Cleaner");

  return 0;
};

Or, if you prefer we can tweak the definition of contraption slightly instead:

contraption(op)
{
  return function(x)
  {
    op(x);
    return contraption(op);
  };
};

Int main(String args)
{
  var printer = contraption(IO.print);
  printer("This")("Is")("Cleaner")("Still!");

  return 0;
};

And so Mix is victorious (or at least works, after a fashion) once again! And incidentally, we see how nice currying can be.
PS - I definitely need to shorten the function keyword; perhaps just fn?

Paranoid

So, I was reading this over on Slashdot this morning, and it got me paranoid. Okay, it didn't really (maybe). But it reminded me that I've wanted an easy way to randomize my MAC address (mostly for fun, so I can pretend that I'm some kind of super-hacker; honestly, no one is interested in tracking my repeated visits to Lambda the Ultimate) for a while.

It should be fairly clear by now that I prefer to write things myself, rather than use an existing tool (as long as I have time, and I can learn something in the process, and it's not too annoying - give me a god damn break, I'm human).

So, I hacked up a MAC address randomizer in Python in a few minutes. It's pretty gross, hard coding stuff everywhere. But I figured somebody might like it for reference (of how not to code, perhaps). Important note: you must run this as an administrator!

import winreg
import random
import os

# This is the name of the interface we want to change.  This can be
# found using "netsh interface show interface", which will list the names
# of all of your interfaces.
INTERFACE_NAME = "Wireless Network Connection"

# This is the registry key holding the item's address.  Unfortunately it has
# a funny name, not based on the INTERFACE_NAME above; we could probably locate
# this from the INTERFACE_NAME somehow, but this was faster.  You will probably
# have several keys of the form '...\0001', '...\0002', etc.  Be sure to
# pick the right one!
KEY_NAME = r"SYSTEM\CurrentControlSet\Control\Class\{4D36E972-E325-11CE-BFC1-08002BE10318}\0011"
SUBKEY_NAME = "NetworkAddress"
ROOT = winreg.OpenKey(winreg.HKEY_LOCAL_MACHINE, "")

# For some reason Windows 7 requires that the first 2 hexadecimal digits be
# "12".  Also, crappy random number generation.
def generate():
    return ("12%02x%08x" %
      (random.randint(0, 255), random.randint(0, 4294967295)))

# As I couldn't easily find a quick way of enabling and disabling the interface
# using pure Python, so shell it is.
def enable():
    print("Enabling interface...")
    if os.system("netsh interface set interface name=\"%s\" admin=ENABLED"
      % INTERFACE_NAME):
        print("Error: unable to enable interface.")
    return
    
def disable():
    print("Disabling interface...")
    if os.system("netsh interface set interface name=\"%s\" admin=DISABLED"
      % INTERFACE_NAME):
        print("Error: unable to disable interface.")
    return
    
def main():
    try:
        # Here we open up the relevant key for reading and writing values.
        with winreg.OpenKey(ROOT, KEY_NAME, 0,
          winreg.KEY_SET_VALUE | winreg.KEY_QUERY_VALUE) as key:
        
            # No need for this, just for reference; newlines for symmetry.
            (oldMAC, type) = winreg.QueryValueEx(key, SUBKEY_NAME)
            print("Current MAC: %s\n" % oldMAC)
            
            # Make a new key and set it; you can check that it worked using
            # "ipconfig /all" and reading of the adapter's MAC afterwards.
            newMAC = generate()
            winreg.SetValueEx(key, SUBKEY_NAME, 0, winreg.REG_SZ, newMAC)
            winreg.CloseKey(key)
            print ("New MAC: %s\n" % newMAC)
            
            # Reset the interface so it catches our update.
            disable()
            enable()
            print("Done.")
            return 0

    except WindowsError as e:
        # Really bad error handling; if you get 'access denied' you aren't
        # administrator and if you get 'file not found' you probably have the
        # wrong KEY_NAME.
        print("Error: %s" % str(e))
        return -1

exit(main())

Enjoy.

PS - I should confess that all of the comments were added after the fact.

Again with Immutabililty

So, a while ago I was telling all of my ardent readers that things can get kind of crazy when it comes to the question of using "real methods" for operator+= vs. using syntactic sugar.

Turns out I'm not the only person that's been troubled by this kind of a question; Scala programmers have to worry about it, as do the designers of Scala. Have a look at this post over on Stack Overflow.

Master's Thesis

I've finally sent my Master's thesis, "Realizing the Dependently Typed λ-Calculus", out for review. If that sort of thing gets you sweating, feel free to take a look.

Innate Immutabilities

A quick note: at some point when implementing the Mix runtime I had occasion to write the Int class. I think I've mentioned abstract classes before; they act as bindings to .NET classes that exist in the runtime, or in user supplied code (in case you want to use your regular .NET code from Mix, and that code can't be automatically imported using the import statement because the types that you want associated with your code are too complicated for Mix to infer).

Anywho I was writing this class and came across a decision I had made a while ago that caused me to scratch my head. In Mix operators are just method calls, which gives an easy to understand form of operator overloading, whereby an operator invocation is just a method invocation on one of the arguments. Which argument is operator dependent, but I think almost all of them use the left argument, passing the right; of course, single argument operators like ++ are easy.

The decision that I made was to make certain operators "real" operators, not just syntactic sugar. For instance, I made operators ++ and -- real operators, and didn't just expand them from i++; to i = i + 1;. Seems cleaner, actually, to not treat it as sugar, so what's the big deal?

Well, in Mix all expressions are objects -- we've talked about functions being objects, methods being objects, and so on. We also have integers as objects, booleans as objects, and so on (note: I write "and so on" because I don't like the strangeness of punctuating an etc. -- I like putting my punctuation on the outside of parens, it just feels right). Another note: for now I want to ignore the performance implications of this choice, and focus on a clean language design. Another other note: classes themselves aren't objects, unfortunately; maybe in Mix version 2.

So integers are just instances of class Int, and we all love to increment our integers using i++;. So how do we write the .NET class implementing the Mix class Int? First, let's look at the abtract class itself:

abstract class Int
{
  public ToInt(){ return null as Int; }
  public ToString() { return null as String; }
  // More conversion operators...
  
  public operator+(i)
  {
    i.ToInt() as Int;
    return null as Int;
  }
  // More arithmetic operators...
  
  public operator++()
  {
    return null as Int;
  }
  // And anything else...
}

Let's take this in a few bites, my hungry friends. First, the syntax term as Type does two things: at compile time, it just checks that the term has only the given Type, and then returns a typeset containing just Type. At runtime, it does nothing, returning term; in an abstract class, it really does nothing, as class never has any code generated for it. The point of the null as Type idiom is to avoid writing new Int(), because it's not as obvious that it's just for compile time.

Given this description, you should be able to understand the definition of operator+; it checks that its argument is convertible to Int, and then returns an Int; the code to actually perform the addition is found in the .NET class implementing Int:

public class Int
{
  public int NativeInt;
  
  // Lots of methods...

  public operator_add(object other)
  {
    int i = Mix.Call(other, "ToInt").NativeInt;
    return new Int(NativeInt + i);
  }
  
  public operator_incr()
  {
    // What to do?
  }
}

So, in operator_add we invoke ToInt on the passed object and then assume that it worked, and that the result is an Int. We can safely assume these, because the Mix compiler verified that all code is well-typed. This lets us get the native .NET integer, add it to our own, and return a new wrapper with the sum of these two numbers.

Finally we come to the real issue: how should we implement operator_incr. Turns out the obvious way to implement leads to really crazy use cases! Let's say that the body is as follows:

public operator_incr()
{
  int original = NativeInt;
  NativeInt++;
  return new Int(original);
}

Well, that's craziness, because integers are almost always in everyone's minds, immutable. In the following, we pretty much all expect b to be 42:

var a = 42;
var b = a;
a++;

And of course with the above definition it isn't, not even a little. So, leave your integers immutable! But, how can we write the code, allowing for operator++ to be a real live operator? I'm not sure, but I certainly couldn't find a clean way (nor for operator+= and company).

One option is to say that when a class implements operator++ we call it, otherwise we interpret it in the "syntactic sugar style". The nice bit about this is that it also works for operator+= and friends, so we can, for instance, write a list that allows you to append elements to it using list += "new list item!". The problem is that it complicates both the mental model of the code, and also the implementation of the back end.

Maybe someone, somewhere has a thought or three?

Artificial

I remember reading a book by Dan Simmons a long time ago; could have been Endymion or The Rise of Endymion. I've always been a science fiction fan, and the Hyperion series was pretty cool. In this book, whichever one it was, there are artificial intelligences, as tends to be usual for works of science fiction. But what was really interesting to me at the time (must have been 10 years ago, at least) was that, in the book, these artificial intelligences were described as having evolved, in the distant past, from an experiment in evolving programs. The best part was that Simmons actually mentioned an artificial life researcher by name: Thomas Ray, whose work (the Tierra project) I promptly investigated.

Turns out it was The Rise of Endymion; I should read my own links.

I eventually implemented my own little a-life simulator, had fun with it for a while, and then moved on to other things; I'm not a biologist. But recently while on vacation I decided to mess around with it again. I had stumbled across nanopond at some point, and it looked rather neat, so I decided to implement a system based loosely on that project -- it is unimaginatively called "PondLife".

The basic idea behind nanopond, PondLife, and a host of other similar projects is simple: you have a bunch of organisms that consist of some kind of "code", and which can reproduce. And you execute them over and over again. Usually the virtual machine that executes them isn't perfect, and makes mistakes; this leads to mutations. And usually the organisms compete for something (energy, processor time, memory, or other more artificial resources), which leads to a form of natural selection. And so you get evolution.

Nanopond is written in really efficient C, and uses all sorts of twiddling to pack 8 instructions into every int. I decided to implement my system in C# because I long ago lost any desire to program in the hellish twisted misery that is C ever again, you can't make me damnit! Bwaahhh!!!!

Sorry about that. So, not a fan of writing C when I don't have to (although, as we shall see, this could have been one of those times), and I just wanted to get something working immediately, which is easy when you have a huge standard library at your fingertips. Plus, everyone says C# can be just as fast as C, so why not?

Here's the scenario: there's a 2 dimensional grid of "cells", which wraps around like in Asteroids; its a torus. Each cell has a "genome", basically a vector of instructions that are its code. (In nanopond every cell gets the same amount of code; in Pondlife different cells can have different amounts of code). The instruction set is basically that of Brainfuck with a few tweaks: there's a register and a pointer, a cell can increment and decrement the register, and move the pointer forwards and backwards. A cell can read its code into the register, and write the register into the code (that is, PondLife code can self-modify). And there is an "output buffer", again which the cell can write into and read out of. Finally, the cell can "turn", updating the way it is facing in the 2D grid, "kill" a neighbor, or "share" with a neighbor (more on neighbor's in a second).

Every cycle a random cell is selected and executed until it is out of energy. If it has written anything into the output buffer, the buffer is copied into the neighbor's code (where "neighbor" depends on which way the cell is facing). Instructions take energy to execute, so each cell also has its own amount of energy; this is the resource I mentioned. And the instructions don't always go as planned; hence mutation.

A cell can gain energy by killing its neighbor, and from the sun or other operators. See, there are various "operators" that are executed every so often. One is the SunshineOperator, which adds energy to all cells. Another is the SedimentOperator. Remember how I said that each cell can have a different length of code? Well, if you think of that length as the depth of the world, then think of this operator as sediment accumulating beneath living cells. Eventually this sediment can accumulate to the point where the cell doesn't have enough room for its replication code, and therefore cannot reproduce.

To combat sedimentation we have the ErosionOperator, which works as you might expect, decreasing the depths of all cells and smoothing them as well. There are also a number of "randomization" operators; the CosmicRayOperator randomly flips bits in cell code every once in a while, and the RandomizeOperator more aggressively randomizes entire genomes. There are operators for decay, for seasons, and other fun things.

So, that's all well and good, but what do we get? Well, one fun thing we get is abiogenesis: starting with an empty environment and a few operators (sunshine and randomization are all that you really need in PondLife) after only a little while "viable replictors", cells which can copy themselves well enough that the copy can copy itself again, appear in the environment. And PondLife doesn't seem to "get stuck" too quickly, where only one life form exists in the environment; this is especially true if you include the sedimentation and erosion operators, which force cells to compete not only for energy but also for "depth".

"Pics or it didn't happen." I'll do you one better. I ran a simulation in a 128 by 128 world for 8 or so hours and have 2 videos. In the first video, different colors are different lineages; two cells have the same lineage if one was produced by the other, or if their parents have the same lineage. In the second video, depth is indicated in grayscale, with black being deeper (where more code can fit) and white being shallower (where less code can fit). In this simulation I also used an operator that caused less energy to be added to cells in "deeper water" for fun.

That simulation only ran for 2 billion cycles. That's not many, considering it took 8 hours (probably would have been the most intense computation this poor laptop has ever seen, except I did a 17 hour run right after). I need to optimize.

EDIT: Here are the videos:

Time Dilation

I haven't had much to say recently. I rather doubt anyone has noticed, and yet nevertheless I feel a bit guilty... Perhaps this indicates some underlying psychological problem? Anyway, I have an excuse: I was working on two different papers with various colleagues. If things work out I may infinitely increase my publication list!

The first, entitled Focused Inductive Theorem Proving describes the theory behind our interactive and automatic theorem prover for an intuitionist logic with support for generic quantification (using nabla, which is nice for reasoning about systems with names and binding) and definitions (via fixed points, which are useful for encoding inductive and coinductive data structures, like lists and streams, respectively). The system is called Tac, and is released under the GPL version 3. One fun note: we have (kind of, call it mostly) solved the POPLMark challenge parts 1A and 2A with Tac.

The second is A Meta-Programming Approach to Realizing Dependently Typed Logic Programming, and describes a technique that we developed to implement logic programming in LF via translation to λProlog, a higher order logic programming with an efficient bytecode based implementation. The tool, named Parinati, is also available under the GPL version 3.

Other than that I've been snowboarding and working on a fun little side project, which will be to topic of my next update, which I am sure you eagerly await.

System Eff

So, last time I mentioned that the first example was one "that cannot be handled under Hindley-Milner style inference". So the question is, "Ummm... what?" Let's look at the same code, but in an ML-like syntax:

let twice f x = f (f x)
let pair x = (x, x)

The types inferred for these lovely functions are:

val twice : ('a -> 'a) -> 'a -> 'a
val pair : 'a -> ('a * 'a)

So, what does the type of twice mean? Well, each 'a stands for a universally quantified variable, and in particular one that is quantified at the top level. So it means that, "for all types x, twice takes a function from x to x, and an item of type x, and returns something of type x". But is this really what we "meant" when we wrote out the definition of twice?

Maybe not. When we try to use it with pair we are treating it as though it really had the following type: "for all types x, twice takes a function from any type to the same type, and an item of type x, and returns an x". That is, we want twice to take, as its first argument, a universally quantified type. So, if we throw in some new syntax, we want this type:

val twice : (forall 'y. 'y -> 'y) -> 'x -> 'x.

We want to be able to introduce a universal quantification within the type of twice, and not just at the top level. And this is the problem: in our system of choice, this is not possible.

Now, there are of course systems in which this sort of quantification is perfectly legal; System F, for example, allows all this and more, for just 27 payments of $34.95! But, then again, type inference in System F is undecidable, which might burst your balloon.

This post is brought to you by the Greek letter...

So, a long time ago I said that a Mix alpha release is coming, and it really is, I swear. Here are some examples of Mix code that the implementation can currently compile correctly.

1: This is an example of some code that cannot be handled under Hindley-Milner style inference. Specifically, notice that in the body of twice we apply f to the type of its own result. This requires that f have type 'a -> 'a, and therefore that twice have type ('a -> 'a) -> a'. Clearly in our application of twice the argument pair doesn't have such a restricted type.

twice(f)
{
    return function(x){ return f(f(x)); };
}

pair(x)
{
  return new Pair(x, x);
}

Int main(String args)
{
  var p = twice(pair)(1);
  return p.First.First;
}

2: This example shows how cool container classes are in Mix, at least to me. I love homogenous containers because they (well, the type system) take care of ensuring I don't do anything too stupid with its elements. However, in a language like C# or Java you must introduce an (often artificial) interface in order to group objects of different type but related functionality in such a container -- otherwise you just have to relegate yourself to containers of object, and live with the lack of type safety. Here Mix infers what operations are possible on all elements of the array. The error arrises because Mix infers that the array possibly contains both integers and strings, the latter of which do not implement the negation operator -operator.

Another note: arrays are enumerable (which just means that they implement GetEnumerator correctly), and enumerables implement ToString by simply concatenating the string representations of all of their elements. So as long as all of the elements of an enumerable implement ToString, the enumerable itself does as well, which is how we can call IO.print on the array.

Int main(String args)
{
  var a = new Array(10);
  for(var i = 0; i < a.Length(); i++)
  {
    a[i] = i;
  }
  a[random(10)] = "Hello!";

  IO.print(a);  //Enumerable.

  a[4] = -a[4]; //Error, strings cannot be negated.
  return 0;
}

3: Here's a funny example in which iterating to a fixed point proves critical. Essentially f gets a type that should be interpreted as "either a pointer to an integer, or a pointer to a pointer to a string, or a pointer to a pointer to a pointer to an integer, or..." Which essentially means that the only operations you can really perform on f are ToString and Get (which gets the value of a pointer).

Int main(String s)
{
  var f = new Ptr(0);
  var g = new Ptr("Foo!");
  
  for(var i = 0; i < 10; i += 1)
  {
    var temp = f;
    f = new Ptr(g);
    g = new Ptr(temp);
  };
  
  IO.print("f: " + f);
  IO.print("g: " + g);
  return 0;
}

I wanted to put a few more up, but it is time to get back to work.