https://kotlinlang.org logo
Title
r

raulraja

12/08/2019, 12:34 PM
@Proof(Subtyping)
inline fun <A> A.first(): Union4<A, Any?, Any?, Any?>
p

pakoito

12/08/2019, 12:35 PM
why any and not Nothing?
r

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
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.