## Stream: new members

### Topic: applying a function to itself

#### Kenny Lau (Jun 03 2020 at 15:37):

meta def foo : Type :=
foo → foo

#check λ f g : foo, f g


#### Kenny Lau (Jun 03 2020 at 15:37):

type mismatch at application
f g
term
g
has type
foo
but is expected to have type
[foo._main]


#### Kenny Lau (Jun 03 2020 at 15:37):

how do I make it work?

#### Kenny Lau (Jun 03 2020 at 15:37):

I want to apply a function to itself

#### Kenny Lau (Jun 03 2020 at 15:37):

why does foo have no equational lemma?

#### Pedro Minicz (Jun 06 2020 at 04:52):

I am not familiar with meta definitions in Lean, but meta def foo : Type := foo → foo seems to be a hack-y attempt at an untyped identity function.

#### Pedro Minicz (Jun 06 2020 at 04:56):

You cannot apply a strictly one argument function to itself, because that necessarily would lead to a type mismatch. That is, you would have α → b and α = α → b, so α would have to be a fix-point ((... → b) → b) → b, which is not possible, because terms themselves can't be infinite.

#### Pedro Minicz (Jun 06 2020 at 05:02):

You can, however, (kind-of) apply an identify function to itself.

def id' {α : Type*} : α → α := λ x, x


id is a function of two arguments, the first of which is implicit, so Lean will try to figure it out for us if it can.

#check id' id'


Lean will figure out that the type α for the leftmost id' is Π {α : Type*}, α → α. You can make implicit arguments explicit using @:

#check @id' (Π {α : Type*}, α → α) @id'


#### Pedro Minicz (Jun 06 2020 at 05:03):

Another example of interest:

variable β : Type*

#check @id' (β → β) id'


@Mario Carneiro

hi

#### Mario Carneiro (Jun 10 2020 at 14:06):

it's not going to work

why not

#### Mario Carneiro (Jun 10 2020 at 14:06):

because this would make the typechecker diverge

#### Kenny Lau (Jun 10 2020 at 14:07):

what does diverge mean?

not stop

#### Mario Carneiro (Jun 10 2020 at 14:07):

recursive meta definitions use macros to indicate the recursion, they aren't defeq to their unfolding

#### Kenny Lau (Jun 10 2020 at 14:08):

but can we prove foo = [foo._main]?

#### Mario Carneiro (Jun 10 2020 at 14:08):

I'm not even sure the concept makes sense since the kernel never sees meta defs

#### Mario Carneiro (Jun 10 2020 at 14:09):

what does that even mean? In meta land everything is provable

#### Kenny Lau (Jun 10 2020 at 14:09):

meta def foo : Type :=
foo → foo

#print prefix foo
/-
foo : Type
foo._main : Type
-/

#print foo
/-
meta def foo : Type :=
foo._main
-/

#print foo._main
/-
meta def foo._main : Type :=
id_rhs Type ([foo._main] → [foo._main])
-/


#### Kenny Lau (Jun 10 2020 at 14:10):

what is the [] in [foo._main]?

a macro

#### Kevin Buzzard (Jun 10 2020 at 14:10):

I just thought it meant "you dunfolded too much"

#### Kenny Lau (Jun 10 2020 at 14:11):

how is [] defined?

#### Mario Carneiro (Jun 10 2020 at 14:11):

You are thinking of the projection macro

#### Mario Carneiro (Jun 10 2020 at 14:11):

It is expr.macro

#### Mario Carneiro (Jun 10 2020 at 14:11):

it is a separate constructor from pi, lam, var,mvar and everything else

#### Mario Carneiro (Jun 10 2020 at 14:12):

Here's a projection macro:

#print and.left
-- @[reducible]
-- def and.left : ∀ {a b : Prop}, a ∧ b → a :=
-- λ (a b : Prop) (c : a ∧ b), [and.left c]


#### Kenny Lau (Jun 10 2020 at 14:12):

how do I produce a term of type [\a]?

You can't

#### Mario Carneiro (Jun 10 2020 at 14:12):

seriously, this is super annoying

alright sorry

#### Mario Carneiro (Jun 10 2020 at 14:12):

but expr.macro uses an opaque type macro_def that lean code can't create

#### Mario Carneiro (Jun 10 2020 at 14:13):

no, not you, macros are annoying

#### Kenny Lau (Jun 10 2020 at 14:13):

can I use unchecked_cast?

#### Mario Carneiro (Jun 10 2020 at 14:13):

I think that will work

#### Kenny Lau (Jun 10 2020 at 14:13):

#check λ f : foo, f \$ unchecked_cast f


#### Kenny Lau (Jun 10 2020 at 14:13):

but would it "work" like I want it to?

#### Mario Carneiro (Jun 10 2020 at 14:14):

hm, best think of a better test

#### Mario Carneiro (Jun 10 2020 at 14:14):

maybe use the Y combinator so that it halts

#### Mario Carneiro (Jun 10 2020 at 14:15):

You can at least use expr.macro_def_name to see what kind of macro you are looking at

#### Kenny Lau (Jun 10 2020 at 14:17):

variable {α : Type*}

meta def Y : (α → α) → α | f := f (Y f)

#check λ f : α → α, (rfl : Y f = f (Y f))
/-
invalid type ascription, term has type
?m_2 = ?m_2
but is expected to have type
Y f = f (Y f)
-/


oh no

#### Kenny Lau (Jun 10 2020 at 14:21):

is it true that |A| = |A^A| iff |A| = 1?

#### Kevin Buzzard (Jun 10 2020 at 14:21):

#print has_add.add
/-
@[pattern, reducible]
def has_add.add : Π {α : Type u} [c : has_add α], α → α → α :=
-/


Is that also a macro?

#### Kevin Buzzard (Jun 10 2020 at 14:21):

If |A|>1 then |A^A|>=|2^A|>|A|

#### Kenny Lau (Jun 10 2020 at 14:22):

so we have proved that foo \equiv unit

#### Kenny Lau (Jun 10 2020 at 14:23):

meta def cantor := cantor → Prop


yay I broke Lean

#### Kevin Buzzard (Jun 10 2020 at 14:23):

You only meta-broke it -- that's allowed

#### Kevin Buzzard (Jun 10 2020 at 14:24):

Reid proved false the other day in meta land -- it wasn't hard

#### Kenny Lau (Jun 10 2020 at 14:26):

@Mario Carneiro how about this as a test: can you prove false using unchecked_cast and cantor?

#### Mario Carneiro (Jun 10 2020 at 14:26):

you can prove false using just unchecked_cast

#### Kenny Lau (Jun 10 2020 at 14:26):

meta def cantor := cantor → Prop

meta example : false :=
let R : cantor := λ A, ¬ (@unchecked_cast _ cantor A) A in
sorry


#### Kenny Lau (Jun 10 2020 at 14:26):

i.e. something like this

#### Mario Carneiro (Jun 10 2020 at 14:27):

meta example : false := unchecked_cast trivial


#### Kenny Lau (Jun 10 2020 at 14:27):

i.e. can you translate cantor's paradox

yes

#### Mario Carneiro (Jun 10 2020 at 14:28):

you need to use unchecked_cast to prove the side condition on cantor_injective though

#### Mario Carneiro (Jun 10 2020 at 14:28):

so it's not very impressive

#### Mario Carneiro (Jun 10 2020 at 14:30):

Without the theorem that says that cantor = (cantor → Prop), you won't get anywhere in the proof

#### Kenny Lau (Jun 10 2020 at 14:30):

A B : set cantor,
H : unchecked_cast A = unchecked_cast B
⊢ A = B


#### Kenny Lau (Jun 10 2020 at 14:30):

you mean this is unchecked_cast H?

#### Mario Carneiro (Jun 10 2020 at 14:31):

It's unchecked_cast of anything you want

#### Mario Carneiro (Jun 10 2020 at 14:31):

I think you are ascribing more meaning to this than is warranted

#### Kenny Lau (Jun 10 2020 at 14:31):

do we even "know" that cantor = (cantor \to Prop)?

#### Kenny Lau (Jun 10 2020 at 14:32):

oh right, in meta land everything is true

#### Mario Carneiro (Jun 10 2020 at 14:32):

In meta land, it's not a complete free for all, there is a semantics but it is more like the semantics of Haskell

#### Mario Carneiro (Jun 10 2020 at 14:32):

however unchecked_cast breaks even that

#### Kenny Lau (Jun 10 2020 at 14:32):

oh no this doesn't terminate:

#reduce @unchecked_cast true false trivial


#### Mario Carneiro (Jun 10 2020 at 14:33):

unchecked_cast is implemented as a loop IIRC

oh nvm

#### Kenny Lau (Jun 10 2020 at 14:33):

#eval @unchecked_cast ℕ ℤ 3 -- 3


#### Mario Carneiro (Jun 10 2020 at 14:33):

try it for larger numbers :)

#### Kenny Lau (Jun 10 2020 at 14:34):

guess the outputs:

#eval @unchecked_cast empty ℕ (unchecked_cast tt)
#eval @unchecked_cast empty ℕ (unchecked_cast ff)


#### Mario Carneiro (Jun 10 2020 at 14:36):

One of these is not like the others:

#eval (list.range 34).map (λ n, @unchecked_cast ℕ ℤ (2^n - 1))
-- [0, 1, 3, 7, 15, 31, 63, 127, 255, 511, 1023, 2047, 4095, 8191, 16383,
--  32767, 65535, 131071, 262143, 524287, 1048575, 2097151, 4194303, 8388607,
--  16777215, 33554431, 67108863, 134217727, 268435455, 536870911, 1073741823,
--  -1, 4294967295, 8589934591]


#### Mario Carneiro (Jun 10 2020 at 14:38):

Oh haha the reason #reduce @unchecked_cast true false trivial doesn't terminate is for the very silly reason that strings are involved

#### Mario Carneiro (Jun 10 2020 at 14:40):

this works fine

meta def {u} unchecked_cast' {α : Sort u} {β : Sort u} : α → β :=
cast (undefined_core "")

#reduce @unchecked_cast' true false trivial
-- eq.rec true.intro (undefined_core {data := list.nil char})


#### Kenny Lau (Jun 10 2020 at 14:40):

why does it being "undefined" make it not terminate?

#### Patrick Massot (Jun 10 2020 at 14:41):

It reminds me that we have something for @Gabriel Ebner who is already hunting down ideas for Lean 3.17.0: fix https://github.com/leanprover-community/doc-gen/blob/master/src/export_json.lean#L284-L287. I had to use the same itersplit trick in the sphere eversion infrastructure.

#### Mario Carneiro (Jun 10 2020 at 14:41):

it terminates but only after about O(size of unicode * length of string * very large #reduce constant) steps

#### Gabriel Ebner (Jun 10 2020 at 14:42):

I'm not sure if these two are related, but this applies for both of them: please file a #mwe at the lean bug tracker!

#### Mario Carneiro (Jun 10 2020 at 14:42):

wait, is there a lean feature suggestion in this thread?

#### Rob Lewis (Jun 10 2020 at 14:42):

Mario Carneiro said:

One of these is not like the others:

#eval (list.range 34).map (λ n, @unchecked_cast ℕ ℤ (2^n - 1))
-- [0, 1, 3, 7, 15, 31, 63, 127, 255, 511, 1023, 2047, 4095, 8191, 16383,
--  32767, 65535, 131071, 262143, 524287, 1048575, 2097151, 4194303, 8388607,
--  16777215, 33554431, 67108863, 134217727, 268435455, 536870911, 1073741823,
--  -1, 4294967295, 8589934591]


#### Kevin Buzzard (Jun 10 2020 at 14:49):

When I've got my number theorists hat on and I find a non-OEIS sequence I add it! But I'm not sure they'll like this one...

#### Kevin Buzzard (Jun 10 2020 at 14:50):

Kenny Lau said:

guess the outputs:

#eval @unchecked_cast empty ℕ (unchecked_cast tt)
#eval @unchecked_cast empty ℕ (unchecked_cast ff)


http://bash.org/?10958 (aah, the old days)

Last updated: May 08 2021 at 03:17 UTC