Could anyone talk about the current state of the t...

# language-evolution

[Leon K]

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?

[raulraja]

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.

[raulraja]

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

[raulraja]

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.

[Leon K]

union types as in

fun foo(x: String | Int) = when(x) {
  is String -> {...}
  is Int ->  {...}
}

? that sound's awesome!

[raulraja]

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

[raulraja]

Yeah unions like those

[raulraja]

https://github.com/arrow-kt/arrow-meta/tree/sv-test-proofs/compiler-plugin/src/test/kotlin/arrow/meta/plugins

[Leon K]

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?

[raulraja]

It may auto generated but essentially type classes have two kinds of members

[raulraja]

Static constructors and member functions

[raulraja]

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

[raulraja]

The proof establishes a subtype relationship

[raulraja]

When a type cast occurs then it replaces it for the function

[raulraja]

It's propositions between types via a morphism/function

[raulraja]

The Curry Howard Lambek correspondence with some limitations and other ways to implement things where you would use path dependent types

[raulraja]

We plan on hooking then to a theorem prover solver to do something similar to what Scala stainless does and have stronger constrains.

[raulraja]

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

[raulraja]

ADTs, equality, vals, etc

[raulraja]

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

[raulraja]

We will submit keeps for most or many of these features in case they are interesting to the lang in 2020

[Leon K]

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

[raulraja]

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

[raulraja]

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

[raulraja]

The biggest showstopper at the moment is that IDEA doesn't autoload IDE plugins projects depend on

[raulraja]

And for some of these features you'd like proper IDE support

[raulraja]

BTW we have type refinements without path dependent types

[raulraja]

Predicates are standard Kotlin

[raulraja]

https://gist.github.com/raulraja/a40b9a9fb3c381ec3281afac77f326d3

[Leon K]

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:

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?

[raulraja]

Yes, thou it can be the full validation map,.either or other type beside nullable

[raulraja]

Whatever you add a proof for. There is a nullable type.

[raulraja]

A proof is nothing but a global extension function between two types that the type system trusts

[Leon K]

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)?

[raulraja]

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

[Leon K]

that makes sense, i guess ;D I'll look be looking forward to try that stuff out! Thanks for your time, man ;D

[raulraja]

No problem, any time! 🙂