https://kotlinlang.org logo
Channels
100daysofcode
100daysofkotlin
100daysofkotlin-2021
advent-of-code
aem
ai
alexa
algeria
algolialibraries
amsterdam
android
android-architecture
android-databinding
android-studio
androidgithubprojects
androidthings
androidx
androidx-xprocessing
anime
anko
announcements
apollo-kotlin
appintro
arabic
argentina
arkenv
arksemdevteam
armenia
arrow
arrow-contributors
arrow-meta
ass
atlanta
atm17
atrium
austin
australia
austria
awesome-kotlin
ballast
bangladesh
barcelona
bayarea
bazel
beepiz-libraries
belgium
benchmarks
berlin
big-data
books
boston
brazil
brikk
budapest
build
build-tools
bulgaria
bydgoszcz
cambodia
canada
carrat
carrat-dev
carrat-feed
chicago
chile
china
chucker
cincinnati-user-group
cli
clikt
cloudfoundry
cn
cobalt
code-coverage
codeforces
codemash-precompiler
codereview
codingame
codingconventions
coimbatore
collaborations
colombia
colorado
communities
competitive-programming
competitivecoding
compiler
compose
compose-android
compose-desktop
compose-hiring
compose-ios
compose-mp
compose-ui-showcase
compose-wear
compose-web
confetti
connect-audit-events
corda
cork
coroutines
couchbase
coursera
croatia
cryptography
cscenter-course-2016
cucumber-bdd
cyprus
czech
dagger
data2viz
databinding
datascience
dckotlin
debugging
decompose
decouple
denmark
deprecated
detekt
detekt-hint
dev-core
dfw
docs-revamped
dokka
domain-driven-design
doodle
dsl
dublin
dutch
eap
eclipse
ecuador
edinburgh
education
effective-kotlin
effectivekotlin
emacs
embedded-kotlin
estatik
event21-community-content
events
exposed
failgood
fb-internal-demo
feed
firebase
flow
fluid-libraries
forkhandles
forum
fosdem
fp-in-kotlin
framework-elide
freenode
french
fritz2
fuchsia
functional
funktionale
gamedev
ge-kotlin
general-advice
georgia
geospatial
german-lang
getting-started
github-workflows-kt
glance
godot-kotlin
google-io
gradle
graphic
graphkool
graphql
graphql-kotlin
graviton-browser
greece
grpc
gsoc
gui
hackathons
hacktoberfest
hamburg
hamkrest
helios
helsinki
hexagon
hibernate
hikari-cp
hire-me
hiring
hongkong
hoplite
http4k
hungary
hyderabad
image-processing
india
indonesia
inkremental
intellij
intellij-plugins
intellij-tricks
internships
introduce-yourself
io
ios
iran
israel
istanbulcoders
italian
jackson-kotlin
jadx
japanese
jasync-sql
java-to-kotlin-refactoring
javadevelopers
javafx
javalin
javascript
jdbi
jhipster-kotlin
jobsworldwide
jpa
jshdq
juul-libraries
jvm-ir-backend-feedback
jxadapter
k2-early-adopters
kaal
kafka
kakao
kalasim
kapt
karachi
karg
karlsruhe
kash_shell
kaskade
kbuild
kdbc
kgen-doc-tools
kgraphql
kinta
klaxon
klock
kloudformation
kmdc
kmm-español
kmongo
knbt
knote
koalaql
koans
kobalt
kobweb
kodein
kodex
kohesive
koin
koin-dev
komapper
kondor-json
kong
kontent
kontributors
korau
korean
korge
korim
korio
korlibs
korte
kotest
kotest-contributors
kotless
kotlick
kotlin-asia
kotlin-beam
kotlin-by-example
kotlin-csv
kotlin-data-storage
kotlin-foundation
kotlin-fuel
kotlin-in-action
kotlin-inject
kotlin-latam
kotlin-logging
kotlin-multiplatform-contest
kotlin-mumbai
kotlin-native
kotlin-pakistan
kotlin-plugin
kotlin-pune
kotlin-roadmap
kotlin-samples
kotlin-sap
kotlin-serbia
kotlin-spark
kotlin-szeged
kotlin-website
kotlinacademy
kotlinbot
kotlinconf
kotlindl
kotlinforbeginners
kotlingforbeginners
kotlinlondon
kotlinmad
kotlinprogrammers
kotlinsu
kotlintest
kotlintest-devs
kotlintlv
kotlinultimatechallenge
kotlinx-datetime
kotlinx-files
kotlinx-html
kotrix
kotson
kovenant
kprompt
kraph
krawler
kroto-plus
ksp
ktcc
ktfmt
ktlint
ktor
ktp
kubed
kug-leads
kug-torino
kvision
kweb
lambdaworld_cadiz
lanark
language-evolution
language-proposals
latvia
leakcanary
leedskotlinusergroup
lets-have-fun
libgdx
libkgd
library-development
lincheck
linkeddata
lithuania
london
losangeles
lottie
love
lychee
macedonia
machinelearningbawas
madrid
malaysia
mathematics
meetkotlin
memes
meta
metro-detroit
mexico
miami
micronaut
minnesota
minutest
mirror
mockk
moko
moldova
monsterpuzzle
montreal
moonbean
morocco
motionlayout
mpapt
mu
multiplatform
mumbai
munich
mvikotlin
mvrx
myndocs-oauth2-server
naming
navigation-architecture-component
nepal
new-mexico
new-zealand
newname
nigeria
nodejs
norway
npm-publish
nyc
oceania
ohio-kotlin-users
oldenburg
oolong
opensource
orbit-mvi
osgi
otpisani
package-search
pakistan
panamá
pattern-matching
pbandk
pdx
peru
philippines
phoenix
pinoy
pocketgitclient
polish
popkorn
portugal
practical-functional-programming
proguard
prozis-android-backup
pyhsikal
python
python-contributors
quasar
random
re
react
reaktive
realm
realworldkotlin
reductor
reduks
redux
redux-kotlin
refactoring-to-kotlin
reflect
refreshversions
reports
result
rethink
revolver
rhein-main
rocksdb
romania
room
rpi-pico
rsocket
russian
russian_feed
russian-kotlinasfirst
rx
rxjava
san-diego
science
scotland
scrcast
scrimage
script
scripting
seattle
serialization
server
sg-user-group
singapore
skia-wasm-interop-temp
skrape-it
slovak
snake
sofl-user-group
southafrica
spacemacs
spain
spanish
speaking
spek
spin
splitties
spotify-mobius
spring
spring-security
squarelibraries
stackoverflow
stacks
stayhungrystayfoolish
stdlib
stlouis
strife-discord-lib
strikt
students
stuttgart
sudan
swagger-gradle-codegen
swarm
sweden
swing
swiss-user-group
switzerland
talking-kotlin
tallinn
tampa
teamcity
tegal
tempe
tensorflow
terminal
test
testing
testtestest
texas
tgbotapi
thailand
tornadofx
touchlab-tools
training
tricity-kotlin-user-group
trójmiasto
truth
tunisia
turkey
turkiye
twitter-feed
uae
udacityindia
uk
ukrainian
uniflow
unkonf
uruguay
utah
uuid
vancouver
vankotlin
vertx
videos
vienna
vietnam
vim
vkug
vuejs
web-mpp
webassembly
webrtc
wimix_sentry
wwdc
zircon
Powered by
Title
t

tschuchort

11/18/2019, 3:56 PM
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

bigkahuna

11/18/2019, 3:59 PM
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

Imran/Malic

11/18/2019, 4:15 PM
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

bigkahuna

11/18/2019, 4:16 PM
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

Imran/Malic

11/18/2019, 4:20 PM
No worries @bigkahuna 🙂
t

tschuchort

11/18/2019, 4:24 PM
What's path-dependent types? Is that like dependent types in Martin-Löf type theory? Even Haskell doesn't have those.
i

Imran/Malic

11/18/2019, 4:25 PM
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.
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

tschuchort

11/18/2019, 4:25 PM
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

Imran/Malic

11/18/2019, 4:43 PM
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

PhBastiani

11/18/2019, 4:49 PM
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

raulraja

11/18/2019, 5:35 PM
Kinds are gonna be easy to use with type proofs
👌 1
1
The only needed or autogenerated boilerplate is:
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

Imran/Malic

11/18/2019, 5:44 PM
@raulraja Can we say that
type-proofs
provide API’s over Types ? Somehow, the first steps for Kotlin to go
type-level
r

raulraja

11/18/2019, 5:45 PM
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

Imran/Malic

11/18/2019, 5:47 PM
I also love the formal answer 👌🏽
h

Hexa

11/20/2019, 7:46 AM
I would love it if Kotlin becomes more powerful than Scala
u

Uberto Barbini

11/20/2019, 9:55 AM
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

raulraja

11/20/2019, 10:13 AM
Agreed
And the type proofs plugin coming which models unions, kinds, refined types and morphisms between Kotlin types in general allowing ad hoc subtyping, extensions and polymorphism without inheritance will allow you to bend the type system to your will.
Since you are all functionally inclined. In the category of the Kotlin types where the morphisms are the functions type proofs establishes a trust relationship with the Kotlin compiler where you can tell it you know the path between two types and the implication that has. The arrow prelude demonstrates the Kotlin type system can be extended by providing a custom typechecker based on proofs that eliminate the need for inheritance by exploiting subtype Polymorphism and the top Any? and bottom types Nothing. In Kotlin we can have value holes we can fill in with type proofs in any expression position.
i

Imran/Malic

11/20/2019, 10:36 AM
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

raulraja

11/20/2019, 10:48 AM
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

jimn

11/20/2019, 11:33 AM
Conversions
take you with a function from A to B without the need to cast ? e.g. let{}. map{} ?
i

Imran/Malic

11/20/2019, 12:04 PM
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

raulraja

11/20/2019, 1:22 PM
@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

Imran/Malic

11/20/2019, 2:02 PM
@raulraja I know I was just giving an example. I hope I didn’t insinuate wrong implications.
r

raulraja

11/20/2019, 2:19 PM
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

jimn

11/20/2019, 3:49 PM
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