Help: Convert an implicit instance with 'A => Nothing' to a given instance

Question
1

Hi,

Could you please help me convert the following program into the given syntax of Scala 3.6, that is, the new given syntax?

  trait A
  implicit def `A and ¬A is a contradiction`(implicit a: A, notA: A => Nothing): Nothing = notA(a)
  implicit val notA: A => Nothing = { _ => throw new Exception("Contradiction") }
2

Reference:

I think

  • implicit class turns into extension,
  • implicit val/def turns into a given, and
  • implicit parameter turns into using.

The implicit def with the implicit parameter can be written in two ways, providing the using yourself, or using the “conditional given” syntax (which desugars to the same thing):

1 Like
3

@spamegg1

It works. That’s what I was asking.

The documentation you linked is very helpful. It makes things clear.

Thank you very much!

1 Like
4

This is not immediately related to the question, but a word of caution:
You should always wrap the type for these kinds of manipulations, for example Proof[A] Proof[A => Nothing]

Example:

Otherwise you might get surprised by the ability of the compiler to deduce things it might not be able to:


given literrallyAnyProofYouWant

// Try to find a proof of `A => A`
summon[A => A] // This will always succeeds

That is because for any type T, T =:= T is given (The proof that T is both a subtype and a supertype of T), but A =:= B is a subtype of A <:< B which is a subtype of A => B !
(and a given subtype succeed for a using of its supertype)

And if you involve other libraries, you might get even more surprises !

2 Likes