You are just specifying implicit conversions. They...

# functionalt

tschuchort

11/20/2019, 12:07 PMYou 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`

hast

tschuchort

11/20/2019, 12:09 PMThey are still implicit conversions aren't they?

tschuchort

11/20/2019, 12:09 PMWhat happens when you have two different proofs of the same proposition/type?

i

Imran/Malic

11/20/2019, 12:13 PMwell that sounds like when you proof an isomorphism in 2 ways.

Imran/Malic

11/20/2019, 12:14 PMAt 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 PMI 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

11/20/2019, 12:22 PMOr 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 PMtwo type proofs consist of 4 functions. In your example your

`from`

and `to`

are properties. you would do something like:
Copy code

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

j

Jannis

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

i

Imran/Malic

11/20/2019, 12:30 PMI 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 PMWell 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 PMImplicit conversions is just a type of proof when you use Subtyping

raulraja

11/20/2019, 12:39 PMThere are others like extensions that don't need to implicitly convert but they expose intersections of the type classes and the types

raulraja

11/20/2019, 12:39 PMThey all follow the same coherence mechanism as typeclasses are proposed in KEEP-87

raulraja

11/20/2019, 12:44 PMYou 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

11/20/2019, 12:46 PMType 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

11/20/2019, 12:48 PMType 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

11/20/2019, 12:49 PMThis 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

11/20/2019, 12:50 PMNo need for imports and resolution remains coherent based on the order proposed in KEEP-87

10 Views