Hi all. I am interested in the possibility of a Ko...

# arrow-contributors

[Nathan Bedell]

Hi all. I am interested in the possibility of a Kotlin compiler plugin for HKTs in Kotlin, and @raulraja invited me to come up with some examples of what such a plugin might look like. I have created an initial gist for this purpose -- which I may flesh out more in the future.

Currently the most fleshed out (and I think most realistic) example for an MVP can be found in FlowHKT.kt, where I have some examples showing how HKTs might interact with subtyping, and some thoughts on inference for kinds. Anyway, I hope this is a good way to get the ball rolling, and I look forward to feedback/discussions.

https://gist.github.com/Sintrastes/3920cf4efcea4c933b19382222e59ce2

[Nathan Bedell]

I think the biggest thing that's kind of an open question as to how this plugin would work in Kotlin is: How would kind inference work? Is that feasible in a language with subtyping?

Of course, in terms of previous work, there's a lot of prior art to go off of in Scala in terms of how HKTs interact with subtyping -- but I don't think even Scala 3 (correct me if I'm wrong) does any inference of kinds, so I'm not sure how feasible that would be to do.

[raulraja]

Thans @Nathan Bedell!, Scala provides multiple features for kinds but there may be only one we may b interested which is the ability to describe programs polymorphically. Maybe we can do it without a cost if we follow a model similar to the one in expect /actual

[raulraja]

For example:

fun <A,B> F<A>.fmap(f: (A) -> B): F<B>

is already possible if

expect class F<out A>

[raulraja]

then actual erases the abstraction replacing F for a target type

[raulraja]

actual typealias F<A> = Flow<A>

[raulraja]

wecan look into a similar model where a user defines a type is a kind

[raulraja]

the plugin then expects what type it maps to based on providers

[raulraja]

as you did there with @Given

[raulraja]

and replaces references to the type for that of the concrete type.

[raulraja]

What I mean to say is that perhaps is much easier to treat special types as kinds and then translate than actually adding kinded types to the type system because that would touch inference, type checking for sub typing, resolution and many features compiler plugins won’t expose by default.

[Nathan Bedell]

@raulraja That definitely seems like a promising approach! I agree that would be far easier than actually trying to interact with the type system itself.

[Nathan Bedell]

The question I have is: Are there any disadvantages to that approach?

If I understand it, it seems like with that approach we would be limiting higher-kinds to use-cases where they can be completely monomorphized. So, for instance, something like:

interface Optic<S,T,A,B> {
    fun <P> P<A,B>.runOptic(): P<S,T>
}

would not be possible -- or I guess at least a higher-ranked usage of such an interface would not be possible.

[Nathan Bedell]

Please correct me if I'm wrong on that -- but even if that were true, I still think that is definitely an acceptable trade-off.

[raulraja]

this would be possible if we treat all function bodies as abstract inlineable templates that are stored and persisted in metadata or we tap in the inline function system.
This way all polymorphic definitions remain templates that at some point someone with the compiler plugin can materialize in a different module.

[raulraja]

This would allow you to store the Optics interface whose members refer to P a type that is kinded as a template. Someone at some point would have to say that P is some actual type or context provider instance

[raulraja]

here is an example of the ide of substituting types in Ir before codegen and inlining

[raulraja]

kinds.cpp

[raulraja]

it recursively substitutes all types of F making them Option, but also preserves the metadata of programs of F

[raulraja]

if you don’t want to use the plugin you have the alternative to implement what F means and that is how you make it concrete in that case paying the cost of the allocation per abstraction