Givens in Scala 3 as proofs of existence of types
Note
From the point of view of Type level programming, a given
proves the existence of a type - e.g. the compiler can prove the existence of types, and then create new given instances using
those types. This can be used for computations at compile time. (e.g. for a type level sum for example)
A given
is conceptually constructing an instance of a type with a concrete behaviour where a using
claused is used.