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.

Links

Given and Using Clauses in Scala 3