alternate notation for nat.cast?

Stream: general

[Mario Carneiro]

This is a response to issues like https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Weird.20error.20message/near/164587381 and #946 . What do people think about having a separate notation just for nat.cast and friends? Like so:

class has_cast (α β : Type*) := (cast : α → β)
prefix `↟`:max := has_cast.cast
instance {α : Type*} [semiring α] : has_cast ℕ α := ⟨nat.cast⟩
instance {α : Type*} [ring α] : has_cast ℤ α := ⟨int.cast⟩
instance {α : Type*} [division_ring α] : has_cast ℚ α := ⟨rat.cast⟩

That's the up-up sign ↟ = \uu; I'm open to other notational choices. The important thing is that it's not a coercion, which can cause unpleasant surprises because it's a computationally very expensive operation. Also because it is not hooked into the coercion framework there is no question of transitivity searches for these instances, and taking these out of the coercion framework fixes the issue with forward searching for coercions.

[Johan Commelin]

@Mario Carneiro Does this mean that we will always have to explicitly type \uu in front if natural numbers if we want to cast them? (Will the casts to int, rat, real, and complex still be coercions?)

[Mario Carneiro]

yes

[Mario Carneiro]

the casts from other number types will be using this new notation as well

[Mario Carneiro]

We could define coercions as well between the number types specifically, but I don't think it's a good idea to have too many ways to say this

[Mario Carneiro]

The coercion from nat to int will still be the coercion int.of_nat

[Johan Commelin]

It still feels like duct tape to me.

[Johan Commelin]

The coercion framework ought to be able to take care of this.

[Mario Carneiro]

I don't think it's possible for the coercion framework to handle this, support transitivity, and be implemented by typeclass inference

[Johan Commelin]

Can we make type class inference smarter, to solve this issue?

[Mario Carneiro]

But actually I think the explicit arrow is a good thing here. The arrow is already present whenever you print statements or are proving things, so hiding it completely is not really useful for proving stuff. It might be useful for the programmers, but they have already weighed in against this coercion

[Mario Carneiro]

If hiding it completely meant you didn't have to invoke any theorems or anything and they were just the same, I would be on board, but if you have to manipulate it then hiding the function is counterproductive

[Johan Commelin]

The cool thing is that it isn't present when you are reading things. I like the cleaner statements

[Mario Carneiro]

there is still a type ascription, usually. Double type ascriptions always look weird

[Johan Commelin]

Also... you could argue the same about coercions in general. Why shouldn't we always write the arrow?

[Mario Carneiro]

why shouldn't we?

[Johan Commelin]

What is the fundamental difference between a cast and a coe? In my mind they are the same thing.

[Mario Carneiro]

Like I said, it can be useful in programming contexts where the coercion appears only once, in the program text, and you are never going to go back through this term. But for defs and theorems in mathematics, you are always coming back to the statements later so that doesn't apply

[Johan Commelin]

No, I don't get it. Sorry for being dense. What makes a cast a cast and a coe a coe?

[Mario Carneiro]

There isn't really a difference, they are basically accomplishing the same thing. In this case the distinguishing feature is that all the cast instances are blanket instances on the codomain, while coe instances usually have a simpler RHS

[Johan Commelin]

Ok, I see.

[Mario Carneiro]

(that was a response to the "always write the arrow" comment)

[Mario Carneiro]

In particular, coe_trans instances require the problem has_coe a ?b to have a finite number of instances for any concrete a

[Johan Commelin]

Can't we make type class inference smarter?

[Johan Commelin]

My brain is able to solve these problems very quickly. And it never explicitly considered casts and coes as different things

[Mario Carneiro]

We almost never use coe transitivity in practice, and in fact we have to rewrite it away when it appears, but I'm sure there is some edge case where it's needed

[Mario Carneiro]

Also typeclass inference isn't very smart (aka "prolog-like search"). We could make it smarter but it wouldn't be typeclass inference anymore, and it probably wouldn't be as much of a swiss army knife

[Johan Commelin]

@Mario Carneiro Is there any literature about type class inference and the problems and challenges involved? I know about prolog-like search... but I would like to read a survey of the alternatives and their downsides.

[Simon Hudon]

This might be a good start: https://link.springer.com/chapter/10.1007/978-3-540-71067-7_23

[Johan Commelin]

@Simon Hudon Thanks for the link. I'll try tomorrow when I'm at the uni to see if I can reach behind springer's paywall.