## Stream: general

### Topic: alternate notation for nat.cast?

#### Mario Carneiro (May 01 2019 at 01:23):

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 (May 01 2019 at 04:17):

@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?)

yes

#### Mario Carneiro (May 01 2019 at 04:18):

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

#### Mario Carneiro (May 01 2019 at 04:19):

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 (May 01 2019 at 04:20):

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

#### Johan Commelin (May 01 2019 at 04:21):

It still feels like duct tape to me.

#### Johan Commelin (May 01 2019 at 04:22):

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

#### Mario Carneiro (May 01 2019 at 04:23):

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

#### Johan Commelin (May 01 2019 at 04:24):

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

#### Mario Carneiro (May 01 2019 at 04:25):

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 (May 01 2019 at 04:26):

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 (May 01 2019 at 04:26):

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

#### Mario Carneiro (May 01 2019 at 04:27):

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

#### Johan Commelin (May 01 2019 at 04:27):

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

#### Mario Carneiro (May 01 2019 at 04:27):

why shouldn't we?

#### Johan Commelin (May 01 2019 at 04:28):

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

#### Mario Carneiro (May 01 2019 at 04:29):

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 (May 01 2019 at 04:30):

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

#### Mario Carneiro (May 01 2019 at 04:30):

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

Ok, I see.

#### Mario Carneiro (May 01 2019 at 04:31):

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

#### Mario Carneiro (May 01 2019 at 04:32):

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 (May 01 2019 at 04:34):

Can't we make type class inference smarter?

#### Johan Commelin (May 01 2019 at 04:35):

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

#### Mario Carneiro (May 01 2019 at 04:39):

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 (May 01 2019 at 04:41):

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 (May 01 2019 at 04:59):

@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 (May 01 2019 at 11:51):

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

#### Johan Commelin (May 01 2019 at 13:19):

@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.

Last updated: May 16 2021 at 20:13 UTC