https://kotlinlang.org logo
Join Slack
Powered by
Question about arrow-proofs: I can see that polymo...
# arrow
y
Question about arrow-proofs: I can see that polymorphic proofs are a thing, so how do you deal with a proof like 
Foo<Foo<T>> -> Foo<T>
? That proof is valid in that it's not cyclical, but if you're working backwards from knowing that we need a 
Foo<T>
then I can't see how to ascertain that this proof isn't applicable (because the proof is applicable if e.g. there's a 
Foo<Foo<Foo<T>>>
that can be created). One can obviously look at other proofs that provide a Foo of something and use those as a starting point, but what if there's a proof 
Bar<T> -> Foo<T>
and the only proof returning 
Bar<T>
requires a 
Foo<Foo<T>>
(akin to mutual recursion) Also will arrow-proofs support something like
Copy code
@Inject fun <A, B> test(@Given bar: Bar<A, B>, @Given foo: Foo<A>): B = bar.someFunctionThatTakesFooAndReturnsB(foo)
As in, will type parameter be properly substituted in like that and allowed to influence the resolution of what proof to use for 
foo
, or will the caller have to specify 
A
and 
B
for the call to resolve correctly? Looking around the plugin code I can see that for every 
Inject
function you generate one with default arguments, so I can't really see how this use case could be supported.
j
About
Copy code
@Inject fun <A, B> test(@Given bar: Bar<A, B>, @Given foo: Foo<A>): B = bar.someFunctionThatTakesFooAndReturnsB(foo)
We are dropping value arguments injections as we are going to center on Context Receivers. So it would be written so:
Copy code
class Bar<X, Y>

class Foo<Z>

fun <A, B> Bar<A, B>.someFunctionThatTakesFooAndReturnsB(foo: Foo<A>): B = TODO()

context(Bar<A, B>, Foo<A>)
fun <A, B> test(): B = someFunctionThatTakesFooAndReturnsB(this@Foo)
And where you need to consume 
test
, or in other words, resolve everything, you need to provide the final types for 
Bar
and 
Foo
Copy code
context(Bar<String, Boolean>, Foo<String>)
@ContextResolution
fun consumer() {
    test()
}
Then you get a generated 
consumer
Copy code
// generated
@JvmName("test_generated")
fun consumer(
    bar: Bar<String, Int> = provideBar(),
    foo: Foo<String> = provideFoo(),
): Int = with(bar) { with(foo) { test() } }
Which you can use in, for example, 
main
Copy code
fun main() {
    consumer()
}
But in order to resolve it, it is necessary to have all 
Contextual
, now we would got an IDE/Compile error indicating that all proofs are missing, so we need to add something like:
Copy code
@Contextual fun <X, Y> provideBar(): Bar<X, Y> = Bar()

@Contextual fun <Z> provideFoo(): Foo<Z> = Foo()

@Contextual fun provideString(): String = "baz"

@Contextual fun provideInt(): String = 42
About 
Foo<Foo<T>>
and so on, I am not sure if we are covering that use case yet, but if we are not doing or it is not working we will do if it is possible
r
All polymorphic proofs (also concrete ones) are resolved with Kotlin's frontend resolution mechanism. That is if you have a 
type
that you need to get injected we provide all proofs as candidates for that resolution from which the most specific and concrete one is selected. For proofs that have injectable arguments we recurse over their resolution. I'm not positive in this case because we don't have a test for it but it should resolve it or we should be able to fix it if it doesn't. It'd be a bug if it does not resolve
Copy code
inject<Foo<Foo<Int>>() == Foo(Foo(0))
for example
y
That makes sense, so no type-inference capabilities then between context receivers. Type-inference only works when you want a concrete type and there's a generic 
@Contextual
fun
for it. That makes sense. I guess for the 
Foo<T>
thing, let me word it instead as this:
Copy code
@Contextual 
context(Foo<Foo<T>>) fun <T> provideFoo(): Foo<T> = this@Foo.extractInternalFoo()

@Contextual fun <T> provideNestedFoo(): Foo<Foo<Foo<T>>> = TODO()
 
context(Foo<T>)
@ContextResolution
fun consumer() {
  // Do something with Foo
}

fun main {
  consumer()
}
This should resolve normally obviously by using provideFoo twice and provideNestedFoo once. Now imagine if provideNestedFoo didn't exist. How would the plugin know in that case that recursively trying to find 
@Contextual
functions for 
provideFoo
will never terminate?
r
It doesn't know about termination at the moment but can detect cycles between proofs. That is, it would keep on resolving if Kotlin had recursive type definitions or recursive type aliases but it doesn't https://github.com/arrow-kt/arrow-proofs/blob/new-approach/arrow-inject-compiler-p[…]ata/diagnostics/context-receivers/circular_proofs_cycle_rule.kt
y
So would that 
Foo<T>
example just keep on resolving forever without provideNestedFoo?
r
I'm not sure but I'm guessing it won't since it will find 
provideNestedFoo
as most specific and at some point if there is a cycle it will detect it
y
Sorry I pressed Enter too early. Without provideNestedFoo there won't be an endpoint so what will happen then?
r
y
Would it really be the same cycle though? In the first example provideFoo is allowed to be used for itself n-times as long as there is a provideNestedFoo returning an n+1 nested Foo (e.g. provideFoo will be used 3 times if there's a provideNestedFoo that returns 
Foo<Foo<Foo<Foo<T>>>>
), and without provideNestedFoo then each call to provideFoo is requesting a more-nested version of Foo, so the "request" is different each time. I'm just wondering algorithmically if there is a way to differentiate the first example (that has provideNestedFoo) from one that doesn't have provideNestedFoo without having to work forwards from all contextuals that don't have 
context
arguments themselves. If you prohibit a 
@Contextual
function from using itself you break the example I mentioned, and if you don't then you risk stack overflows whenever a 
provideNestedFoo
doesn't exist.
r
yeah, it's very likely broken now, we did not dig that far there and this is something we probably should add to the test cases
y
Thank you for taking the time to answer my questions btw. I'm working on something similar to arrow-proofs but with support for more type-system features (akin more to C++`s concepts) and I ran into this breaking case myself.
r
But it may detect the cycle because the cycle knows if it's iterating over the same @contextual, even if it's broken now it's something we can detect and stop if it's not making progress
If what you are working on it's public would love to take a look. 🙂
y
Yeah I guess you can have a hard limit of 100 calls or something and then you just report it as a cycle. It is, it's pretty barebones though. github.com/kyay10/Koncept A lot of it is broken right now, even polymorphism. But basically I'm injecting my own 
ConeCallConflictResolverFactory
into the session so then the 
FirCallResolver
uses me for conflict resolution and so I can inject my own `Candidate`s. I then use 
FirTowerResolver
with a custom 
CandidateCollector
which replaces the 
CheckContextReceiver
resolution stage with a custom one that tries out my `@Concept fun`s and sees if any provide the right return type.
Where it differs from 
arrow-proofs
is that it works without a 
ContextResolution
annotation or a 
context<TypesNeeded>()
call, and hence it doesn't need concrete types to be specified. I'm also planning to introduce certain plugin-provided `Concept`s like 
Kind<A, B>
which only has an instance available if A is a type that came from a type constructor applied to B (e.g. 
Kind<List<Int>, Int>
exists, so does 
Kind<Map<String, Boolean>, String>
but 
Kind<List<String>, Int>
doesn't). Then with those pieces you can practically make Type classes actually a thing in Kotlin, which is what I'm trying to achieve. I think that arrow-proofs can actually do this rn but you'll have to call 
context<Functor<List<String>, String>>()
before a function that requires a Functor in its context.
r
in the new iteration of arrow proofs we don't have a 
context
function
simply we automatically turn context receivers to regular arguments with default values that point to the providers. This allows you to override a provider in any place with the generated function
Same as @Javier described above in the 
consumer
example.
That is the same as type classes in my mind but not restricted to declaring them based on type arguments, works for any context type.
The current missing piece in Kotlin for context receivers to provide the same set of features as type classes is to have the automatic injection piece. In practice injection can be deferred with context receiver all the way to the edge. For what I can see here it's very similar to what we have https://github.com/kyay10/koncept/blob/master/kotlin-plugin/src/testData/box/simple.kt
In our case, this would look like:
Copy code
package foo.bar

import io.github.kyay10.koncept.Concept

@Contextual class A
class B(val message: String)

context(A, B) fun myFun(): String {
  return message
}

@Contextual
fun gimmeB() = B("OK")

@ContextResolution
context(A, B)
fun box(): String = myFun()
then it would generate a regular 
box
without the 
context(A, B)
that surrounds the call to 
myFun
with nested 
A().run { gimmeB().run { ...
it actually places those in arguments so you can call 
box
with different impls of A and B that may be used for testing
y
Have a look at https://github.com/kyay10/koncept/blob/master/kotlin-plugin/src/testData/sandbox/display%20concept.kt I'm not sure if arrow-proofs would be able to do it because of 
Display
declaring its required contexts inside of its type parameters (it's a trick I came up with so that everything can be an 
object
and so no allocations would be needed). Also issue with proofs is that it still requires the user to manually specify all contexts that are used inside the function. Not only will it get very long and unmaintainable if we're using arrow-proofs for type classes, but also possibly contexts could have some interaction with others. (e.g. a 
List<String>
could be coming from a library, while a 
List<CharSequence>
is coming from an internal declaration. A user might add the 
List<String>
context first, then silently the function that wanted a 
List<CharSequence>
will use it, but if using automatic injection, both functions will receive the most specific value. It's a small difference, but it can change behaviour in unexpected ways)
j
We are blocking providing third party types outside of the current module as you have to mark those providers as 
internal
So it is not possible to provide 
List<String>
outside the current module as it will be 
@Contextual internal fun foo(): List<String>
= …
y
Replace 
List
in my explanation with a library-defined type. So the library provides a 
MyList<String>
and the user internally provides a 
MyList<CharSequence>
.
r
I believe the display example would work with proofs as well because we support val, fun, object and class and if those where @Contextual you can define Display<String> in an object in the same way, if it doesn't work it should not be by design since type arguments and generics are supported too
But maybe it doesn't work today because we are still in rough state in some areas
y
Huh, that's pretty reassuring then. I guess my only gripe with proofs is the manual injection, but if that's solved then it's basically what I'm designing right now. I can make a PR with a custom 
ConeCallConflictResolverFactory
for arrow-proofs if you'd like to pursue automatic injection because frankly it feels like I'm reinventing the wheel and I don't think I have the compiler expertise to continue on solo with such a mammoth task.
r
Also issue with proofs is that it still requires the user to manually specify all contexts that are used inside the function
If you look in the same repo you will find everything we discussed for context also working over regular value arguments. In that case we resolve injection on the body as you do there. We found resolving injection on the body it's problematic because then it resolves to the provider in the module but it cannot be replaced for testing or other purposes. In order to work similar to scala implicits you have in that case a function like:
Copy code
fun <A> given(): A = TODO("replaced by compiler plugin")

val x = given<Int>()
Once you do that then it becomes bytecode and not an argument you can replace later with a different instance of Int
we plan on getting rid of value argument injection and focus exclusively in context receivers
We think people in Kotlin would use that for DI in most cases and the missing piece is just the resolution of a context function into a non context function
that will be the base of the plugin
y
When it comes for replacing for testing, one can obviously just turn it into a context receiver if it makes sense to replace that argument for testing. I don't think that that's an argument for not going with automatic injection then because who's going to be replacing a functor implementation for lists only in tests?
I think context receivers are definitely the way to go in that regard
j
for testing, the codegenerated function has default values, but you can override any of them easily
r
yeah, we are just aiming it at DI not so much at the notion of type classes
j
Copy code
// generated
@JvmName("test_generated")
fun consumer(
    bar: Bar<String, Int> = provideBar(),
    foo: Foo<String> = provideFoo(),
): Int = with(bar) { with(foo) { test() } }

fun sometest() {
    consumer(bar = anotherBar())
}
r
When it comes for replacing for testing, one can obviously just turn it into a context receiver if it makes sense to replace that argument for testing
The issue is that we want to support compiled providers and we scan all the class path not just the local module. Functions with implicit arguments in our case need to survive compilation so they can be replaced when you have a library of providers
If you resolve in the body you loose the ability to replace already compiled functions that had dependencies on providers. The only way is to preserve those as arguments in context or regular
y
I see, yeah from the prespective for a DI user they obviously want to preserve the ability to replace providers for compiled functions, while from the prespective of type classes it doesn't seem as important.
r
right
different goals but indeed very similar 🙂
y
So that makes automatic resolution not very vital then for arrow-proofs. That makes sense! Thanks for all the help. What I think I might try to do is create like a "companion plugin" for arrow-proofs maybe that can do automatic resolution and that will add plugin-provided proofs for things like 
Kind
and such. That's probably the best of both worlds. I'll have a look to see if the visible API surface of proofs is enough to do that, and if not I might make a PR exposing some of it.
r
would love to collaborate together, keep us updated and we will ping you with any progress, thanks for sharing all this info @Youssef Shoaib [MOD] 🙂
8 Views
Open in Slack
PreviousNext
Powered by