Appling a function to itself

Stream: new members

[Fejfo]

I noticed functions like def doTwice {α : Type} (f : α → α) (x: α) := f (f x) can be applied to themselves #check doTwice doTwice
Is there any way to type def doSelf (f : ?) := f f ?
def doSelf (f : ({α : Type u} → (α → α) → α)) := f f doesn't work. Why? (I've noticed {α : Type u} → (α → α) → α) : Type (u+1))

[Kyle Miller]

The type of doTwice seems to be {α : Type} → (α → α) → α → α, not {α : Type} → (α → α) → α

[Kyle Miller]

If you fix the type of f in doSelf, then it almost works (you just need to tell it what to use for the implicit argument)

[Yongyi Chen]

This worked:

def doSelf (f : {α : Type*} → (α → α) → (α → α)) : (α → α) → (α → α) := f f
def doTwice (f : α → α) := f ∘ f

#eval doSelf doTwice (.^2 : ℕ → ℕ) 2

[Yongyi Chen]

Fun fact:

#eval doTwice doTwice doTwice doTwice Nat.succ 1

works and outputs 65537 while

#eval doTwice doTwice doTwice doTwice doTwice Nat.succ 1

causes Lean to crash!

[Yongyi Chen]

Another fun fact, this is a valid definition too:

def doSelf2 (f : {α : Type*} → α → α) : α → α := f f

but one can't apply it to doTwice because doSelf2 expects a family of functions α -> α for every type α, and doTwice is not such a family -- it's only a family of functions (α -> α) -> (α -> α), in other words, a family of functions α -> α only for those α which happen to be of type β -> β for some type β.

In fact I wonder if anyone can think of a family {α : Type*} → α → α besides id.

[Kevin Buzzard]

In Wadler's "theorems for free" paper he shows that in a certain kind of type theory, id is the only inhabitant of that type. However in Lean you can just make things like "if alpha = Nat then fun n \mapsto 37 else id"

[Yongyi Chen]

I did manage to do something like that!

import Mathlib.Tactic

def doSelf2 (f : {α : Type*} → α → α) : α → α := f f

noncomputable def g : {α : Type} → α → α := by
  intro α
  if h : α = ℕ then
    subst h
    exact fun _ : ℕ => 37
  else
    exact id

example : g 4 = 37 := by
  simp only [g, dite_eq_ite, ite_true]

example : doSelf2 g 4 = 37 := by
  have : (ℕ → ℕ) ≠ ℕ := sorry
  simp [g, doSelf2, this]

I just have an issue with how to prove that (ℕ → ℕ) ≠ ℕ. Is that even provable in Lean?

[Kevin Buzzard]

If two types have different cardinalities then you can prove they're unequal in Lean (and if they don't then you can't). So here you're OK here because Nat -> Nat is uncountable and Nat is countable.

[Joachim Breitner]

(deleted)

[Kyle Miller]

@Joachim Breitner Type doesn't have decidable equality, so at least you can't write that if statement without the definition being noncomputable. (At least, I don't think you can.)

[Yongyi Chen]

Interesting!

example : doSelf2 g 4 = 37 := by
  have : (ℕ → ℕ) ≠ ℕ := by
    apply_fun Cardinal.mk
    simp
    exact ne_of_gt Cardinal.aleph0_lt_continuum
  simp [g, doSelf2, this]

[Joachim Breitner]

That makes sense. I was expecting that eliminating into Type from something that feels Prop-y (Types themselves) would not work, but this is ”just” using classical logic to decide, so that's why it works?

[Shreyas Srinivas]

Kevin Buzzard said:

In Wadler's "theorems for free" paper he shows that in a certain kind of type theory, id is the only inhabitant of that type. However in Lean you can just make things like "if alpha = Nat then fun n \mapsto 37 else id"

The proof I have seen of this property relied on a very strong semantic model of system F types.

[Shreyas Srinivas]

I just checked the paper and it doesn't say anything about dependent types at all