Archive for February, 2005


Thursday, February 24th, 2005

Hugs and GHC seem to disagree on this one:

ERROR “./DeBruijn.lhs”:111 - Cannot justify constraints in explicitly typed binding
*** Expression : (\)
*** Type : (Named a, Bind b) => Bwd a -> b -> b
*** Given context : (Named a, Bind b)
*** Constraints : Named a

Peter directed me towards:

So presumably some more type annotations are required. Can’t work out what though…

Fear and Parsing in 2D Syntax

Thursday, February 24th, 2005

Over the past couple of weeks I’ve been working on improving the error messages you get from the Parser, they will now give you some idea of what was being tried when the error occurred and where you might find the error in your code.

This is not the finished article, but I thought it was best that it got commited as soon as it compiled and ran. For instance I haven’t used the new parser combinators anywhere in the parser for frames so, for the moment, it’s error messages may be a little misleading.

Please feel free to try out testConcrete!


Thursday, February 17th, 2005

After a lovely time with mfix making cyclic data structures, so that Nat knows about its bits which are typed in terms of Nat, I then had a horrid time chasing down a peculiar bug. It turns out that

(t :->> w) @@ e = t @@ e :->> w @@ e

ain’t the same as

(t :->> w) @@ e = (t @@ e) :->> (w @@ e)

which is what I meant. Differently grouped, it loops rather tightly. Took me ages to find it. Now that I’ve nailed that little sod, I can confirm that 2+2 is indeed 4.

I’ll commit the changes tomorrow, when I’ve yanked out all the tracing.

This Code Malarkey

Thursday, February 17th, 2005

The Compressor type is a reasonable first approximation to the datatype squishing technology we might want, but it wasn’t quite satisfying. For one thing, it was ‘backwards’, reflecting the order in which we unstack arguments, rather than the order in which the arguments arrive—I was always checking the length of the spine against the length of the compressor, which is clearly dumb.

Also, the compressor made it tricky to get at the types of compressed data without just expanding to a spine and forgetting which data was really needed. The new format enables us to get a vector of types for the vector of compressed arguments—we can use this to push types into the equality check for compressed data, so we don’t check whether arguments are equal to each other when we already know what they’re equal to.

Moreover, I thought it would be handy to have a uniform language for implementing constructors, elim gadgets, combinators etc, which allows you to say ‘keep this, sling that, jump when you’re ready’. I’m planning to put this code into object files, so that objects we trust are fully realoadable. If we’re checking object files, we should regenerate the code instead. Credit to Edwin: I looked at his .tt file and thought ‘I’ll have a bit of that!’.

This involves quite a bit of tweaking, with stuff broken in the meantime, so I won’t commit until it’s done.

Yesterday’s stuff

Thursday, February 17th, 2005

You may have noticed that Term.lhs is a little shorter. I just shifted everything not strictly necessary for the syntax and operational semantics into other files, viz.

  • TermTools.lhs
    with yer abstractor and yer instantiator // and yer discharger |- and yer quantifier-stripper -| and a’that. Most especially, the β-behaviour of typed terms (which must only be used in a type-correct way). See here. This is what the typechecker will call to assemble values with which it’s happy. See here.
  • Normal.lhs now has the weak-head and full normalization algs. The latter will be tweaked to use typed β next time I commit.

You’ll also have noticed that I’m up to something, down the bottom of the file, with some form of Code. More on that in a bit.

Some loud pictures from today’s meeting

Tuesday, February 15th, 2005
Conor's whiteboard 0 Matters arising
Conor's whiteboard 1 Conor's whiteboard 2 Infer strike one
Conor's whiteboard 3 Conor's whiteboard 4 Infer strike two
Conor's whiteboard 5 Conor's whiteboard 6 Conor's whiteboard 7 Equality

Toy compiler

Thursday, February 3rd, 2005

I’ve been writing a toy compiler, which sort of half works now, except that there’s no optimisations, the generated code is quite bad and the virtual machine is too slow - you can get it from It spits out C, and you have to do a bit of work to get your program to do anything, but it’s a start (and at least there’s an example). I was going to spit out GHC core, but then I realised that writing abstract machines was too much fun.

Anyway, I thought I’d let you know just to show that I was actively doing something ;) .

It’s probably still worth having a GHC core back end, and certainly generating .hs/.hi files. But I think this way is going to work better for compile-time evaluation.

Today’s mission…

Wednesday, February 2nd, 2005

I’m stuck at home with a rotten cold, so I think I’ll try to do something useful. Specifically, how about turning the current bunch of stuff into a main program which takes an object file name as a command line parameter and loads it (in a suitably verbose style, for the now)? Apart from anything else, that would give us a more sensible basis for testing stuff. All I have to do is learn to make Haskell programs read command-line arguments, open files etc. I’ll be poking about in webland to see how do to my Haskell homework, but I’d be delighted to have someone elses’s to plagiarize…