Type Proofs brings first-class idiomatic syntax for functional programming to Kotlin and replace the need for Dependency Injection containers resolving the injection of components and verifying applications dependency graphs at compile time.

Type Proofs is a new compiler plugin built on Arrow Meta enabling new features in the Kotlin type system, such as Type Classes, Union Types, Type Refinements, and many other extensions.

Type Proofs propositions are expressed as extension functions that unlock new relationships between types ad-hoc whilst remaining fully compatible with sub-type polymorphism and the existing inheritance type system.

At the root of this design is the Curry-Howard-Lambek Correspondence where we can establish a relationship between two types that act as a proposition, and a function that acts as morphism or proof of the relationship.

This talk demonstrates Algebraic Domain Modelling with these advanced type system features and how applications and libraries can benefit when using Type Proofs in their design.

Join us and learn about all these new type-system features that the Arrow & 47 Degrees team is proposing as KEEPs in 2020.