mietek / epigram2

Mirror of Epigram 2, by Conor McBride, et al.
https://code.google.com/p/epigram
MIT License
48 stars 7 forks source link

Remove automatic Enum-splitting / generate proper induction principle #48

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago
Currently, on a goal of type "Enum E -> T", Epigram will automatically split 
the enumeration and ask you to build as many functions as there are cases in E.

This is a hack for the induction principle of (i)Desc to be in a nice form when 
using it: it automatically splits the function definition per-constructors 
(that are members of an enumeration).

Now, always doing that is incorrect. One could think of conditioning the 
simplification to the fact of working on a Description, not running it 
otherwise.

But better (and I wish we could that more often): we just remove this Haskell 
code and implement this in Epigram itself! That is, we define a generic 
function that takes a tagged description and hands out a properly expanded 
induction principle for the data-type.

Original issue reported on code.google.com by pedag...@gmail.com on 23 Aug 2010 at 1:28

GoogleCodeExporter commented 9 years ago
I've pushed a couple of patches that deal with this for IDesc but without 
switching off the offending problem simplification code (since a number of 
tests using Desc still rely on the old behaviour).

Currently the definitions of induction and case for tagged data types in 
test/TaggedInduction.pig are simply used to generate Haskell representations 
which are pasted directly into src/Features/IDesc.lhs. This ugly hack is in 
place of a more serious attempt at bootstrapping a prelude of some sort. (The 
in built versions are named differently to the file for stupid reasons, try 
idind and icase)

If you use the |idata Blah ...| tactic to build data types then these gadgets 
get specialised for you as Blah.Ind and Blah.Case.

http://www.e-pig.org/darcsweb?r=Pig09;a=commit;h=20100824120257-8a29d-793f843018
903b4c411f5d273e5b705f5956d2e1.gz
http://www.e-pig.org/darcsweb?r=Pig09;a=commit;h=20100824124512-8a29d-9c4c3c86f6
6cecc654365a6643f8175fa5d7565b.gz

Original comment by morris...@gmail.com on 24 Aug 2010 at 12:54

GoogleCodeExporter commented 9 years ago
I've restricted the automatic enum switching code to the case where the 
enumeration is completely canonical. This means the old test cases still work, 
but things do not go as badly wrong when you try generic programming. The 
sooner we can remove this simplification for good, the better.

http://www.e-pig.org/darcsweb/darcsweb?r=Pig09;a=commit;h=20100831141611-e29d1-e
93b3242501049f2499b68bbc8116b265a654e2d.gz

Original comment by adamgundry on 31 Aug 2010 at 2:25