I’ve just committed the blasphemy against the gods of version control that is sticking a generated binary in the repo. But we could use an up-to-date binary of the design doc on line, so I think it’s a justified and equitable squalid little hack. Please feel free to suggest a better way of doing this. (This is one respect in which our old makey-makey cvs regime was slightly better, I’m afraid.)
I’ve added the beginnings of a story about equality, but we haven’t got to the good bit yet.
*UPDATED: link to Epigram2.pdf above changed (see comment below) – pwm
The story about equality is now matched by the corresponding functionality, giving us an equality which is intensional but proof-irrelevant. Ecce can now check the implementation of JMelim which is given in the doc, which exploits proof-irrelevance to simplify my earlier construction using K. Next, we need to reimplement the machinery for shunting coercions through canonical terms, so we can add extensionality without losing canonicity.
I’ve deleted the document from the repository and implemented a cheap hack to get a (possibly broken) copy of the dvi and a (always consistent but possibly out of date) copy of the pdf in a public place with out having obscene binary patches. To make the obscene patches we already have go away I think the best option is to optimize the sneezy repo, which means tagging it… I’ll look into this anon
Something I think that document could do with is an explanation of the notation and jargon for the programmer new to epigram. To me it looks like somebody’s 1 year-old started bashing on a greek-layout keyboard.
I quite agree that some document should do that, just not this document.
This document is primarily intended as a space for developers to express their ideas coherently in a mathematical notation on paper, before hacking them into the system. Believe it or not, this actually happens. We kick ideas around on the whiteboard, then we try to note them down on paper to see if all the details work out. And then we actually code. This discipline has already prevented several wrong turnings.
The document is on the web for ease of access within the team, and in case anybody happens to be interested, and because it’s not a secret. Much of its content is quite volatile, and it’s certainly very patchy. So I’m sorry that it’s not so forgiving to non-insiders: much here is new and strange, so the time will come soon enough, fear not, when it will be necessary to give a proper and accessible account of what is going on.
By the way, if you know the parents of this 1 year-old, I may have a proposition for them.
I should add that there is a tutorial for Epigram 1, available from our parent site http://www.e-pig.org, full of examples and exercises for use with the existing system. Epigram 2 will certainly be accompanied by similar materials when it eventually emerges from this development process.