unchecked cast

Stream: general

[Kenny Lau]

#eval @unchecked_cast int nat (-3) -- 2147483645
#eval @unchecked_cast (list nat) (list nat) [3] -- [3]
#eval @unchecked_cast nat (list nat) 3 -- []
#eval @unchecked_cast nat (nat → nat) 3 3
-- vm check failed: cidx(closure) == 0 (possibly due to incorrect axioms, or sorry)
#eval @unchecked_cast (list (list nat)) (list nat) [[3]]
-- vm check failed: is_mpz(o) (possibly due to incorrect axioms, or sorry)

[Kenny Lau]

quite fun

[Kevin Buzzard]

can you cast int to nat?

[Kevin Buzzard]

Lean always has fun trying to do that

[Kevin Buzzard]

oh duh that's exactly what you just did

[Kevin Buzzard]

Is this related to why Lean times out if you try to do this?

[Chris Hughes]

I doubt it. I don't think the kernel or the elaborator care about the VM representation.

[Kevin Buzzard]

How come the VM can deal with integers bigger than 2^32 if it is storing things in this classical manner?

[Kenny Lau]

#eval @unchecked_cast int nat (-21474836450) -- -21474836450

[Kenny Lau]

looks like -21474836450 is a natural number!

[Keeley Hoek]

@Kevin Buzzard for small enough integers it stores them in 4-bytes, for bigger ones it uses the GMP multiprecision library

[Chris Hughes]

How come the VM can deal with integers bigger than 2^32 if it is storing things in this classical manner?

My guess is that a nat is 31 bits for the nat, plus one more bit that says we need more bits. An int is probably 30 bits plus a sign and one more bit for if we need more bits.

#eval @unchecked_cast nat int (2 ^ 30) -- -1073741824

[Keeley Hoek]

https://gmplib.org

[Kevin Buzzard]

rofl the "need help" bit.

[Reid Barton]

Interesting, it hadn't occurred to me that you could define unchecked_cast (in meta) yourself, without a special constant.
I wonder how badly you can break things with it. I tried casting a nat to a function nat -> nat and then applying it, hoping for a crash, but all I got was a boring vm check failure.