You are just specifying implicit conversions. They...

# functional

[tschuchort]

You are just specifying implicit conversions. They are proofs in the sense that any function is a proof by the curry-howard isomorphism, but such proofs aren't worth much in a language with bottom values since they are a proof of any type.

[Imran/Malic]

type-proofs are global not like the one Scala has

[tschuchort]

They are still implicit conversions aren't they?

[tschuchort]

What happens when you have two different proofs of the same proposition/type?

[Imran/Malic]

well that sounds like when you proof an isomorphism in 2 ways.

[Imran/Malic]

At that point it should matter to the compiler. As a user you have to take care that both of them are valid in your domain.

[tschuchort]

I can have two proofs of `Int -> Long`:

fun p1(from: Int): Long = (from as Long)
and
fun p2(from: Int): Long = (-from as Long)

They are both proofs of the same proposition but at the end of the day the conversion is different.

[tschuchort]

Or I can do fun <A,B> unsound(from: A): B = Nothing that is a proof of every proposition.

[Imran/Malic]

two type proofs consist of 4 functions. In your example your from and to are properties. you would do something like:

fun Int.from1(): Long = ...
fun Long.to1(): Int = ...
fun Int.from2(): Long = ...
fun Long.to2(): Long = ...

[Jannis]

or simple unsafe typecasts from A to B 🙈

[Imran/Malic]

I agree that both of these proofs have to be validated either with property-based testing or other means @tschuchort if that is what you were pointing out

[Jannis]

Well actually I think it's fine as is, leave it to users to validate conversions, however it's misleading to call them proofs, which I think is what @tschuchort was trying to pointing out

[raulraja]

Implicit conversions is just a type of proof when you use Subtyping

[raulraja]

There are others like extensions that don't need to implicitly convert but they expose intersections of the type classes and the types

[raulraja]

They all follow the same coherence mechanism as typeclasses are proposed in KEEP-87

[raulraja]

You can also proof impossible paths to disallow path of calls between types and express architectural boundaries. For example disallowing persistence objects calls from view objects and return diagnostics from the proof to enhance compiler errors and checks across the codebase

[raulraja]

Type proofs is an open door to the type checker and impossible type casts that otherwise would have failed to codegen where the proof is inserted in place or used for static analysis of the type system for any of the strategies of ProofType

[raulraja]

Type classes can also be expressed as type proofs since the Kotlin compiler supports intersection types and a value with syntax is the intersection of the receiver and the type class proof extension without altering the Lang one bit syntactically and activating Polymorphism with type param constrains or where clauses which is already in Kotlin

[raulraja]

This is because the proof can alter Subtyping and make the type class instance ad hoc part of the hierarchy of any value for which there is an extension

[raulraja]

No need for imports and resolution remains coherent based on the order proposed in KEEP-87