# Zulip Chat Archive

## Stream: new members

### Topic: Chaining coercions

#### Kevin Sullivan (Feb 11 2021 at 02:50):

Hi Folks, A question about chaining of coercions. I start with three types, X, Y, and Z, and define pairwise coercions in both directions: from X to Y and Y to X and from Y to Z and Z to Y. Coercions of X-valued objects to Z then works fine, and from Z to X as well. However, if I now add a "branch" in the coercion graph, say from X to Y' and back, the automatic chaining of coercions (at least from X-Z and Z-X) now fails. What are the constraints on how complex a graph of coercions can be, in which automatic chaining will continue to work, and why? Thanks! --Kevin S

#### Mario Carneiro (Feb 11 2021 at 02:51):

X to Y and back is bad, that's a typeclass cycle and will make all typeclass inference problems fail

#### Mario Carneiro (Feb 11 2021 at 02:52):

You can have X to Y and back if you inhabit `has_coe_t`

instead since it won't try to chain them

#### Kevin Sullivan (Feb 11 2021 at 02:55):

Mario Carneiro said:

X to Y and back is bad, that's a typeclass cycle and will make all typeclass inference problems fail

I see. Interesting. The use case is that I have a tree of isomorphic types, and I'd like to have automated coercions between any two types in the tree. Any thoughts on how we might obtain such a capability?

#### Mario Carneiro (Feb 11 2021 at 02:56):

You could have a coe `A -> X`

and a coe_t `X -> A`

for all A and some chosen X

#### Kevin Sullivan (Feb 11 2021 at 02:57):

Mario Carneiro said:

You could have a coe

`A -> X`

and a coe_t`X -> A`

for all A and some chosen X

I will let you know how that works out. Thanks a ton as always, Mario.

#### Mario Carneiro (Feb 11 2021 at 03:00):

```
structure foo := (out : nat)
structure bar := (out : nat)
structure baz := (out : nat)
instance foo_nat : has_coe foo nat := ⟨foo.out⟩
instance bar_nat : has_coe bar nat := ⟨bar.out⟩
instance baz_nat : has_coe baz nat := ⟨baz.out⟩
instance nat_foo : has_coe_t nat foo := ⟨foo.mk⟩
instance nat_bar : has_coe_t nat bar := ⟨bar.mk⟩
instance nat_baz : has_coe_t nat baz := ⟨baz.mk⟩
variables (a : foo) (b : bar) (c : baz)
#check (a : foo)
#check (a : bar)
#check (a : baz)
#check (b : foo)
#check (b : bar)
#check (b : baz)
#check (c : foo)
#check (c : bar)
#check (c : baz)
```

#### Kevin Sullivan (Feb 11 2021 at 03:06):

Basic types for tree of linear spaces .

```
abbreviation coord := ℕ
mutual inductive space, frame
with space : Type
| base
| der : frame → space
with frame : Type
| std
| new : space → ℕ → frame
-- open space frame
def getf : space → frame
| space.base := frame.std
| (space.der f) := f
def gets : frame → space
| frame.std := space.base
| (frame.new s n) := s
-- get coord of new frame relative to old frame
def getc : frame → coord
| frame.std := 1
| (frame.new f n) := n
-- get old frame on which which frame is built
-- std frame is built on itself
def geto : frame → frame
| frame.std := frame.std
| (frame.new s n) := getf s
inductive point (s : space) : Type
| mk : ℕ → point
def getps : ∀ {s : space}, point s → space
| s p := s
def getpf : ∀ {s : space}, point s → frame
| s p := getf s
```

A simple demo/test case.

```
import .space_tree
--
def s0 : space := space.base -- implicit std frame
def f0 := getf s0 -- standard frame
def f1 := frame.new s0 2 -- new basis coord 2
def s1 := space.der f1
def f2 := frame.new s1 3 -- new basis coord 3
def s2 := space.der f2
def f1' := frame.new s0 5
def s1' := space.der f1'
-- forward and backward transforms
def pt_0_1 : point s0 → point s1
| (point.mk n) :=
let f := (getf s1) in
let c := (getc f) in
(point.mk (n/c))
def pt_1_0 : point s1 → point s0
| (point.mk n) :=
let f := (getf s1) in
let c := (getc f) in
(point.mk (n*c))
--
def pt_0_1' : point s0 → point s1'
| (point.mk n) :=
let f := (getf s1) in
let c := (getc f) in
(point.mk (n/c))
def pt_1'_0 : point s1' → point s0
| (point.mk n) :=
let f := (getf s1) in
let c := (getc f) in
(point.mk (n*c))
--
def pt_1_2 : point s1 → point s2
| (point.mk n) :=
let f := (getf s2) in
let c := (getc f) in
(point.mk (n/c))
def pt_2_1 : point s2 → point s1
| (point.mk n) :=
let f := (getf s2) in
let c := (getc f) in
(point.mk (n*c))
--
instance pt_1_0_coe :
has_coe (point s1) (point s0) :=
⟨pt_1_0⟩
instance pt_0_1_coe :
has_coe_t (point s0) (point s1) :=
⟨pt_0_1⟩
--
instance pt_1'_0_coe :
has_coe (point s1') (point s0) :=
⟨pt_1'_0 ⟩
instance pt_0_1'_coe :
has_coe_t (point s0) (point s1') :=
⟨pt_0_1' ⟩
--
instance pt_2_1_coe :
has_coe (point s2) (point s1) :=
⟨pt_2_1⟩
instance pt_1_2_coe :
has_coe_t (point s1) (point s2) :=
⟨pt_1_2⟩
--
/-
Hmm: Need an explicit has_coe_t from
point s0 to point s2.
-/
--
def p0 : point s0 := point.mk 12
def p2 : point s2 := point.mk 2
def p01 : point s1 := p0 -- coerce
def p12 : point s2 := p01 -- coerce
def p02 : point s2 := p0 -- coerce chain
#reduce p01 -- expect 6
#reduce p12 -- expect 2
#reduce p02 -- expect 2 (chained)
def p21 : point s1 := p2 -- coerce
def p10 : point s0 := p21 -- coerce
def p20 : point s0 := p2 -- coerce chain
#reduce p21 -- expect 6
#reduce p10 -- expect 12
#reduce p20 -- expect 12 (chained)
```

#### Kevin Sullivan (Feb 11 2021 at 03:48):

Mario Carneiro said:

`structure foo := (out : nat) structure bar := (out : nat) structure baz := (out : nat) instance foo_nat : has_coe foo nat := ⟨foo.out⟩ instance bar_nat : has_coe bar nat := ⟨bar.out⟩ instance baz_nat : has_coe baz nat := ⟨baz.out⟩ instance nat_foo : has_coe_t nat foo := ⟨foo.mk⟩ instance nat_bar : has_coe_t nat bar := ⟨bar.mk⟩ instance nat_baz : has_coe_t nat baz := ⟨baz.mk⟩ variables (a : foo) (b : bar) (c : baz) #check (a : foo) #check (a : bar) #check (a : baz) #check (b : foo) #check (b : bar) #check (b : baz) #check (c : foo) #check (c : bar) #check (c : baz)`

Here's more what I'm looking for. This example subsumes yours and illustrates the problem. I'm not a typeclass inferencing person, but might not an inferencer just stop when it detects a cycle, and move on if necessary? (Yeah, that's why I post in beginners.)

`structure foo := (out : nat) structure bar := (out : nat) structure baz := (out : nat) structure bam := (out : nat) /- nat ^ ^ | | v v foo bar ^ ^ | | v v bam baz -/ -- ^ arrows instance foo_nat : has_coe foo nat := ⟨foo.out⟩ instance bam_foo : has_coe bam foo := ⟨λ m, foo.mk m.out⟩ instance bar_nat : has_coe bar nat := ⟨bar.out⟩ instance baz_bar : has_coe baz bar := ⟨λ bz, bar.mk bz.out⟩ -- v arrows instance nat_foo : has_coe_t nat foo := ⟨foo.mk⟩ instance foo_bam : has_coe_t foo bam := ⟨λ f, bam.mk f.out⟩ instance nat_bar : has_coe_t nat bar := ⟨bar.mk⟩ instance bar_baz : has_coe_t bar baz := ⟨λ r, baz.mk r.out⟩ -- what works and what breaks? variables (f : foo) (r : bar) (z : baz) (m : bam) #check ((1 : nat) : foo) #check ((1 : nat) : bar) #check ((1 : nat) : bam) -- no: no downward chaining #check ((1 : nat) : baz) -- no: no downward chaining #check (f : nat) #check (m : nat) #check (r : nat) #check (z : nat) #check (m : bar) -- one coe_t at end of chain ok #check (z : foo) -- works symmetrically #check (m : baz) -- no: at most one coe_t at end #check (z : bam) -- no: symmetric /- Looks like I need to write an explicit has_coe_t for each link in the transitive closure of the down-pointing arrows minus the down-pointing arrows already written. Better than nothing but not great. Best we can do? -/`

#### Mario Carneiro (Feb 11 2021 at 03:52):

I'm not a typeclass inferencing person, but might not an inferencer just stop when it detects a cycle, and move on if necessary?

Yes. Lean 3's algorithm is bad, Lean 4's is better and mostly solves this problem

#### Mario Carneiro (Feb 11 2021 at 03:55):

Like I said, you need a coe from A -> X and coe_t from X -> A for varying A and fixed (privileged) X; this is a star graph of coercions. A general graph isn't going to cut it because you need at most one edge in every path to be a coe_t edge (and in fact the coe_t edge has to be the last in the path)

#### Kevin Sullivan (Feb 11 2021 at 03:59):

Mario Carneiro said:

I'm not a typeclass inferencing person, but might not an inferencer just stop when it detects a cycle, and move on if necessary?

Yes. Lean 3's algorithm is bad, Lean 4's is better and mostly solves this problem

I see. Do you happen to know where I can read more about the new approach?

Here's a more general form of the problem, I suppose:

Given (statically) a collection, C = { T }, of isomorphic types, and a connected tree (dag, graph, etc), S, of pairwise bijections between types in C, generate coercions for each edge in the complete directed graph over C.

#### Mario Carneiro (Feb 11 2021 at 04:02):

https://arxiv.org/abs/2001.04301

It's probably not especially useful to you though

#### Mario Carneiro (Feb 11 2021 at 04:03):

The problem is that typeclass resolution is far more general than your statement

#### Mario Carneiro (Feb 11 2021 at 04:03):

so we need an algorithm that solves the general case but also does the smart thing in this restricted setting

#### Mario Carneiro (Feb 11 2021 at 04:04):

The problem as posed is easy; you can use e.g. tarjan's algorithm for finding SCC's in a directed graph

#### Mario Carneiro (Feb 11 2021 at 04:05):

but it's a challenge to make that work within the constraints of lean 3 coercions

#### Mario Carneiro (Feb 11 2021 at 04:05):

if you are fine with a tactic doing the coercion you have a lot more flexibility

#### Kevin Sullivan (Feb 11 2021 at 04:05):

Mario Carneiro said:

https://arxiv.org/abs/2001.04301

It's probably not especially useful to you though

Yes. What I'm wondering, very pragmatically, is whether Lean 4's approach solves my problem?

#### Mario Carneiro (Feb 11 2021 at 04:06):

I'm not entirely sure, you could try it

#### Kevin Sullivan (Feb 11 2021 at 04:06):

Also, yes, I could write a tactic. But I'm lazy. And yes I'll give it a try in Lean 4 and report back. Thank you for the conversation. It's clear to me now where things stand with Lean 3. Love this community.

#### Mario Carneiro (Feb 11 2021 at 04:07):

The problem with a tactic is that it's not invisible

#### Kevin Sullivan (Feb 11 2021 at 04:07):

Mario Carneiro said:

The problem with a tactic is that it's not invisible

Aye

#### Mario Carneiro (Feb 11 2021 at 04:07):

coercion does not require any syntax, tactics don't get that luxury

#### Mario Carneiro (Feb 11 2021 at 04:08):

mathlib has lots of `by exactI`

in it which ideally you wouldn't have to see at all

#### Kevin Sullivan (Feb 11 2021 at 04:09):

Mario Carneiro said:

coercion does not require any syntax, tactics don't get that luxury

Very interesting.

Last updated: May 10 2021 at 00:31 UTC