search

mietek / epigram2

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

Eta-expansion during pattern matching #50

Open GoogleCodeExporter opened 8 years ago

GoogleCodeExporter commented 8 years ago 
1/ Imagine we work to solve this programming problem: < f z : T > where z : 
Sigma X Y.

We would like to have "eta-rules" while pattern-matching, that is the ability 
to write:
f (x , y) instead of invoking the split eliminator.

2/ Further, when working on <flip g : B -> A -> C> with g : A -> B -> C, it 
would be exciting to be able to write:
flip (\ x y -> f y x) = f

(1) seems a reasonable target, (2) is more extravagant.

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