``` Proof Subtyping inline fun lt A gt A first Union4 lt A Any Any Any gt ```

``` Proof Subtyping inline fun lt A gt A first Union4 lt A A kotlinlang #arrow-contributors

Channels

lincheck

kobweb

kotlin-multiplatform-contest

osgi

brikk

revolver

tricity-kotlin-user-group

cincinnati-user-group

prozis-android-backup

refactoring-to-kotlin

russian-kotlinasfirst

androidgithubprojects

navigation-architecture-component

stayhungrystayfoolish

practical-functional-programming

tensorflow

swagger-gradle-codegen

kotlinultimatechallenge

competitive-programming

skia-wasm-interop-temp

java-to-kotlin-refactoring

event21-community-content

myndocs-oauth2-server

jvm-ir-backend-feedback

Title

raulraja

12/08/2019, 12:34 PM

@Proof(Subtyping)
inline fun <A> A.first(): Union4<A, Any?, Any?, Any?>

pakoito

12/08/2019, 12:35 PM

why any and not Nothing?

raulraja

12/08/2019, 12:44 PM

I have inverted the runtime as encoded in Arrow to make it leaners so there is a single interface and single inline class. Nothing in a proof position is assignable to unions that would have included types not in the unions based on this encoding

👍🏼 1

https://github.com/arrow-kt/arrow-meta/blob/829176e97454c6653b1b1332675837f5513225cc/prelude/src/main/kotlin/arrow/unions.kt#L13

proofs need to be applicable by their upperbound since they are polymorphic

Proofs are a way to encode the Curry - Howard correspondence as a meta library for Kotlin

since you can draw morphisms in the category of the Kotlin Types where the types are the objects

and in a directed graph you can walk the graph with Dijstra shortest path or similar to find inductive proofs like the ones for tuples and hlist

Inductive proofs will bring automatic derivation for data classes and sealed classes, unions, etc.

3 Views

#arrow-contributors Join Slack