Archive for December, 2006

Always, always test

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 🙂


Abusing exceptions

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.

  2. type env
  4. (* Takes an environment, a success "continuation",
  5. and a failure "continuation", and pretends that it
  6. will give you an exception back *)
  8. type 'a monad = env -> (env * 'a -> exn) -> exn -> exn
  10. infix 5 >>=
  11. infix 5 >>
  12. infix 5 ||
  14. (* Unit *)
  15. fun return x =
  16. (fn s => fn sk => fn fk => raise (sk (s, x)))
  18. (* Bind *)
  19. fun (m : 'a monad) >>= (f : 'a -> 'b monad) =
  20. let
  21. exception SuccCont of env * 'a
  22. in
  23. (fn s => fn sk => fn fk =>
  24. (m s SuccCont fk)
  25. handle SuccCont (s', x) => ((f x) s sk fk))
  26. end
  28. (* Sequence *)
  29. fun (m1 : 'a monad) >> (m2 : 'b monad) =
  30. [| x | _ <~ m1, x <~ m2 |]
  32. (* Choice *)
  33. fun (m1 : 'a monad) || (m2 : 'a monad) =
  34. let
  35. exception FailCont
  36. in
  37. (fn s => fn sk => fn fk =>
  38. (m1 s sk FailCont)
  39. handle FailCont => (m2 s sk fk))
  40. end
  42. (* Zero, disjunctive unit *)
  43. val zero = (fn s => fn sk => fn fk => raise fk)


Hacking for great justice!

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.

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

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.

Comments (2)

Finite-state automaton for the InforML parser

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

The grammar of the InforML Language

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

  1. val 1 : Int

corresponds to the AST

  1. 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.


Research versus engineering

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

Comments (1)

AMS Euler compared with Computer Modern

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.

AMS Euler and Computer Modern Comparison

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.

Comparison of inference rules typeset with AMS Euler and Computer Modern

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.

Comments (4)

Caution: dissertating in progress

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.