Syntax sugar for automatically coercing into subtypes?

Stream: general

[Lhr]

Currently the refinement subtypes in Lean have worse ergonomics when compared to a language like F*, because you must explicitly provide trivial proofs like rfl, cluttering the callsite such that I honestly hardly ever want to use the feature in general programs.

def f (x : {n : Int // n % 2 = 0}) := x

#eval f ⟨2, rfl⟩

If F*, it looks like

let f(x : int{x % 2 = 0}) = x

let y = f 2

seamless, because the proof is handled for you automatically.

is there any way currently in Lean, through its macros or notation system or implicit arguments, to make f 2 translate into f ⟨2, rfl⟩without requiring manual callsite clutter?

[Aaron Liu]

you could write an OfNat instance

[Lhr]

Aaron Liu said:

you could write an OfNat instance

What would that look like?

[Aaron Liu]

actually I don't know

[Aaron Liu]

since you should be able to have 2 but not 3

[Aaron Liu]

so it's a bit weird

[Kim Morrison]

We can't do this at the moment.

What we can do is:

structure EvenInt where
  n : Int
  even : n % 2 = 0 := by grind

def f (x : EvenInt) := x

#eval f { n := 2 } -- no proof required!

#eval f ⟨2⟩ -- but this still doesn't work, nor `f 2`.

It would not be crazy to make f ⟨2⟩ work, and this is been requested before. Making f 2 work is harder.

Notice here I had to make my own subtype in order to provide the auto_param (:= by grind).

[Lhr]

Thanks. what sort of thing would be required to make f 2 work, with no prior ceremony or manual labor like defining a structure and your example, but just using the native subtype notation like my example

def f (x : {n : Int // n % 2 = 0}) := x

are you saying it would need to be a sophisticated change in the compiler? what sort of change would need to happen in the compiler?

I'm interested in reading through the compiler and experimenting.

[Kim Morrison]

It's the elaborator, rather than the compiler. Are you imagining this is restricted to subtypes? Or any structure with a single data field? Which tactic do you want to use.

[Lhr]

Kim Morrison said:

It's the elaborator, rather than the compiler. Are you imagining this is restricted to subtypes? Or any structure with a single data field? Which tactic do you want to use.

Yes, getting this to work for subtypes is what I only care about for now, coming from F* where subtypes feel awesome and boilerplate-free.

In this case, I would want the expression to just translate into ⟨2, rfl⟩behind the scenes. Will this not work for other subtypes? Also, I see that there is an smt solver lib for lean. Possibly, that could be used, but I am hoping that most subtype proofs are as simple as rfl

[Edward van de Meent]

if this is such an issue, you might want to try this pattern for your functions:

def f (x : Int) (hx : x % 2 = 0 := by grind) : Int := x

#eval f 2

It's not quite the same as what you wrote (the return type is different), but usually that's just better anyway, as you are able to decide afterward what facts you want to show about the returned value of your function.

[Jakub Nowak]

But it's not always possible to use unbundled version. For the good UX, we should either get rid of subtypes completely, or ensure seamless feature parity between subtypes and unbundled version.

[Robin Arnez]

It is also possible to write an OfNat with some instance magic:

structure EvenInt where
  n : Int
  even : n % 2 = 0

class IsTrue (b : Bool) where
  out : b = true

instance : IsTrue (no_index true) := ⟨rfl⟩

instance [even : IsTrue ((n.mod 2).beq 0)] : OfNat EvenInt n :=
  ⟨n, by norm_cast; simpa using even.out⟩

def f (x : EvenInt) := x

#eval f 2 -- works
#eval f 3 -- fails

[Lhr]

Edward van de Meent said:

if this is such an issue, you might want to try this pattern for your functions:

def f (x : Int) (hx : x % 2 = 0 := by grind) : Int := x

#eval f 2

It's not quite the same as what you wrote (the return type is different), but usually that's just better anyway, as you are able to decide afterward what facts you want to show about the returned value of your function.

I'm aware of this approach, but it still seems worse than what a proper subtype system could do. The type of x is not truly refined there, so you may have to reprove this extrinsic statement elsewhere as you compose f with other functions. Consider our case here where f is the identity function

def f (x : Int) (hx : x % 2 = 0 := by grind) := x
#eval f (f 2) -- error

could not synthesize default value for parameter 'hx' using tactics
`grind` failed
case grind
h : ¬f 2 ⋯ % 2 = 0
⊢ False
(trace)

[Aaron Liu]

there will always be times it can't automatically prove the subtype condition

[Aaron Liu]

what kind of "proper subtype system" are you imagining

[Jakub Nowak]

Aaron Liu said:

there will always be times it can't automatically prove the subtype condition

Maybe we could have a syntax like with arrays: el'?_ or el!.

[Jakub Nowak]

Or just normal \<el, ?_\> but only required when the condition can't be proved.

[Aaron Liu]

and there's also stuff like

[Aaron Liu]

what if you have a subtype of a subtype

[Aaron Liu]

so it might become ambiguous?

[Jakub Nowak]

If both target and source types are known that I don't think there's ambiguity? But I could imagine cases where one or the other might be not known without additional type annotations. I guess that's similar kind of problem as with coercions from subtype to underlying type?

[Aaron Liu]

yeah so now if you have coercions in both directions it becomes a problem

[Aaron Liu]

that's why we got rid of the coercion from Nat to Fin

[Violeta Hernández]

I'm not sure if it's worthwhile putting any substantial effort into saving a total of six keystrokes.

[Jakub Nowak]

Violeta Hernández said:

I'm not sure if it's worthwhile putting any substantial effort into saving a total of six keystrokes.

There's no mechanism to specify automatic dischargers for subtypes atm. And the solution here is way more than six keystrokes.

[Lhr]

Violeta Hernández said:

I'm not sure if it's worthwhile putting any substantial effort into saving a total of six keystrokes.

It is worthwhile if you want the language to be adopted for practical general purpose programming, rather than only for mathematicians writing proofs. In normal business applications, refinements like these are only slightly beneficial, which means that any amount of friction will be enough to make most programmers decide that they are not worth doing in general. Consider:

class User(val age : Int)

This is standard in industry, C++ and Java programmers write this all the time. Everyone knows the code would be slightly more sensical and less bug prone if we could express that a user's age cannot be negative, but it really isn't a big deal -- it's unlikely someone would ever actually pass a negative anyway. Mainstream languages have existed for decades without this feature just fine. And if a programmer did care enough, they could always compensate for the inexpressive type system by putting runtime checks will throw errors:

class User(val age : Int) {
    assert(age >= 0)
}

Now consider the fact that despite this being available to industry programmers as an objective improvement to their code, almost no one ever bothers to do it. It's just too much effort to justify as a general practice. "Do we really need to enforce that factorial(n) accepts only natural numbers, especially if that is going to make invoking the function a slight pain everywhere else forever? Can't we just expect that this will be obvious to other programmers?"

Application developers are only willing to sprinkle refinements like this throughout their code if it is dead simple -- nearly as easy as without them. That means: no prior ceremony like @Robin Arnez's example, and no cluttering callsites with awkward tuples or explicit casts. I want to call factorial on a natural number, not on a natural number paired with a proof that it is natural.

The language I used for the code snippets is Scala, and in Scala there is actually a compile time refinement library called Iron which lets you seamlessly express this

class User(val age : Int :| GreaterEqual[0])

And can even be made easier with alias if desired

class User(val age : Int :| >=[0])

And callsites are unchanged

val a = User(42)
val b = User(-42) // fails to compile

That's to say that, it would be sad if a much less sophisticated language like Scala is able to offer a more pleasant refinement type experience than a premium dependently typed language like Lean4. Surely we can make this more ergonomic for the common simple cases.

[Aaron Liu]

so how is this lacking?

Edward van de Meent said:

if this is such an issue, you might want to try this pattern for your functions:

def f (x : Int) (hx : x % 2 = 0 := by grind) : Int := x

#eval f 2

It's not quite the same as what you wrote (the return type is different), but usually that's just better anyway, as you are able to decide afterward what facts you want to show about the returned value of your function.

[Lhr]

Well I showed an example of how the type not truly being refined causes certain usages that you would expect to work, not work

#eval f (f 2) -- error

there may be more I haven't found where it breaks. I know that if you try using rfl or simp instead of grind, composition with another function breaks:

def f (x : Int) (hx : x % 2 = 0 := by rfl) := x
def g (x : Int) (hx : x % 2 = 0 := by rfl) := f x -- could not synthesize default value for parameter 'hx' using tactics

whereas both work using subtypes

def f (x : { x : Int // x % 2 = 0 }) := x
def g (x : { x : Int // x % 2 = 0 }) := f x

#eval f (f ⟨2, rfl⟩)

[Aaron Liu]

how are we possibly supposed to know the output of f 2 satisfies the constraint

[Lhr]

Aaron Liu said:

how are we possibly supposed to know the output of f 2 satisfies the constraint

Because f is an identity function. It returns it's input unchanged, and we have established that it's input has this constraint, so we should - we hope we could - be able to conclude that it's output has the same constraint.. That's the advantage of subtypes I'm seeing.

[Aaron Liu]

ah, but how are we supposed to know f is an identity function

[Aaron Liu]

tactics usually don't peek inside defs

[Aaron Liu]

if you want to expose that f is an identity function you can make it an abbrev f or you can write a lemma that says f is an identity function and you can mark it @[simp] or @[grind =] or something

[Aaron Liu]

don't we do something similar for GetElem where the proof of correctness is done automatically using an extensible tactic and you can still supply a proof manually if you want to

[Aaron Liu]

I don't really know what kind of constraints you would want to express anyways

[Aaron Liu]

since I don't really use subtypes

[Yan Yablonovskiy 🇺🇦]

Lhr said:

That's to say that, it would be sad if a much less sophisticated language like Scala is able to offer a more pleasant refinement type experience than a premium dependently typed language like Lean4. Surely we can make this more ergonomic for the common simple cases.

I would think this is actually to be expected when comparing the two, more expressivity leaves room for more ambiguity surely. In your example, assert(age >= 0) doesn't work in a Lean friendly way. In Scala, Int is a 32-bit signed integer value type, so this would be an example of type punning.

[Kim Morrison]

@[grind]
def f (x : Int) (_hx : x % 2 = 0 := by grind) : Int := x

#eval f 2

#eval f (f 2)

works fine.

[Lhr]

Yan Yablonovskiy 🇺🇦 said:

Lhr said:

That's to say that, it would be sad if a much less sophisticated language like Scala is able to offer a more pleasant refinement type experience than a premium dependently typed language like Lean4. Surely we can make this more ergonomic for the common simple cases.

I would think this is actually to be expected when comparing the two, more expressivity leaves room for more ambiguity surely. In your example, assert(age >= 0) doesn't work in a Lean friendly way. In Scala, Int is a 32-bit signed integer value type, so this would be an example of type punning.

assert(age >= 0) was meant as an example where expressing a constraint is upleasant, such that few programmers ever do it even in languages like Java.

Anyway yes, it is true that sometimes we trade having simple cases be seamless to that we can unlock more advanced cases. But we often can still post-fact introduce syntax sugar for making the simple cases easy again. Option a is more powerful than null | a, but we also provide an implicit conversion from a -> Some a where Option a is required to get the best of both worlds.

I would look to F* as an example of a language that is far far more expressive than Scala while still having just as easy and often easier syntax. Yes this is largely because of their SMT solver, but even without one I assume there are ways we could improve the handling of subtypes in Lean.