Missing numeric conversion type classes?

Stream: new members

[Tom]

It seems there are functions such as

UIntX.ofNat as well as Int.ofNat, Float.ofNat, Fin.ofNat etc. Most of these also have a corresponding T.toNat (with the exception of Float and Fin, which potentially seems like an omission)

However, I can't seem to find any type classes which would support these operations, which makes it hard to write generic numeric code. Does something like that exist? Do I need to somehow manually invoke Coe.coe?

[Derek Rhodes]

Hi, maybe you've seen this page from the docs, that shows the typeclass Coe being instantiated with two parameters:

instance : Coe Nat Int := ⟨Int.ofNat⟩

As for manually invoking a coercion, are you familiar with the up arrow? From the same page ^^

You can also use the ↑ operator to explicitly indicate a coercion.

Maybe posting a specific piece of code that demonstrates the problematic generic code would help others pin down better suggestions.

[Daniel Weber]

There is docs#NatCast

[Daniel Weber]

If you want to write proofs I think you should use docs#AddMonoidWithOne (and strengthen it if you need stronger assumptions)

[Eric Wieser]

Daniel Weber said:

There is docs#NatCast

Nat.cast is the preferred spelling of the function performing the coercion

[Tom]

Hi,

Thanks everyone for helping me out and the pointers to documentation. I really appreciate it. As I mentioned, I was "aware" of the Coe type class but perhaps using it wrong. Let me write down some examples of the kinds of issues I was running into:

def nat : Nat := 10

def a : Int := Coe.coe (β := Int) nat -- Does not work (why?)
def b : Int := ((nat : Nat) : Int)     -- Docs say this is an alternate syntax for "uparrow".
                                       -- Not sure why I have to spell the "current" type again unless it's something hardcoded
                                       -- in the parser?
def c : Int := ↑nat

Why does the explicit type class syntax not work? My understanding is that that's what's the "sugar" is doing.

[Tom]

Now, while this seems to work for the above, the following examples do not work for me:

def d : Float := ((nat : Nat) : Float) -- Does not work
def e : Float := ↑n                                 -- Does not work

def float : Float := 1.3
def f : Nat := ↑float                                 -- Does not work

Now, I am guessing that this is because these conversions are not "safe" in the numeric sense but then that would mean that Coe cannot apply to these things in day-to-day programming when I know it's safe and don't want to have to prove. Interestingly, all the toNat etc functions which are associated with specific types happily convert back and forth by e.g. just throwing away bits.

[Tom]

To further understand/illustrate my point, I wrote a helper

def test_conversions (α : Type) (n : Nat) [Coe Nat α ] [Coe α  Nat]: α :=
  let conv: α := ↑n
  let ret_conv: Nat := ↑conv
  ret_conv

[Tom]

Note that none of UInt8/16/32 etc work with this function! Yet,

#check test_conversions (UInt8) 1
-- But this works
def nn := 10000           -- Even though it's "out of range"
def ui8 : UInt8 := UInt8.ofNat nn
#eval nn.toUInt8
#eval ui8.toNat

[Tom]

It's a similar story for Fin and Float:

-- Doesn't work
#check test_conversions (Fin 100) 1           -- Doesn't work
def fin_bad : Fin 1001 := ↑(nn) -- Does not work
def fin : Fin 100 := Fin.ofNat nn -- Have to say, coe is not working.
#eval fin

-- Doesn't work
#check test_conversions (Float) 1                   -- Doesn't work
def float_bad : Float:= ↑(nn) -- Does not work
def flt : Float := Float.ofNat nn -- Have to say
#eval flt

[Edward van de Meent]

if you replace Coe with CoeHTCT, your test_conversions should be a bit more general...

[Edward van de Meent]

i think it still won't work with UInt8 and the like though, because you'd rather not such lossy casting happens implicitly...

[Tom]

Hi @Edward van de Meent

I guess there a few observations here:

1) I've never even heard of CoeHTCT. From a "learner" perspective, I don't see any mentioned of it in either FPiL or TPiL, so it's hard to know if it's just an implementation detail or should be used by users.

2) As a programmer, with my current impression is that converting between numerical types is very inconsistent/haphazard. Some things convert and just "reinterpret", even if values are "out of range". Sometimes explicit conversions compile, and sometimes they don't.

3) I seem to be missing some type classes to reach for - e.g. (an unsafe) ofNat seems to exist on (most?) of the built-in types but I can't seem to find a type class where I could do this generically. I can't find a similar thing for toX either.

I guess I was trying to learn to write some generic code but am running into a lot of roadblocks.

[Edward van de Meent]

if you'd like, i could try and explain exactly how the Coe-family of typeclasses works, but i find the documentation for this (which is in the defining file) is well-written...

[Tom]

Hi @Edward van de Meent

I appreciate your continued help. I want to assure you that I am trying to read documentation but as I mentioned, some of type classes are not mentioned in either one of the "reference" texts, such as FPiL or TPiL.

I am interpreting your last suggestion as "go read the Init/Coe.lean code, ie. parts of the implementation of the compiler. I had looked at that file but it specifically says:

On top of these instances this file defines several auxiliary type classes:
 <snip>
  * `CoeHTCT := CoeHead? CoeOut* Coe* CoeTail?`

Which is why I think this may not be for "users" and certainly not for someone like me just trying to learn the ropes! :smile:
In fact, the documentation string (aside from being basically identical to Coe), says

/--
Auxiliary class implementing `CoeHead* Coe* CoeTail?`.
Users should generally not implement this directly.
-/
class CoeHTCT (α : Sort u) (β : Sort v) where
  /-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
  or by double type ascription `((x : α) : β)`. -/
  coe : α → β
attribute [coe_decl] CoeHTCT.coe

Hopefully this clarifies why I'm not sure of the "correct way" of accomplishing what I'm looking for.

Thanks.

[Kyle Miller]

You can use set_option trace.Meta.synthInstance true to see what typeclasses are being used during coercion.

set_option trace.Meta.synthInstance true
def a : Int := nat
-- [Meta.synthInstance] ✅️ CoeT ℕ nat ℤ

[Kyle Miller]

The elaborator has special support for coercions as well, including unfolding the coe function once a coercion has been found. You shouldn't use these functions directly.

[Kyle Miller]

No need to write def b : Int := ((nat : Nat) : Int) , def b : Int := (nat : Int) will do.

[Kyle Miller]

For numbers, it's important that all the coercions for numbers form a directed acyclic graph, and that none of the coercions are lossy. Coercions can be chained. What's to stop 5 : Nat from going through Fin 2 and back to Nat?

[Kevin Buzzard]

What should be stopping it is no coercion from Nat to Fin 2 ;-) but people don't like to put in the proof that n < 2...

[Kevin Buzzard]

In fact right now all of these work fine:

import Mathlib

example (n : ℕ) : Fin 2 := n

example (nbar : Fin 2) : ℕ := nbar

example : Fin 2 := (1 : ℕ)

example : ℕ := (1 : Fin 2)

so I don't quite understand Kyle's last point.

[Tom]

@Kevin Buzzard

What should be stopping it is no coercion from Nat to Fin 2 ;-) but people don't like to put in the proof that n < 2...

While I am excited to continue exploring Lean as a vehicle toward learning more about mathematics and formal systems (obviously not to the same degree as someone as yourself), I am primarily interested in using it for programming. I like the idea of using stricter types to build more correct programs and have the option of proving certain properties if I chose to.

I guess there eventually need to be some parts of the language/library which allow me to say "I know this is fine", e.g. converting a Nat to a Float, perhaps similar to how I can choose to avoid proving the termination of a def by saying partial def. Kind of reminds me of the unsafe blocks in e.g. Rust, if you know what I mean.

[Kyle Miller]

@Kevin Buzzard Mathlib's had a bug for a while due to the fact it introduces a coercion from Nat to Fin 2. Core does not have this.

-- In core Lean
#eval (5 : Nat) = (1 : Fin 2)
-- false
#eval (1 : Fin 2) = (5 : Nat)
-- false

-- In mathlib:
#eval (5 : Nat) = (1 : Fin 2)
-- false
#eval (1 : Fin 2) = (5 : Nat)
-- true (!)

[Kyle Miller]

Context: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib4.20.60calc.60.20issue.3F/near/438679909

[Daniel Weber]

Tom said:

[...]

I guess there eventually need to be some parts of the language/library which allow me to say "I know this is fine", e.g. converting a Nat to a Float, perhaps similar to how I can choose to avoid proving the termination of a def by saying partial def. Kind of reminds me of the unsafe blocks in e.g. Rust, if you know what I mean.

For floats in particular I think that there is very little on Lean about them, because everything about it is opaque, i.e. nothing can be proven about it, so general type classes don't work well for it. You can add local instances if you want to have those coercions locally, using docs#Float.ofNat. A function from Float to Nat does seem to be missing, but you can go through docs#Float.toRat0 and then convert the rational number to a Nat