I’m not very well at the moment, but I do get bored very easily. So I’ve made a thing. It’s an OTT piglet for us all to play with. It isn’t terribly exciting yet: I only have Pi and enumerations. I’m hoping to add more, real soon.
What you get is syntax, semantics, evaluation, equality testing, quotation and typechecking. In that order. There’s a rather crude test rig which lets you type definitions as could-be-worse Haskell expressions. I can’t even be bothered to write a parser or a printer.
The nice thing is that you can kind of see the connection between Wouter’s Agda development and this lump of Haskell. It’s chopped up the same way.
I’m plotting my next move. Something involving containers, perhaps…