https://kotlinlang.org logo
#language-evolution
Title
# language-evolution
l

Leon K

02/23/2020, 1:01 PM
Could anyone talk about the current state of the two "type-class"-like KEEP-proposals? (https://github.com/Kotlin/KEEP/pull/176 and https://github.com/Kotlin/KEEP/pull/87) What is their current status? Is there any indication that one of them will be implemented into the language in the "not-so-distant" future?
r

raulraja

02/23/2020, 5:48 PM
Regarding type classes as far as KEEP-87 is concerned is being reworked in a much more flexible system that allows encoding of type classes, type refinements, union types etc. We are working on it on Arrow Meta and it's called Type Proofs. We plan on resubmitting keeps for all these features after April as we test them in the arrow code base.
❤️ 1
It's currently still on meta on a branch but soon will make it to master and when it does anyone can try them out
Type classes and polymorphism as designed in meta works for both subtype and ad-hoc polymorphism. It eatablishes synthetic subtype relationships between the types and replaces impossible casts for proofs.
l

Leon K

02/23/2020, 5:51 PM
union types as in
Copy code
fun foo(x: String | Int) = when(x) {
  is String -> {...}
  is Int ->  {...}
}
? that sound's awesome!
r

raulraja

02/23/2020, 5:52 PM
Type classes as in proyecting members from one type to another as syntax https://github.com/arrow-kt/arrow-meta/blob/sv-test-proofs/prelude/src/main/kotlin/arrow/typeclasses.kt
Yeah unions like those
l

Leon K

02/23/2020, 6:00 PM
that looks incredibly promising! You guys are doing god's work over at arrow! could you explain the
Syntax<A>
part? what does that
Syntax
interface do / mean?
arrow 1
1
r

raulraja

02/23/2020, 6:01 PM
It may auto generated but essentially type classes have two kinds of members
Static constructors and member functions
To work naturally with Kotlin subtyping it's best to differentiate them so you can project them over the companion or over the data type accordingly
The proof establishes a subtype relationship
When a type cast occurs then it replaces it for the function
It's propositions between types via a morphism/function
The Curry Howard Lambek correspondence with some limitations and other ways to implement things where you would use path dependent types
We plan on hooking then to a theorem prover solver to do something similar to what Scala stainless does and have stronger constrains.
At that point proofs will be able to verify formally local programs that are a pure subset of Kotlin and that we model for the solver
ADTs, equality, vals, etc
We were hoping to use Arend from Jetbrains but it seems it's not yet at that point so most likely will end up depending on inox ir similar to hook to the constrain solver
We will submit keeps for most or many of these features in case they are interesting to the lang in 2020
l

Leon K

02/23/2020, 6:12 PM
I'll need to wrap my head around most of that, haha! sounds brilliant! How much of that can you imagine ever being implemented into standard kotlin? I feel like It's realistic to have Unions some day, and the whole KEEP-87 idea seems to be pretty universally liked as well, but I cannot really imagine having anything resembling dependent types or type-based Proofs in Kotlin.. but maybe that's just me ;D
r

raulraja

02/23/2020, 6:16 PM
I'm not sure but the good news is that plugins are already powerful enough to do these things and the output they produce is compatible in regular Kotlin
As a user nothing stops me from adopting these features in the same way I use the serialization plugin or the allopen plugin, or jetpack compose which entirely relies on plugins
The biggest showstopper at the moment is that IDEA doesn't autoload IDE plugins projects depend on
And for some of these features you'd like proper IDE support
BTW we have type refinements without path dependent types
Predicates are standard Kotlin
l

Leon K

02/23/2020, 6:27 PM
so the compiler check's the String-literal in
TwitterHandle("@adminxxxxxxxxxxxxxxxxxxxxxxxx")
, check's it with the validate function and then knows it's not a valid TwitterHandle, thus the code does not compile? That sounds pretty cool! But how does this work with non-literal values? I see you have these examples:
Copy code
val runtimeAdminWillBeNull: TwitterHandle? = admin 
//null

val runtimeWhateverIsValidated: TwitterHandle? = whatever 
//TwitterHandle("@whatever")
.. Am I correct in understanding it the following way: if you provide a literal, the compiler can know that your value is either valid or not, and validate the type at compile-time. If you give it a value or otherwise a "calculation", It cannot compile-time verify and thus returns a nullable type?
👍 1
r

raulraja

02/23/2020, 6:34 PM
Yes, thou it can be the full validation map,.either or other type beside nullable
Whatever you add a proof for. There is a nullable type.
A proof is nothing but a global extension function between two types that the type system trusts
l

Leon K

02/23/2020, 6:39 PM
So this is a kind of implicit conversion, specialized for type-refinement? you provide the
@Proof
function that converts from
String -> TwitterHandle?
(or one that converts into
Maybe<TwitterHandle>
, etc) which is then used to generate the inline class instance? what would happen if i did
TwitterHandle(admin)
(put a non-literal value into the constructor)?
r

raulraja

02/23/2020, 6:56 PM
It fails to compile and forces you to use instead
TwitterHandle.from
or one of the validation methods in the refined interface, still under design
l

Leon K

02/23/2020, 7:04 PM
that makes sense, i guess ;D I'll look be looking forward to try that stuff out! Thanks for your time, man ;D
r

raulraja

02/23/2020, 7:07 PM
No problem, any time! 🙂
2 Views