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.
Interesting… I did it that way because I wanted to make the simple examples work quickly without having to write code for generating gadgets! In the end (that is, when I get around to it) I’d prefer to be able to generate my own gadgets, treating data types that we know how to eliminate fast (eg Nat, Fin, possibly List, Vect, and anything of similar shape) specially. But there’s no reason why there can’t be some kind of syntax for doing that too.
Yes, I want to be able to play around with hand-cooked examples sooner rather than later. Also, I want to have the option to do an entirely dumb and trusting reload.