explicit class-based conversion

Stream: Is there code for X?

[JJ]

lean offers implicit class-based coersion: https://leanprover-community.github.io/mathlib4_docs/Init/Coe.html

does explicit class-based conversion exist? i have found myself writing a considerable amount of helper methods like the below for type conversion and it seems like there simply must be a better way. does something akin to rust's From/Into traits exist?

namespace BitVec
def ofUInt8 (n : Nat) (i : UInt8) : BitVec n :=
  BitVec.ofNat n <| UInt8.toNat i
end BitVec

namespace Array
def ofUInt32 (long : UInt32) : Array Byte :=
  #[UInt8.ofNat <| UInt32.toNat long >>> 24, UInt8.ofNat <| UInt32.toNat long >>> 16,
    UInt8.ofNat <| UInt32.toNat long >>> 8, UInt8.ofNat <| UInt32.toNat long]
end Array

[JJ]

i.e. i'm looking for the following:

class Convert (α : Sort u) (β : Sort v) where
  to : α → β

[Eric Wieser]

Lean3 had docs3#lift / docs3#has_lift for this

[Edward van de Meent]

isn't this just docs#Coe ?

[Edward van de Meent]

(see also docs#CoeOut )
i now see you already found that...

[JJ]

i'm mostly looking for a way to not need to explicitly say FromType.toNewType foo every time i want to convert types

let a : α := sorry
let b : β := a.to  -- when the type is known, no need to re-specify in method name
let g := a.to[γ]   -- when the type is unknown, specify as a generic

it would also be cool if this would resolve things transitively, i.e. if there is an instance of Convert for α → β and an instance from β → γ, ((a : α).to : γ) would Just Work

[Edward van de Meent]

looking at it, i'd say you could do some adapting to use the existing Coe infrastructure... however, i don't know you can get the dot-notation to work...
the following might help:

abbrev coeTo (α :Type u) {β : Type v} [CoeTC β α] : β → α := CoeTC.coe

[Edward van de Meent]

which allows coeTo α b assuming [CoeTC β α] exists (rather than the notation of b.coeTo α you suggested)

[JJ]

hmm, but my impression is that Coe is for implicit coersion, and implementing Coe or any related classes for some types will add them to that system. i don't want implicit coersion b/c i don't want ex. UInt32 to be implicitly coerced to an Array UInt8, but i would like explicit ((foo : UInt32).to : Array UInt8) to work

[Edward van de Meent]

the following might work?

universe u v

class Convert (α :  semiOutParam (Type v)) (β : Type u) where
  convert : α → β

instance Coe.toConvert [Coe α β] : Convert α β where convert := Coe.coe
export Coe (toConvert)

class ConvertTC (α :  semiOutParam (Type v)) (β : Type u) where
  convert : α → β

instance ConvertTC.cons [Convert β γ] [ConvertTC α β] : ConvertTC α γ where
  convert a := Convert.convert (ConvertTC.convert a : β)

instance ConvertTC.single [Convert α β] : ConvertTC α β where
  convert a := Convert.convert a

instance ConvertTC.id: ConvertTC α α where convert a := a

def convertTo (β : Type u) {α : Type v} [ConvertTC α β] : α → β := ConvertTC.convert

this adds the existing Coe classes to the new Convert system, but since these aren't marked with the @[coe] attribute i'd guess that new Convert instances don't get implicitly inserted?

[Edward van de Meent]

btw, the TC stands for Transitive Closure, if someone didn't make that connection before

[Kevin Buzzard]

I have never understood how the coercion system works in lean 4 with all this CoeTC etc. I wonder if you can just use the coercion system as is but you just have to be an expert to implement it

[Edward van de Meent]

Just did a dive into the file defining these coe-classes, and i have to say it is quite enlightening.

the issue with extending the existing infra is that the top class in the hierarchy automatically gets tied into the system: if you add only to classes the bottom, you don't get to add new coercions; if you add only to the top of the hierarchy, everything you do gets tied into the system; if you add a separate hierarchy, you don't get to leverage existing coercions.

there may be a solution using attributes/options/other magic i dont know about. particularly i don't know how how the coe_decl attribute is handled/what it gets used for, which may be significant.
The only solution to this that i can think of would be to add a second layer to the hierarchy which runs parallel on top of the existing one, but is connected per (base) class. This leads to duplicating quite some code, unfortunately...

[Eric Wieser]

A way to avoid duplication would be to change Coe X Y : Type to Coe X Y isImplicit

[Eric Wieser]

(where isImplicit : Bool or belongs to some enum type)

[Eric Wieser]

This would need an RFC, since obviously this is a nontrivial change to core

[JJ]

okay, cool. i might make an RFC to extend Coe when i am more familiar with the language. for now, i think i'll play around with implementing my own local Conv class in my projects.

[Edward van de Meent]

Eric Wieser said:

A way to avoid duplication would be to change Coe X Y : Type to Coe X Y isImplicit

that avoids duplicating the classes, sure. however, i think that might double/triple the instances necessary to make the transitive synthesis work?

[Edward van de Meent]

because you'd need something like this:

instance [Coe β γ NotImplicit] [CoeTC α β x] : CoeTC α γ NotImplicit := ...
instance [Coe β γ x] [CoeTC α β NotImplicit] : CoeTC α γ NotImplicit := ...
instance [Coe β γ IsImplicit] [CoeTC α β IsImplicit] : CoeTC α γ IsImplicit := ...

[Edward van de Meent]

at least, i think something like this might not work because of transparency issues?

instance [Coe β γ x] [CoeTC α β y] : CoeTC α γ (x ∧ y) := ...

[Edward van de Meent]

or free variable issues?

[Edward van de Meent]

having a bit of a try, it requires 4(!) (not factorial) instances due to the free variable issue.