Comments on: Moderate Badness http://www.e-pig.org/epilogue/?p=130 for Epigram Sun, 6 Nov 2011 09:25:45 +0000 http://wordpress.org/?v=2.8.4 hourly 1 By: Conor http://www.e-pig.org/epilogue/?p=130&cpage=1#comment-6281 Conor Thu, 05 Oct 2006 07:24:19 +0000 http://www.e-pig.org/epilogue/?p=130#comment-6281 I should add that there is a tutorial for Epigram 1, available from our parent site 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. 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.

]]> By: Conor http://www.e-pig.org/epilogue/?p=130&cpage=1#comment-6280 Conor Thu, 05 Oct 2006 07:02:52 +0000 http://www.e-pig.org/epilogue/?p=130#comment-6280 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 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.

]]> By: Tristan http://www.e-pig.org/epilogue/?p=130&cpage=1#comment-6276 Tristan Wed, 04 Oct 2006 23:39:47 +0000 http://www.e-pig.org/epilogue/?p=130#comment-6276 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. 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.

]]> By: pwm http://www.e-pig.org/epilogue/?p=130&cpage=1#comment-6197 pwm Tue, 26 Sep 2006 16:04:22 +0000 http://www.e-pig.org/epilogue/?p=130#comment-6197 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 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

]]> By: Conor http://www.e-pig.org/epilogue/?p=130&cpage=1#comment-6129 Conor Thu, 21 Sep 2006 09:30:47 +0000 http://www.e-pig.org/epilogue/?p=130#comment-6129 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. 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.

]]>