Could KAnnotator infer @Immutable and @Pure annotations?


#1

Sorry if this isn't the correct forum for KAnnotator questions, I couldn't find a more appropriate one.

Could KAnnotator infer a @Pure annotation on methods?  Eligable static methods would guarantee that for a given set of @Immutable parameters, it will produce the same result with no side effects?

It could also infer @Immutable on classes, which would indicate that all of the classes fields are themselves immutable (ie. vals and either primitive types, or immutable classes)?

Instance methods on @Pure classes are @Immutable if they guarantee that for a given instance of the class, and a given set of @Immutable parameters, they are guaranteed to return the same result without side-effects.

Applications for this would include a compiler code-transformation that automatically makes @Pure methods cache their results.


#2

We are working on these things. There's a lot to be done. Any related work you know about is of interest for us.


#3

I'm excited to hear that Andrey!

I’m afraid I’m not aware of any work other than my own thinking about it, which I suspect is way behind your thinking on it, but here it is anyway:

Classes can be declared @Immutable if all of their fields are vals (final), and if those vals are types that are themselves @Immutable.

A method is @Pure if all of its parameters and return type are @Immutable types, it doesn’t modify any vars in its object, and it only calls @Pure methods.

I’m probably over-simplifying it.  I suppose one issue might be a method that met the criteria for being @Pure, but actually did employ mutable state for efficiency reasons (eg. to cache a result).  KAnnotator might decide that the method isn’t @Pure, even though it behaves exactly as a @Pure method would, just faster.


#4

Is there a reason to not use a "const" keyword? Although I can see how it would be useful to make Java code seen as immutable/pure/const transparently from a Kotlin side and annotations is probably the easiest way to get there.

Another thing I’m thinking about is how far the immutability concept should be taken?
I personally don’t think that the various possibilities to directly change data using JVM trickery should stop efforts to have helpful semantics at the language level.

I’d love to have a feature that by saying a class is immutable I get assistance from the editor suggestions and compiler that my class is in fact immutable, including the aggregated data.


#5

I'd love to have a feature that by saying a class is immutable I get assistance from the editor suggestions and compiler that my class is in fact immutable, including the aggregated data.

+1 from my side. If a method could be declared @Pure (because all in and out parameters and return type are @Pure) that would be terrific. I looked several times at FP. Each time I took another serious unbiased attempt to get the point what all the effort is about. I always came to the conclusion that programming without sidde-effects (aka @Pure) is what has a good effort/utility balance and can be realistically brought over to imperative programming.

– Oliver


#6

Yeah I just bumped into this,

writing my first ever kotlin unit test i discovered the extension method:

class Pair{
  public infix fun <A, B> A.to(that: B): Pair<A, B> = Pair(this, that)
}

Thats obviously pure, and without any additional information for the compiler the kotlin statement

someObject.to("B")

is perfectly legal kotlin, a no-op, and likely an error all-in-one.

With @Pure annotations and an extra compiler pass it should not be hard to generate warnings on these kinds of statements, which might catch a number of newbie errors.


#7

Hey Andrey,

I have no Idea if you guys are still working on this topic, but maybe you can check out Frege. They call it “a Haskell for the JVM”. And somehow they managed to include a concept for Immutability and for pure functions.


#8

We have retired KAnnotator for a number of reasons. Introducing extra metainformation, like purity, would be interesting, but we need more use cases to justify the costs


Inconsistency in null safety