search

mwleeds / epigram

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

Eta-expansion during pattern matching #50

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 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