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!
Can you show some code? I’m really curious now.
Hi Sjoerd! We’re just tweaking things a bit. Today, we dumped our hardwired type of datatype descriptions: it has a description itself, so we can use quite a lot (not all — bootstrapping issues) of the generic machinery even for the machinery of generics. Once we’ve completed this levitation trick (if you really stare, you can see the wires), we’ll blog in more detail. Note that we’re nowhere near any kind of tasteful high-level code yet: just now, we have only core gore, where more is more!
Meanwhile, for code of another kind, the literate implementation can always be found in the Epitome (in the sidebar of the front page).
(Peter, is the repo available over http? You never know, intrepid people might like to poke about with it.)
Thanks to some minor fixes and additions today, it is now possible to define the natural numbers from scratch in the Cochon interactive environment, thus:
make nat := (Mu @ [`arg { zero, suc } [ (@ [`done]) (@ [`ind1 @ [`done]]) ] ] ) : * ;make zero := @ [`zero] : nat ;
make suc := (\ x -> @ [`suc x]) : nat -> nat ;
make one := (suc zero) : nat ;
make two := (suc one) : nat ;
make plus := @ @ [(\ r r y -> y) (\ r -> @ \ h r y -> suc (h y))] : nat -> nat -> nat ;
make x := (plus two two) : nat
As Conor said, we’re a little way from high-level code at the moment…
Adam