Proving that a match type resolves to a specific concrete type

Question

I am trying to create an implementation of a trait that uses a match type, where the right-hand-side of that match type is known in advance. However, I can't seem to get the compiler to accept my "proof" of this. This is pretty new to me, so sorry if this is really obvious. Can someone help me understand if/how I can achieve what I want?

Here's some minimal code (Scastie) to illustrate what I'm doing:

class NumberBox {} class LongBox {} trait Boxer[T] { def box(): Boxer.Box[T] } object Boxer { type Box[T] = T match case Long => LongBox case _ => NumberBox } case class Val[T](v: T) extends Boxer[T] { def box(): Boxer.Box[T] = v match case _: Long => new LongBox() case _ => new NumberBox() } // here we prove that Boxer.Box[T] is a NumberBox case class NoLongs[T](v: Boxer[T])(using Boxer.Box[T] =:= NumberBox) extends Boxer[T] { override def box(): Boxer.Box[T] = new NumberBox() } NoLongs(Val(1))

But this fails with:

Found: NumberBox Required: Boxer.Box[T] Note: a match type could not be fully reduced: trying to reduce Boxer.Box[T] failed since selector T does not match case Long => LongBox and cannot be shown to be disjoint from it either. Therefore, reduction cannot advance to the remaining case case _ => NumberBox override def box(): Boxer.Box[T] = new NumberBox()

Silvio Mayolo · Accepted Answer · 2023-04-15 03:19:51Z

Scala doesn't automatically apply proofs in the way you're looking for. But you're right that you do have a proof. In fact, your proof constitutes a callable object: the type =:=[From, To] defines a method called apply:

override def apply(f: From): To

Now, you have a value of type Boxer.Box[T] =:= NumberBox, which means that apply would convert a Boxer.Box[T] to a NumberBox. You want the opposite: to convert a NumberBox into a Boxer.Box[T]. So we need to flip your proof around and then apply it.

def flip: To =:= From

In your specific use case, consider

case class NoLongs[T](v: Boxer[T])(using eq: Boxer.Box[T] =:= NumberBox) extends Boxer[T] { override def box(): Boxer.Box[T] = eq.flip(new NumberBox()) }

We give the proof argument a name, eq, and then we apply its symmetric proof (that NumberBox =:= Boxer.Box[T]) to our NumberBox to convert it to the desired type.

You could also just take a proof that NumberBox =:= Boxer.Box[T] directly and get rid of the flip, if desired.

case class NoLongs[T](v: Boxer[T])(using eq: NumberBox =:= Boxer.Box[T]) extends Boxer[T] { override def box(): Boxer.Box[T] = eq(new NumberBox()) }

This was so helpful, thank you. I had no idea that =:= was callable like that 🤯

Dmytro Mitin · Accepted Answer · 2023-04-16 17:08:51Z

I'll just add to @SilvioMayolo's answer that

type class =:= is not symmetric (i.e. if there is implicit A =:= B then generally there is no implicit B =:= A generated by compiler automatically)

Why this scala code has a compilation error type mismatch

T <: A, return T method

https://typelevel.org/blog/2014/07/02/type_equality_to_leibniz.html

https://typelevel.org/blog/2014/09/20/higher_leibniz.html

In scala 3, is it possible to make covariant/contravariant type constructor to honour coercive subtyping?

you don't have to call eq explicitly

case class NoLongs[T](v: Boxer[T])(using NumberBox =:= Boxer.Box[T]) extends Boxer[T] { override def box(): Boxer.Box[T] = new NumberBox() }

case class NoLongs[T](v: Boxer[T])(using eq: Boxer.Box[T] =:= NumberBox) extends Boxer[T] { given (NumberBox =:= Boxer.Box[T]) = eq.flip override def box(): Boxer.Box[T] = new NumberBox() }

you can have constraints in both directions

case class NoLongs[T](v: Boxer[T])(using Boxer.Box[T] =:= NumberBox, NumberBox =:= Boxer.Box[T]) extends Boxer[T] { override def box(): Boxer.Box[T] = new NumberBox() }

I'm not sure I understand your first bullet point (isn't flip quite literally a proof of the symmetric property, namely that A =:= B implies the existence of B =:= A?). But that is really interesting to know that Scala will use =:= constraints automatically if the given is in the right order. Is that a new feature in Scala 3 or did I just never notice it before?
@SilvioMayolo "isn't flip quite literally a proof of the symmetric property" It is but it's not an implicit. If there is implicit A =:= B then generally there is no implicit B =:= A generated by compiler automatically. "Is that a new feature in Scala 3" It exists in 2.x too. A =:= B extends A => B, so it defines an implicit conversion.

Collectives™ on Stack Overflow

Proving that a match type resolves to a specific concrete type

2 Answers 2

1 Comment

2 Comments

Linked

Hot Network Questions

Collectives™ on Stack Overflow

2 Answers 2

1 Comment

2 Comments

Linked

Related