Hi all I am interested in the possibility of a Kotlin compil

Question

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

Nathan Bedell · Answer

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 · Answer

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 · Answer

For example ```fun lt A B gt F lt A gt fmap f A gt B F lt B gt ``` is already possible if ```expect class F lt out A gt ```

raulraja · Answer

then actual erases the abstraction replacing F for a target type

raulraja · Answer

```actual typealias F lt A gt = Flow lt A gt ```

raulraja · Answer

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

raulraja · Answer

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

raulraja · Answer

as you did there with Given

raulraja · Answer

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

raulraja · Answer

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 · Answer

< 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 · Answer

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 lt S T A B gt fun lt P gt P lt A B gt runOptic P lt S T gt ``` would not be possible or I guess at least a higher ranked usage of such an interface would not be possible

Nathan Bedell · Answer

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 · Answer

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 · Answer

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 · Answer

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

raulraja · Answer

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

raulraja · Answer

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