This may not seem startling, and it isn’t. It’s the first thing we check when we have a system that’s beginning to work. Today, we constructed + for the natural numbers by appeal to the generic elimination operator. Then we applied this + to two and two. Then we compiled the resulting definition to a standalone executable. Then we ran that executable. It printed four (in a suitable encoding). Dr Brady has been visiting, which helps with this sort of shenanigans.
When I say “the generic elimination operator”, I don’t mean the elimination operator for the natural numbers. I mean the generic elimination operator for all inductive datatypes, applied to the piece of data which describes the natural numbers. This version of Epigram has datatype-generic programming built in. So what we’ve really been doing is thrashing that datatype encoding mechanism. It seems to be working, so I’d better change it.
The long dark is ending. We’ve been hacking up bits of kit for ages, but we now have an end-to-end system: construction commands go in; compiled code comes out. Time to chuck in functionality and get playing!