https://kotlinlang.org logo
#arrow-contributors
Title
# arrow-contributors
r

raulraja

12/08/2019, 12:34 PM
Copy code
@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
3 Views