Parent to Subtype coercion

Stream: general

[nrs]

def Digit := @Subtype Char (fun c => c.isDigit)

Is it possible to define a coercion such that the following will typecheck?

def myDigit : Digit := '5'

[Kyle Miller]

Option 1: define a Coe instance, and if the data is invalid, replace it with a default value. Maybe use panic! too so you get a runtime error that this happened.

Option 2: define a term elaborator toDigit and write toDigit '5', where the elaborator synthesizes a proof that Char.isDigit holds.

[Kyle Miller]

Any particular reason you didn't write it in the following more canonical way?

def Digit := { c : Char // c.isDigit }

[nrs]

Kyle Miller said:

Option 1: define a Coe instance, and if the data is invalid, replace it with a default value. Maybe use panic! too so you get a runtime error that this happened.

Option 2: define a term elaborator toDigit and write toDigit '5', where the elaborator synthesizes a proof that Char.isDigit holds.

I've been attempting the Coe instance path, but how do I suspend evaluation of the proof until the actual coercion? e.g. the following will fail because the proof evaluates immediately

instance : Coe Char Digit where
  coe c := .mk c (fun c => c.isDigit)

[Kyle Miller]

That fails also because (fun c => c.isDigit) is not a proof of c.isDigit

[nrs]

Kyle Miller said:

def Digit := { c : Char // c.isDigit }

ah this is neat! ty

[Kyle Miller]

but in any case, you have to think about the fact that a coercion is a function Char -> Digit. It has to succeed on all Chars

[Kyle Miller]

(I figured you might have known about this syntax given your question yesterday.)

[nrs]

Kyle Miller said:

but in any case, you have to think about the fact that a coercion is a function Char -> Digit. It has to succeed on all Chars

so necessarily even 'a' and 'b' will need to coerce to a Digit?

[Kyle Miller]

Yes, that's the contract for Coe

[Kyle Miller]

Here's an example:

def Digit := { c : Char // c.isDigit }
instance : Inhabited Digit := ⟨'0', rfl⟩

def Digit.ofChar (c : Char) : Digit :=
  if h : c.isDigit then
    ⟨c, h⟩
  else
    panic! "not a digit"

instance : Coe Char Digit where
  coe := Digit.ofChar

def myDigit : Digit := '5'

#eval myDigit
-- '5'

[nrs]

Kyle Miller said:

Here's an example:

def Digit := { c : Char // c.isDigit }
instance : Inhabited Digit := ⟨'0', rfl⟩

def Digit.ofChar (c : Char) : Digit :=
  if h : c.isDigit then
    ⟨c, h⟩
  else
    panic! "not a digit"

instance : Coe Char Digit where
  coe := Digit.ofChar

def myDigit : Digit := '5'

#eval myDigit
-- '5'

ah I see! thank you very much for the example!

[Kyle Miller]

Then

def myBadDigit : Digit := 'A'
#eval myBadDigit
/-
PANIC at Digit.ofChar lean.run.foo:65:4: not a digit
'0'
-/

[Kyle Miller]

Or you can use CoeDep for specific characters:

instance : CoeDep Char '0' Digit where
  coe := Digit.ofChar '0'
instance : CoeDep Char '1' Digit where
  coe := Digit.ofChar '1'
-- ...
instance : CoeDep Char '5' Digit where
  coe := Digit.ofChar '5'
-- ...

def myDigit : Digit := '5'

#eval myDigit
-- '5'

[nrs]

Kyle Miller said:

Or you can use CoeDep for specific characters:

instance : CoeDep Char '0' Digit where
  coe := Digit.ofChar '0'
instance : CoeDep Char '1' Digit where
  coe := Digit.ofChar '1'
-- ...
instance : CoeDep Char '5' Digit where
  coe := Digit.ofChar '5'
-- ...

def myDigit : Digit := '5'

#eval myDigit
-- '5'

oh this is a neat solution! maybe there is a way to make a recursive definition here that will work?

[Kyle Miller]

No this is very limited, it looks for (more-or-less) the specific syntax. The '5' here must be a literal.

[Kyle Miller]

Here's the 'metaprogramming' approach.

def Digit := { c : Char // c.isDigit }

notation "toDigit " c => (Subtype.mk c rfl : Digit)

def myDigit : Digit := toDigit '5'

#eval myDigit
-- '5'

[Kyle Miller]

This only works if rfl is a proof of c.isDigit = true (recall: c.isDigit is a Bool, so when it appears where a Prop is expected it is coerced to c.isDigit = true)

[nrs]

Kyle Miller said:

This only works if rfl is a proof of c.isDigit = true (recall: c.isDigit is a Bool, so when it appears where a Prop is expected it is coerced to c.isDigit = true)

I see, thank you very much for the examples, these are very useful!