https://kotlinlang.org logo
Join Slack
Powered by
Do you think that with the advent of arrow-meta Ko...
# functional
t
Do you think that with the advent of arrow-meta Kotlin will become as good at functional programming as Scala? Or is there still something missing that Scala has but we don't? I'm trying to learn Scala and it's only now that I can fully appreciate the syntactic simplicity of Kotlin 😄
b
Kotlin doesn’t have higher-kinded types like Scila but not really missed IMO. I’ve only used Scala 2.x but isn’t Dotty supposed to simplify everthing i.e. language constructs etc.
i
HKT exist in Kotlin. @tschuchort we’re all working on making that happen for Kotlin. One among other things, which is missing in Kotlin is Path dependent types, which Scala has, if you want one comparison.
b
I stand corrected. I just looked at Arrow’s API. I haven’t looked at Arrow for a while. My bad. I was referring to Kotlin itself but didn’t know Arrow enables HKTs
i
No worries @bigkahuna 🙂
t
What's path-dependent types? Is that like dependent types in Martin-Löf type theory? Even Haskell doesn't have those.
i
the JVM already has the notion of HKT in it’s internals, what we have in Arrow right now is just a workaround. With 
Arrow-Meta
we will have those descriptors at Compile-time with an Additional Type Checker, which jumps in for conversions like.
Copy code
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
.
@bigkahuna here is an example of a 
type-proof
https://kotlinlang.slack.com/archives/CJ699L62W/p1574067540396900
t
The last time I looked at arrow the HKTs were super awkward to use. Hopefully that will be remedied with arrow-meta but afaik you are still limited by the original parser with the current implementation using kastree
i
I cant comment on the whole spectrum of path dependent types, because they can be used in a variety of levels (they can get pretty complex, if you add GADT’s and Haskells Generics to it or 
Shapeless 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.
I really enjoyed this video if you want to hear more

https://www.youtube.com/watch?v=I1RAij4aX6Y▾

, but they’re plenty out there. I cant confidently answer what the difference is between Path dependent types in Scala and Dependent Types in Haskell. At first glance they seem to solve the same problem, but I am not a Haskell programmer, nor Scala.
👍 1
p
From my point of view, HKTs in Arrow are not easy to use; but, we cannot say "super awkward to use" ! The main difference with Scala concerns the management of implicit parameters/classes. And, the use of the FX part.
r
Kinds are gonna be easy to use with type proofs
👌 1
➕ 1
The only needed or autogenerated boilerplate is:
Copy code
class `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)
And there is no need to create wrappers
that turns 
List
into a kinded value you can use in ad hoc polymorphism
Kinded
is an erased inline class that wraps the concrete value
also the 
conversion = 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.
We have unions, kinds, refined types and in the work to implement also type classes all with just type proofs
i
@raulraja Can we say that 
type-proofs
provide API’s over Types ? Somehow, the first steps for Kotlin to go 
type-level
r
type proofs are contract with the compiler where you describes the rules between types. they will be discoverable with the same resolution as proposed for type classes
🔝 1
It’s a proof at the type level because it’s inspected at compile time but it’s not type level programming in the sense of a type level HList, Nat etc as you seen in Scala and Haskell, but you can use them for similar purposes
i
I also love the formal answer 👌🏽
h
I would love it if Kotlin becomes more powerful than Scala
u
Even without arrow-meta (that I'm looking forward to) Kotlin can go 90% as far as scala with a tenth of the hassle. On top the Nullable types can be used as lightweight Maybe while in Scala you still have to protect yourself against nullability. As for me Kotlin is the best choice right now for functional programming on the Jvm.
FP is about trying to stay as close as possible to Lambda.Calculus and Category theory. It can be done even without HKT (not saying they would not be useful).
r
Agreed
i
Hi @raulraja 🙂 Do you have a good read on Subtyping and it’s relation to FP architecture. I am digging through some papers about Foundational Theories about Programming Languages, but I dont get to the point where I can see how expressive 
Subtyping
can be in FP at an architectural level. But I might be looking in the wrong direction.
r
It's simpler. Kotlin is inheritance based on subtype Polymorphism and it's type checker only checks for equality and subtype relationships. You can stablish those relationships synthetically without using supertypes declarations. Then with codegen insert conversions where a class cast would occur otherwise Conversions take you with a function from A to B without the need to cast If the runtime is inlined then it's a zero cost abstraction for adhoc Polymorphism, that is the kind of Polymorphism where you don't need to inherit a supertype.
So this is an alternative to inheritance which favors composition and separation of data and behaviors
j
Conversions
take you with a function from A to B without the need to cast ? e.g. let{}. map{} ?
i
let 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.
Or let me put it differently
A 
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
r
@jimn yes, the 
Subtyping
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 this is regardless of kinds or containers of F. It works for all types regardless if they are kinded or not.
i
@raulraja I know I was just giving an example. I hope I didn’t insinuate wrong implications.
r
No wrong implications just pointing out this is more generic than just kinded value so there is no confusion. This works for all types
j
https://github.com/arrow-kt/arrow-meta/blob/rr-type-conversions/prelude/src/main/kotlin/arrow/Proof.kt points to an annotation... and the supporting directory of mechanisms looks like the reborth of boost template metaprogramming solutions.
is this going to elongate compilation times ?
i have a kotlin analog of pandas... i want to be able to specify a decoder from seralization bytes to Floats, and then perform some aggregations and signal that there will be a list of Floats. currently the only generic options i have are to use Any? and explicitly front-run all of my conversions
e.g. https://github.com/jnorthrup/columnar/blob/507f2b42e732b22d98f53c35325fa6793b78ce44/src/test/java/com/fnreport/mapper/ColumnarTest.kt#L91-L93 How am I able to define a system of functions to start with a column decoder of type A and stuff transforms of type T1....n into a tuple for these proofs to end up decoding input byte[] into output List<Float> ?
i would gladly submit this Columnar aggregation toy as a before and after example for Arrow-kt concepts, it's at a point where it simplifies the unpleasant pandas areas in my actual dayjob, and is purpose-built. I think arrow-kt type-proofs may be the start of a mechanism to track data transformations and potentially rescue SIMD compiler opportunities from combinatorial inputs
5 Views
Open in Slack
PreviousNext
Powered by