Chaining coercions

Stream: new members

[Kevin Sullivan]

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]

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

[Mario Carneiro]

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]

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]

You could have a coe A -> X and a coe_t X -> A for all A and some chosen X

[Kevin Sullivan]

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]

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]

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]

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]

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]

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]

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]

https://arxiv.org/abs/2001.04301

It's probably not especially useful to you though

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Sullivan]

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]

I'm not entirely sure, you could try it

[Kevin Sullivan]

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]

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

[Kevin Sullivan]

Mario Carneiro said:

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

Aye

[Mario Carneiro]

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

[Mario Carneiro]

mathlib has lots of by exactI in it which ideally you wouldn't have to see at all

[Kevin Sullivan]

Mario Carneiro said:

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

Very interesting.