Zulip Chat Archive

Stream: new members

Topic: Chaining coercions


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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?
-/

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 11 2021 at 04:02):

https://arxiv.org/abs/2001.04301

It's probably not especially useful to you though

view this post on Zulip Mario Carneiro (Feb 11 2021 at 04:03):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 11 2021 at 04:05):

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

view this post on Zulip Mario Carneiro (Feb 11 2021 at 04:05):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 11 2021 at 04:06):

I'm not entirely sure, you could try it

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 11 2021 at 04:07):

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

view this post on Zulip Kevin Sullivan (Feb 11 2021 at 04:07):

Mario Carneiro said:

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

Aye

view this post on Zulip Mario Carneiro (Feb 11 2021 at 04:07):

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

view this post on Zulip 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

view this post on Zulip 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