https://kotlinlang.org logo
Join Slack
Powered by
I want to add some fuel to the discussion about my...
# feed
a
I want to add some fuel to the discussion about my favorite multiple recievers, so I've added a small issue to the KEEP: https://github.com/Kotlin/KEEP/issues/209. The issue is built upon the old idea of file-level receivers in KEEP-176. In my opinion, the proposed solution in future could cure a split between KEEP-87 and KEEP-176 followers, fixing a rising concern for scripting framework as well. @raulraja, your comments are welcome.
h
You forgot one of my favourite proposals, companion vals, where i somehow extended the proposal and did a prototypal implementation of something very similar to what you search for. https://github.com/hannespernpeintner/kotlin/tree/keep-106/compiler/testData/codegen/box/companionval take a look at the CompanionValAtTopLevel.kt file. What is missing to fulfill your need is sth like an "external companion val foo:Foo" thing that may be enabled for Scripts only or so.
r
Hi @altavir, I very much like your proposal and would fit the use case for type classes. I have developed as part of Arrow Meta a lower level feature called Type Proofs as a compiler plugin that can express type classes, union types, tuples, kinds, refinements and implicit conversions using just extension functions to declare relationships between two types. It does exactly as your proposal does but does not use imports because the proofs are global and coherent in resolution. I will be happy to show you over hang outs if you are interested in this lower level feature that can express more things. We are using it to prototype KEEPs in 2020 for Unions, Refined types and derivation based on structure
If your proposal is accepted it’d be a good solution for type classes as mentioned.
The difference with KEEP-87 or how we are envisioning currently type classes in arrow is that users of type classes expect them to be coherent and when you want to do a local override you just add a new 
internal
instance you can’t export to third parties.
The compiler establishes synthetic subtype relationships between the two types and in codegen it replaces impossible casts for the proof
that is a proof for 
A
in 
Union<A, ….
This still uses the subtype system of Kotlin untouched, off course these features could be more deeply integrated all type classes are is syntax between two types, and with type proofs that is not just reduced to containers or parametric type classes but to any relationships between two types.
a
There is still a significant difference from what is (or at least was) at KEEP-87, namely this globality. It my proposal, the recievers are specifically local and are bound at use-site, not in declaration site. Meaning you can actually use a stateful object, not only a type-class. I hope that we will be able to find a solution, which suits everyone. Also, I need to mention, that my primary target is of course multipl recievers. File-level receivers are just a nice addition.
r
yes, I’m also in favor of multiple receivers
but I prefer implicit injection of type class syntax
a
Yeah, this is the point where the split lies.
r
if that is enabled with imports its fine too but then it becomes file scoped implicits not type classes
file scoped implicits it’s a good compromise
a
Yes, we already had a discussion in russian chat. And I agree that it is not exactly type-class. It is bound to the scope, not to a type.
And they should be explicits, otherwise you can't use stateful instances, which makes it useless for scriping.
The good thing that you can pass those explicits implicitely (sorry) from file to file, until you reach actual call site. And this call site could lie in a different module, which actually solves some problems, for which type-classes are used.
I still not sure what to do about generics, but it could probably be solved too.
r
Copy code
use com.mypackage.MyObject for com.mypackage.MyInterface
if that is stateful what controls instantiation for injection?
how would the compiler call 
MyObject
?
a
No, this is actually object usage which is quite similar to KEEP-87. I am talking about explicit scope:
Copy code
with(scope){
  callFunction()  // works
}
In this example the bounding is done in the call place and we can't call a method from our scoped file without a context
The same way it now works with scripts
r
I mean if 
MyObject
is a class or a global function that provides a value for 
MyInterface
the compiler needs to inject it somewhere in the case of enabling syntax by imports
In that case you have 
val
, 
fun
, 
object
and 
class
as concrete possible targets
a
MyObject is just a singleton instance of MyInterface
r
if you allow generics then you have to somehow express it in the import to disambiguate colliding instances
right but if it wasn’t an object
for example
a
If it is not an object, you provide only an interface and instantiate an object in the call site.
The code inside the file is compiled against the interface but actually called on provided instance. The scripting with implicit receivers works like that right now. You provide a reciever type for script deffinition and actual instance when script is called.
r
Copy code
use arrow.core.EitherMonad<Throwable, _> for arrow.core.Monad
There are cases where extensions need to be parameterized
a
Generics are hard subject and require a thorough study since type parameter will exist in the whole file. It could break something
Some limited aspects of HKT could also be implemented this way, at least it works for mathematical constructs in kmath (I use scoping objects, no file-level scopes, but idea is the same).
r
cool, is there an example somewhere of that encoding related to Kinds?
I’m using currently this encoding in meta which is more efficient than the one in arrow https://github.com/arrow-kt/arrow-meta/blob/sv-test-proofs/prelude/src/main/kotlin/arrow/kinds/kinds.kt
I’m interested in better encodings until I find a way to express this in a plugin but without the Kind interface in the way
a
Kmath separates operations from data so operations could be added to existing types by specifying the scope. Type binding is explicit, but in some cases it gives the same result as hkt: you can write mathematical expressions without knowing in advance what type will you use. Not in all cases of course. And from Scala/Haskell point of view it is not "true" hkt because of explicit bindings
4 Views
Open in Slack
PreviousNext
Powered by