SKB – Scala implicit proof


This article is part of the Scala knowledge bits Series.

Periodically, I will publish new exercises so you can slowly build up knowledge about Scala.

It is designed to be done in a very short amount of time and learn a little bit each day, just to create a routine.

This episode will teach you about Scala implicit proof.

Hope you are going to enjoy it! It is designed for anyone to learn Scala from scratch and slowly learn, one Bit at a time.

After this Bit, I would love to hear your feedback in the comments down below.

Feel free to join the Discord server as well if you would like some help and support from the rest of our community.

What are we learning today?

Today we are going to learn about Scala implicit proof !

Today diving deeper into making a friend out of the compiler.

We are going to learn on how to guarantee that a generic type follow specific rules. We are going to use implicit proof.

Time to try on the exercise on your own and scroll down for more information when you are done or if you are stuck.


Here is an exercise to complete today.

If I did my job well, you should be able to guess by yourself the solution based on what you previously learned and based on the clues.

But if you get stuck, scroll down to get more information.

The goal of the exercise is to replace the ??? by a piece of code so that the exercise compiles and that’s how you win! Good luck!

You can fill the exercise right in here:

Or, if it does not load, go on to Scastie (rPQxPMehSye8cwfa4VU9zg).

More information about Scala implicit proof

In this exercise you will learn (or have learned, if you have already solved the puzzle) about Scala implicit proof.

Hopefully this was not too hard. If you have any questions, please come ask them on the Discord server.

The first way to prove that a generic type A is of type T, we can do the following:

def name[A: T](arguments...): RETURN_TYPE = ???

This syntax will block compilation if we use the method with a type that cannot be proven to be of type T or made of type T with conversions.

You will often see this being used with A : TypeTag: ClassTag but we are going to look into those Scala standard types an other time in a dedicated episode.

In our example, you can see that we define our proofs in ValidFoos using the syntax:

implicit val name: PROOF_TYPE[TYPE_NEEDING_PROOF] = ???

Our example is of course a bit silly but there are production use cases that would need those structures. For instance if you have complex data types that share underlying trait. But we are going to see more advance use case right now, when we actually use the proof.

In the second example, not only we are requiring a proof, but we are not using the [A: T] syntax, we are using the syntax that expose the proof so we can use it:

def name[A](arguments...)(implicit proof_name: PROOF_TYPE[A]): RETURN_TYPE = ???

Written this way, we can actually use the proof and do things with it.

In this case, we want the proof that the input is some kind of number, we do not want to write one function for Int, one for Double, one for Long, etc… That would be very tedious. So we need a way to target all numbers. In Scala, we can prove that a TYPE is a number when there a Numeric[A] proof.

Once we acquire the proof, we can use num to perform operations. For instance, we simply perform a sum here.

Feel free to go back to the exercise, modify the code to try out new things and get a better intuition for Scala implicit proof.


I hope you have learned something new or had fun during this Scala Knowledge Bit.

Please ask questions or post feedback in the comments below.

Feel free to try on the next Scala Knowledege Bit.

If you are curious about the previous Scala knowledge Bits, go check it out! 🙂

Leave a Reply