I think I'm warming up to the idea of having a personal blog. Of course, being myself, I re-wrote my static site generator in OCaml, and then re-wrote it again just to add support for blogging.

How does it feel? Good, I think. Many times ago I tried this I didn't consider the end result worth the effort, so it makes me feel good that now I have a plan for this.

What goes in a first post? Maybe a recap of what I've been doing lately:

Growl, my programming language, was re-written from C to OCaml this month, and gained a static type system based on subtyping along with a type inference algorithm inspired by SimpleSub.

Currently I'm weighing the benefits of principal type inference in a concatenative language. Types in applicative languages, like OCaml, are more well-behaved, and give you better errors when something goes wrong.

In concatenative languages, this is not the case. I've had to add more and more heuristics to the type inference algorithm to discern from a "good type" and a "bad type that still looks good", and the existence of type annotations was bolted in after I noticed that some programs give types that are too general.

An example of the latter point is the definition for list/each in the current (unpublished) branch with support for ADTs:

type a list 
  { nil
  | cons : a, a list
  }

def list/each
  [..r, a list, [..r, a -> ..r] -> ..r]
  { list/case: swap
      [drop]
      [swap unbury [unbury drop call] 3keep
       swap drop list/each];
  }

That annotation is required, or else the type inference algorithm gives list/each a type of [..r, a list, [..r, a -> ⊤] -> ..r] (where ⊤ is the "top" stack). Since we lose track of the stack returned by the quotation given to list/each, it can, for example, push values to the stack indiscriminately, and the type inference will have de-synced from the actual result of the program, and that's no good.

Of course, the language doesn't really stop us from doing that with the correct annotation, it just returns a weird recursive type of [(..r & μr. (..r, nat & ..r)) -> (..r | μr. (..r, nat | ..r))]:

def main 
  { list/each: {1 2 3 4}
      [];
  }

Whether we should reject words with recursive types or not is a heuristic I haven't touched on yet. There's also the problem in that the type inference can't infer the types of useful combinators, like bi@, but I've decided to just ignore them for the meantime.

So for Growl, the updates are a resounding "meh", but that's okay. I'm not like a type theorist, I'm just a guy playing around with their computer.

I've also been working on an album, titled Dogyears, but you'll be hearing more about it during the year as I get it done.