https://kotlinlang.org logo
Title
t

tschuchort

11/20/2019, 12:07 PM
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.
i

Imran/Malic

11/20/2019, 12:08 PM
type-proofs
are global not like the one
Scala
has
t

tschuchort

11/20/2019, 12:09 PM
They are still implicit conversions aren't they?
What happens when you have two different proofs of the same proposition/type?
i

Imran/Malic

11/20/2019, 12:13 PM
well that sounds like when you proof an isomorphism in 2 ways.
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.
t

tschuchort

11/20/2019, 12:20 PM
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.
Or I can do
fun <A,B> unsound(from: A): B = Nothing
that is a proof of every proposition.
i

Imran/Malic

11/20/2019, 12:26 PM
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 = ...
j

Jannis

11/20/2019, 12:26 PM
or simple unsafe typecasts from A to B 🙈
i

Imran/Malic

11/20/2019, 12:30 PM
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
j

Jannis

11/20/2019, 12:31 PM
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
r

raulraja

11/20/2019, 12:38 PM
Implicit conversions is just a type of proof when you use Subtyping
There are others like extensions that don't need to implicitly convert but they expose intersections of the type classes and the types
They all follow the same coherence mechanism as typeclasses are proposed in KEEP-87
You can do unsound propositions as this is an open door to replace Subtyping by composition with access to all types in the type system from Any? To Nothing. It's not ment to be used to model applications but type system features such as those proposed in the arrow prelude.
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
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
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
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
No need for imports and resolution remains coherent based on the order proposed in KEEP-87