You are just specifying implicit conversions They are proofs

Question

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 · Answer

`type proofs` are global not like the one `Scala` has

tschuchort · Answer

They are still implicit conversions aren t they

tschuchort · Answer

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

Imran/Malic · Answer

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

Imran/Malic · Answer

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 · Answer

I can have two proofs of `Int gt 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 · Answer

Or I can do `fun lt A B gt unsound from A B = Nothing` that is a proof of every proposition

Imran/Malic · Answer

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 · Answer

or simple unsafe typecasts from A to B see no evil

Imran/Malic · Answer

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 · Answer

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 · Answer

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

raulraja · Answer

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

raulraja · Answer

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

raulraja · Answer

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

raulraja · Answer

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 · Answer

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 · Answer

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 · Answer

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 · Answer

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