Since I worked out the proper monad implementation strategy and added the monadic syntactic sugar to SML/NJ, work has been moving along quite well.

I did extend the monad so that it has an additional »zero« element that allows for non-backtracking failure. That way a fatal error does not get masked by a non-deterministic choice. A good example of this is if some disjunct in performing a label subsumption check fails because it encounters an unknown variable, it shouldn't just try the other disjunction and ignore the fact that somehow an unknown variable wandered into the program.

Having things written in a monadic style is making the implementation way more pleasant than it would otherwise. While I could have in AspectML used global reference cells to avoid having to pass bits around, that would have required some annoying management with the backtracking that occurs in InforML.

Anyway, my hope is to have the rest of type inference mostly working in time for a video-conference with Stephanie later this coming week. At this rate, submitting to ICFP and defending in August looks pretty realistic.

So after some more work today I concluded that the code for a backtracking state monad yesterday does not work as hoped. Mostly because the exception handling scopes don't work they way I thought when I was squinting at them yesterday.

Fortunately, I was able to save the day with callcc. However, locally defined exceptions were still necessary to hide the return type when actually running the monad. I want to clean parts of it up a little more before I post the new and improved and hopefully bug free version.

Of course, I could ask why all of you out there didn't run off and try my code and tell me how wrong I was

I was trying to implement Ken Shan, et al's fair backtracking monad (ICFP 2005) yesterday for the InforML typechecker. However, no matter how I tried implementing it, I would become stuck trying to give them a type because SML doesn't have existential data types. It kept gnawing at me and this morning it came to me that by abusing local exception definitions I could work around this. It wouldn't work if, like OCaml, SML only allowed top level exception definitions. It might also be possible to use SML/NJ's callcc, but I had an easier time wrapping my head around this.

 
type env
 
(* Takes an environment, a success "continuation",
and a failure "continuation", and pretends that it
will give you an exception back *)
 
type 'a monad = env -> (env * 'a -> exn) -> exn -> exn
 
infix 5 >>=
infix 5 >>
infix 5 ||
 
(* Unit *)
fun return x =
    (fn s => fn sk => fn fk => raise (sk (s, x)))
 
(* Bind *)
fun (m : 'a monad) >>= (f : 'a -> 'b monad) =
    let
      exception SuccCont of env * 'a
    in
      (fn s => fn sk => fn fk =>
         (m s SuccCont fk)
         handle SuccCont (s', x) => ((f x) s sk fk))
    end
 
(* Sequence *)
fun (m1 : 'a monad) >> (m2 : 'b monad) =
  [| x | _ <~ m1, x <~ m2 |]
 
(* Choice *)
fun (m1 : 'a monad) || (m2 : 'a monad) =
    let
      exception FailCont
    in
      (fn s => fn sk => fn fk =>
         (m1 s sk FailCont)
         handle FailCont => (m2 s sk fk))
    end
 
(* Zero, disjunctive unit *)
val zero = (fn s => fn sk => fn fk => raise fk)
 

I just finished hacking the SML/NJ parser to allow monad comprehension sugar. Here is an example of using it when using the list monad.

- infix 5 >>=;
infix 5 >>=
- [| x | x <~ [1,2,3] |];
val it = [1,2,3] : int list
- [| (x, y) | x <~ [1,2], y <~ ["a", "b"] |];
val it = [(1,"a"),(1,"b"),(2,"a"),(2,"b")] : (int * string) list
-

I first looked at adding »do« notation, but that would have been kind of ugly without the offside rule. The only disadvantage to using comprehension syntax is that you must always »return« something. However, I expect that will be reasonable enough for my work on InforML. Additionally I had original chosen to use <- instead of <~, but it was already taken in some user defined code somewhere in the SML basis.

I also determined that the source of my mysterious parsing behavior in InforML was being caused by a few small instances of backtracking in my grammar. However, I still can't see how backtracking was causing the problem. In any event, I was lucky and discovered that the backtracking was no longer necessary in the grammar and all is well.

Generated using »dot« from the dump produced by »ml-antlr«.

I'm encountering odd behavior with some examples that should not parse. For example, it believes the input

val 1 : Int

corresponds to the AST

val it = (1 Int)

Which seems to indicate that it thinks the input is an expression because it is creating a dummy value declaration for »it«. I'm still uncertain as to whether this is a bug in my code or »ml-antlr«. At least staring at the automaton and my EBNF I can't see how it could possibly not report a parse error on my example.

In any event, modulo bug squashing I've finally finished parsing and pretty-printing for InforML. Tomorrow I'll start on implementing the truly interesting stuff: type-inference.

You know you're doing research when you spend today undoing nearly everything you did yesterday.

So I'm still working on away on typesetting the inference algorithm for InforML. Partly it is because I've decided to just go ahead and do all of it. It has already paid off on illuminating some tricky bits. Additionally, at some stage in my revision I concluded that not only would it be very useful to have higher-rank universal quantification, but that »first-class« existential types would be really handy too.

My initial attempts at this weren't entirely satisfactory, but Stephanie became quite interested in the problem again and worked out her own take on existential inference (kind of a dual to Damas-Milner). So I'm massaging the latest draft of that system in during my current revision cycle.

I expect however I am on my last major pass of revisions before I go back to coding.  If nothing else I'll code up the parts that have become pretty stable to make testing examples stressing the more tenuous bits easier.

Of course, the language has also changed in all sorts of random ways since I last touched the parser, so I may have to spend a bit of time wrestling making the grammar LL(k) approved.  I also have to implement all sorts of operations on graphs, as I'm modeling most of the queries on constraint sets using DAGs.

Anyway, I expect there will be more exciting news to come on the implementation front.

I've been meaning to put up this sort of comparison for a quite some time, so that it is perhaps clearer why I have been thinking about designing a symbol font to serve as a better companion to AMS Euler.

Above is an excerpt of a side by side comparison of AMS Euler and Computer Modern Italic (which is the Computer Modern math font) that I just prepared. For the most part it is hopefully clear that AMS Euler has a generally darker »color« and more »robust« stems. Now consider a comparison of an inference rule not unlike would be seen in many papers I read or write.

The important points to note here are that currently, many important symbols are used identically regardless of which typeface has been chosen. Therefore, despite AMS Euler's darker color the turnstile, equivalence symbol, up-arrow, and »forall« quantifier remain the same »weight«. It is interesting to note that the up-arrow is ever-so-slightly wider for AMS Euler though. Additionally, in this context it feels like the universal quantifier should have a wider spread when used with AMS Euler. The star probably is fine as is, but it might even be worth providing a heavier version.

Anyway, I hope this makes things clearer. However, if you disagree with my assessment, and feel that the differences are insignificant, let me know that too.

I haven't really been saying nearly enough about my research lately. However, for the most part it has involved hacking away on AspectML to slowly remake it as InforML. The new frontend is kind of finished. I still need to fix the parser so it generates output that satisfies the Barendregt convention. Aaron Turon deserves considerable credit for all the help and hacking he's been doing to get ml-antlr (an LL(k) parser generator for SML) and ml-ulex working for me and the peculiarities of my implementation style.

The past week or so I've been focusing on extending my current »specification« with descriptions of the algorithms for solving label constraints, kind and type subsumption, and type joins and meets. This has been particularly hard on my brain. But I think I'm closing into something that should be sound and close to complete, at least without having explicitly done the proofs. But my committee decreed that I should not prove anything from my proposal on out, so it will have to do. I'm hoping maybe that tomorrow I'll have settled on a essentially final design and will be able to get back to implementation.

The sort of vague plan is to aim for an ICFP submission (which I just learned today will be doing double-blind reviewing this year) with the plan to defend in time for an August graduation date. It could happen.

I spent some time of Friday putting my current dissertation draft into the correct format for the Ruler Lady. I am hoping to provide an alternate format for pleasant reading; I did some pricing on Lulu and definitely think I'll print some nice copies for a few people when I'm done.