tschuchort
11/18/2019, 3:56 PMbigkahuna
11/18/2019, 3:59 PMImran/Malic
11/18/2019, 4:15 PMbigkahuna
11/18/2019, 4:16 PMImran/Malic
11/18/2019, 4:20 PMtschuchort
11/18/2019, 4:24 PMImran/Malic
11/18/2019, 4:25 PMArrow-Meta
we will have those descriptors at Compile-time with an Additional Type Checker, which jumps in for conversions like.
val list: List<Int> = listOf(4)
val l: ListOf<Int> = list
In the past you would get an TypeError. @raulraja made further improvements on this API with type-proofs
.type-proof
https://kotlinlang.slack.com/archives/CJ699L62W/p1574067540396900tschuchort
11/18/2019, 4:25 PMImran/Malic
11/18/2019, 4:43 PMShapeless in Scala
). But one standard example is this https://stackoverflow.com/questions/2693067/what-is-meant-by-scalas-path-dependent-types.
Let’s say your trying to define a Type with a Tree Hierarchy and you don’t want to mix the wrong parent & child. Then Path dependent Types
come in handy.
They allow you to use the Type System to your advantage and express in one way, they are sure others, hierarchical relationships between types.PhBastiani
11/18/2019, 4:49 PMraulraja
11/18/2019, 5:35 PMclass `List(_)`
@arrow.proof(conversion = true)
fun <A> Kind<`List(_)`, A>.fix(): List<A> =
(this as Kinded).value as List<A>
@arrow.proof(conversion = true)
fun <A> List<A>.unfix(): Kind<`List(_)`, A> =
Kinded(this)
List
into a kinded value you can use in ad hoc polymorphismKinded
is an erased inline class that wraps the concrete valueconversion = true
eliminates the need to ever call fix
as it looks today when using polymorphic functions because the type proof plugin is able to tell the Kotlin compiler type checker those are kinds given those proofs that are provided by the user.Imran/Malic
11/18/2019, 5:44 PMtype-proofs
provide API’s over Types ? Somehow, the first steps for Kotlin to go type-level
raulraja
11/18/2019, 5:45 PMImran/Malic
11/18/2019, 5:47 PMHexa
11/20/2019, 7:46 AMUberto Barbini
11/20/2019, 9:55 AMraulraja
11/20/2019, 10:13 AMImran/Malic
11/20/2019, 10:36 AMSubtyping
can be in FP at an architectural level.
But I might be looking in the wrong direction.raulraja
11/20/2019, 10:48 AMjimn
11/20/2019, 11:33 AMConversions
take you with a function from A to B without the need to cast ? e.g. let{}. map{} ?Imran/Malic
11/20/2019, 12:04 PMlet and map
not really @jimn.
map implies that your Container F
stays the same, what @raulraja introduces is a way to go from one Category to another if I got that right.type-proof
has 2 components a to
and a from
function. Where we go from A
to B
and back. Thus we proof to the compiler, that this conversion is valid. Similar if you would describe an isomorphism between Functor’s F
and G
raulraja
11/20/2019, 1:22 PMSubtyping
type proof takes you from a type to another without the need to cast if you know the path and declare it as a proof.Imran/Malic
11/20/2019, 2:02 PMraulraja
11/20/2019, 2:19 PMjimn
11/20/2019, 3:49 PM