Comments on: 2+2=4 http://www.e-pig.org/epilogue/?p=266 for Epigram Sun, 6 Nov 2011 09:25:45 +0000 http://wordpress.org/?v=2.8.4 hourly 1 By: Adam http://www.e-pig.org/epilogue/?p=266&cpage=1#comment-70851 Adam Mon, 21 Dec 2009 15:31:25 +0000 http://www.e-pig.org/epilogue/?p=266#comment-70851 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: <code>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</code> As Conor said, we're a little way from high-level code at the moment... Adam 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

]]> By: Conor http://www.e-pig.org/epilogue/?p=266&cpage=1#comment-70845 Conor Fri, 18 Dec 2009 22:02:58 +0000 http://www.e-pig.org/epilogue/?p=266#comment-70845 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.) 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.)

]]> By: Sjoerd Visscher http://www.e-pig.org/epilogue/?p=266&cpage=1#comment-70841 Sjoerd Visscher Thu, 17 Dec 2009 12:32:19 +0000 http://www.e-pig.org/epilogue/?p=266#comment-70841 Can you show some code? I'm really curious now. Can you show some code? I’m really curious now.

]]>