Idris should have judgemental eta for functions

[JasonGross]

I would like the following code to work:

eta : (f : a -> b) -> f = (\x => f x)
eta f = refl

[jonsterling]

I just ran into this as well; would be very useful. :)

[JanBessai]

eta : (f : a -> b) -> f = (\ x => f x)
eta f = believe_me (refl {f})

does the trick. But note that it does not create a universally type qualified proof, but really means

f {a} = \ (x : a) => f {a} x

for a fixed type "a". This can become quite confusing.

Edit: Typo.

[JasonGross]

What does eta f : (f : a -> b) ... mean? That eta takes two parameters named f? I strongly suspect your function is wrong.

Regardless, this is equivalent to adding an axiom to Idris, and is not what I meant when I requested (native) support for eta.

[JanBessai]

Typo, sry.

[JasonGross]

Where does the f taking a type parameter come from?

[JanBessai]

f : a -> b
f x = ?test

:p test
----------                 Goal:                  ----------
{ hole 0 }:
 (iType : Type) -> (a : Type) -> a -> iType

type variables become implicit parameters.

eta : (f: a -> b) -> (f = \x => f x)
eta f = ?test

:p test
----------                 Goal:                  ----------
{ hole 0 }:
 (a : Type) -> (b : Type) -> (f : a -> b) -> f = λx => f x

[JasonGross]

Yes, but that happens because you are defining f. I am not defining f, I am taking it as an argument, and so it has no type parameter.

[JanBessai]

True if you have f : Int -> Int it will be eta {a = Int} f. But if you have f : a -> Int it will be eta {a = k} (f {a = k}) for a fixed k creating the f {k} = \ (x : k) => f {k} x result from above. This is confusing because, what you see is (f = \ x => f x) which syntactically hides k. Lectures on the Curry-Howard Isomorphism, Exercise 7.7.6 is related and shows what happens for a system treating a as a variable.

[JasonGross]

eta {a = k} (f {a = k})

No, that's wrong. Not all functions in Idris are universally quantified. Only functions at top level are implicitly universally quantified. If what you're saying is true, then I could do something stupid like

bad : (f : a -> False) -> False
bad f = f {a = unit} tt

really_bad : False
really_bad = bad {a = False} (\ x => x)

[JanBessai]

I didn't say all of them are. My last example even includes one that clearly isn't: f: Int -> Int. Just some are and for those files even need them explicitly written down in top-level definitions

module Eta

f : a -> Int
f x = 3

eta : (g: a -> b) -> (g = \ x => g x)
eta g = believe_me (refl {g})

useEta : f {a = Int} = \ x => f {a = Int} x
useEta = eta (f {a = Int})

while the repl will show

>> :t useEta 
*Eta.useEta : f = \ x => f x

leading to situations where people try:

*Eta> let p : (useEta = eta {a = Float} f) = refl in p
Can't unify
    believe_me refl = believe_me refl
with
    useEta = eta (f)

Specifically:
    Can't unify
        believe_me refl
    with
        believe_me refl

and start to file bug reports ;)

[jonsterling]

Can we close this issue? Eta conversion seems to work fine on the latest version of Idris.

[JasonGross]

If the code I gave at the top typechecks in the latest version of Idris, feel free to close this issue (though possibly use the code to make a simple regression test?)

[jonsterling]

@JasonGross Good idea! If nobody gets around to it before I do, I'll put in a regression test.

[LeifW]

Doesn't seem to compile for me. Gives:

Can't unify
        f = \x => f x
with
        f = f

[LeifW]

Seems to work in non-pointfree (eta-expanded) form:

eta : (f : a → b) → (x : a) → f x = (λy ⇒ f y) x
eta f x = refl

[JasonGross]

@LeifW the point of this issue is that it should work in pointfree form; the law you gave is properly called beta reduction/expansion, not eta.

Use cases including proving that there is a category of sets.

[puffnfresh]

The original definition isn't working in master:

Can't unify
        f = \x => f x
with
        f = f

Specifically:
        Can't convert
                f = \x => f x
        with
                f = f