search

mwleeds / epigram

Automatically exported from code.google.com/p/epigram
0 stars 0 forks source link

Can we program with IDesc itself? #106

Open GoogleCodeExporter opened 8 years ago

GoogleCodeExporter commented 8 years ago 
Peter's idata tactic allows us to define (Catholic) families and program nicely 
with them, but it's really tough programming with yer actual IDesc itself. 
Generic programming is not as easy as it should be? Can we at least identify 
the bottlenecks? Are there any small things we could do to get off the ground 
here?

Serious target here: the rec memoroid. Peter got close, but what killed it? 
Let's figure out how to get that done.

Original issue reported on code.google.com by co...@strictlypositive.org on 14 Sep 2010 at 12:56

GoogleCodeExporter commented 8 years ago 
I've had a stab at implementing the guarded fixpoint construction, and 
succeeded for Desc, but IDesc doesn't seem to want to cooperate. One of the 
eliminations fails but I have no idea why (printing the error message is too 
painful). The mutual recursion with helper functions is made more difficult 
because you cannot write labelled types (with fake out-of-scope references) in 
Cochon.

http://www.e-pig.org/darcsweb/darcsweb?r=Pig09;a=commit;h=20100916141532-e29d1-e
6d73133d07f6202c43ad1cee83cc267d3f53246.gz

Original comment by adamgundry on 16 Sep 2010 at 2:47