Implicit Casts for Verified Type Information

Evolution Pitches
1

Kotlin implicitly casts an object after its type is checked. As a Swift and Kotlin programmer, I frequently find myself wishing Swift, which has a similar type system, had this feature. It seems to be in line with Swift's design goals of supporting sophisticated (while still being predictable) type inferencing.

These implicit casts are type-safe, reduce code clutter and improve performance by eliminating redundant checks:

Example (Swift-ified version):

if obj is String { print(obj.count) }  // implicit cast

The same is true for nullability. After you've verified a type isn't nil it is converted to its non-nullable counterpart, so the ! is no longer required.

Edit: A clarification in response to @cukr's question - The reference type isn't being changed. The compiler tracks type and nullability narrowing for the context and dynamically inserts casts.

5 Likes
2

What would happen to code like this?

var obj: Any = "Hello"
if obj is String {
    obj = 123
    print(obj)
}

What would happen to code like this?

var _obj: Any = "Hello"
var obj: Any {
    defer { _obj = 123 }
    return _obj
}

if obj is String { 
    print(obj)
}

What would happen to code like this?

var obj: Any = "Hello"
func indirectMutation() {
    obj = 123
}
if obj is String {
    indirectMutation()
    print(obj)
}
5 Likes
3

@cukr Thank you for these questions. In your first example, the re-assignment of 123 will work because obj's declared type is Any.

Kotlin's behavior for:

    var obj: Any = "hello"

    if obj is String {
        print(obj.count) // smart cast inserted before .count is accessed
        obj = 123 // is allowed because the declared type is Any
        print(obj) // prints "123"
    }

Under the covers it is tracking the checks that narrow the known type and nullability, inserting casts as needed.

Details: Type Checks and Casts: 'is' and 'as'

For your other example:

var obj: Any = "Hello"

func indirectMutation() {
    obj = 123
}

if obj is String {
    indirectMutation()
    print(obj)
}

This is allowed for the same reason: obj is declared as Any. The output will be 123.

1 Like
4

What would happen if I wrote print(obj.count) instead of print(obj) in these code samples?

5

It will work. Under the hood the compiler inserts a cast:

print(obj.count) becomes print((obj as String).count)

...which allows .count to work, but also allows obj to be reassigned to 123 (because it is declared as Any).

1 Like
6

(I'm assuming you meant Kotlin's as which is equivalent to Swift's as!)

Oof. So I'm going to start getting random crashes from failed casts even though I don't cast, or use exclamation marks anywhere? I don't like the sound of that. I wouldn't trust this feature at all.

I bet that there would be a lot of people confused by the method resolution.

Today we have if let which is slightly more to write, but doesn't magically change the behavior of my variables, and is more explicit about what it does. And you can trust that it won't randomly crash your code. And it even gives you access to both the original variable, and the casted object.

2 Likes
7

I would expect statically checked type safety from something described as "type-safe".

Wouldn't it reduce performance by introducing more checks?
if let foo = obj as? String { print(foo.count) } does a single check, but if obj is String { print(obj.count) } would perform two, one for is, one for obj.count

I wonder what do you find similar in the type systems of kotlin and swift

1 Like
8

I think you are unfairly criticizing the initial pitch.

if obj is String {
   // do string stuff
}

If the compiler can verify that obj is not modified between the if expression and its use within the block, it should be perfectly safe for an implicit cast to be inserted by the compiler, such that it would be equivalent to:

if let obj = obj as? String {
  // locally-scoped obj is a String
}

but with optimizations possible by avoiding the actual type checking at runtime.

I don't know if the compiler can guarantee success analysis in a sufficient number of cases to make the feature both useful and non-confusing, but that's a separate pair of questions.

9

(I'm assuming you meant Kotlin's as which is equivalent to Swift's as! )

This works with "is" exactly as written. It also works with "as". Feel free to test it using the Kotlin REPL.

Oof. So I'm going to start getting random crashes from failed casts even though I don't cast, or use exclamation marks anywhere? I don't like the sound of that. I wouldn't trust this feature at all.

That is incorrect. As @Avi pointed out, when the compiler sees you have just tested obj is String and there is no assignment prior to treating it like a string, the cast is provably safe.

Remember, this is a feature used in a popular language. It isn't a random idea that just popped into my head.

I bet that there would be a lot of people confused by the method resolution.

Why would it confuse Swift developers more than Kotlin developers?

I wonder what do you find similar in the type systems of kotlin and swift.

Both type systems make heavy use of type inferencing and support null safety in similar ways.

@Avi

I think you are unfairly criticizing the initial pitch.

Thank you Avi. Your description of how it works is correct. I probably could have explained it more clearly in my initial post.

It is thoroughly documented in the Kotlin spec and docs.

I don't know if the compiler can guarantee success analysis in a sufficient number of cases to make the feature both useful and non-confusing, but that's a separate pair of questions.

Kotlin's success with it makes me confident that Swift's compiler can "guarantee success analysis in a sufficient number of cases to make the feature both useful and non-confusing".

I've been porting a new typed declarative language called KD to Kotlin, Swift and C#, so I've been head deep in type systems for months. I prefer Swift 75% of the time, but Kotlin does a few things better, even with the restrictions of the JVM. This is one of the things that bites me when I move back and forth between them.

10

Okay, I studied the kotlin documentation, and repl. The moment my understanding went off the rails is here:

I started talking about casts at runtime, because it was the only way I thought it could work, but in kotlin it does not work. There are situations where kotlin smart casts will not work, and code samples all fall into them.

In the first code sample local variable is mutated (broken rule 3 "if the variable is not modified between the check and the usage") 
fun main(args: Array<String>) {
	var obj: Any = "Hello"
	if (obj is String) {
    	obj = 123
    	print(obj.length) // Unresolved reference: length
	}
}

In the second code sample I'm using a computed variable (broken rule 2 "properties that have custom getters" or rule 1 "local delegated properties") No code sample, because I don't think you can have a custom getter for a local var in kotlin.

In the third code sample (broken rule 3 "captured in a lambda that modifies it") 
fun main() {
    var obj: Any = "Hello"
	fun indirectMutation() {
    	obj = 123
	}
	if (obj is String) {
   	 	indirectMutation()
    	print(obj.length) // Smart cast to 'String' is impossible, because 'obj' is a local variable that is captured by a changing closure
	}
}

Btw, the real rules are even more complicated than this. For example this code compiles in kotlin, even though the variable is modified between the check and usage. What's more, it's being smart casted into a type that it's not being checked for!

fun main(args: Array<String>) {
    var obj: Any = "Hello"
    if (obj is String) {
        obj = "World"
        println(obj.length)
        obj = 5
        println(obj.countOneBits())
    }
}

I filed a bug report. https://youtrack.jetbrains.com/issue/KT-42579

I am a swift developer, and I'm already confused. :(

2 Likes
11

I'm most certain this has been pitched one or two times before, if only I could find it. IIRC, we'd want a very consistent rule where this does or does not apply. Relying on when the compiler can proof it is not great when things can get arbitrarily complex, like:

if !(x is Int) {
  var continuing = true
  while continuing {
    continuing = ...
    if !continuing { continuing.toggle() }
    else { return }
  }
}
// Umm, do we cast?

There's also a Swift's stance that type conversion should be explicit, which let has been doing nicely.

4 Likes
12

Okay, I studied the kotlin documentation, and repl.

I appreciate you taking the time.

I started talking about casts at runtime, because it was the only way I thought it could work, but in kotlin it does not work .

I failed to notice you were passing a local var in your example. Apologies.

There are situations where kotlin smart casts will not work, and code samples all fall into them.

These restrictions all make sense. You can't use implicit casts when the compiler can't guarantee the type, just as Swift requires you to provide an explicit type declaration if the inferencing system lacks the information necessary to determine the type. Also, the rules are different for local variables in both cases.

Neither fails silently. You will get a compile time error in both cases.

re: Your examples. These examples check if obj is a String (which would normally cause a smart cast in that context if the compiler can guarantee it can't be modified, per the rules you quoted), then immediately assign an Int, and attempt to perform operations on obj. This fails, as it should, because the newly assigned obj's type is Any and the compiler has no additional information. If you want to see a quick example of a smart cast working in the Kotlin REPL try:

fun printCount(obj:Any) {
     if (obj is String) { println(obj.length) }
 }
 printCount("Hello")

I am a swift developer, and I'm already confused.

I'm willing to bet this is due to, as you said, you having spent more time with Swift. I'm also a Swift developer, and when I first came to Kotlin this implicit type / nullability narrowing behavior was unexpected, but as with Swift, once I understood the concept I could guess how it's going to work with a high degree of accuracy and it saved me a lot of casting and null safety checks that aren't needed. When I made a mistake, the compiler's errors were very clear. As an experienced Swift developer, it's likely you would have the same experience.

The great thing about Swift and Kotlin is that, once you get the concepts, you can usually guess how something is going to work. This is no exception. At this point I've spent a couple thousand hours with Kotlin, and I assure you, it is helpful in avoiding unnecessary type and nullability checks.

Swift goes to a lot of trouble to remove unneeded explicit type declarations. I posit this is in keeping with the language's design goals.

13

On a separate note, I'm not sure if it's really an improvement given that Swift already has multiple ways to type cast, unwrap optionals, and express the control flow intention.

I feel like the Kotlin's way of doing

if (x is Foo) { /* x is Foo */ }
if (x !is Foo) { /* always returns */ } // x is Foo

is just equivalent to Swift's way of doing

if let x = x as? Foo { /* x is Foo */ }
guard let x = x as? Foo { /* always returns */ } // x is Foo
4 Likes
14

Thank you @Lantua. I'm happy to review any previous discussion of this feature.

IIRC, we'd want a very consistent rule where this does or does not apply.

They are. The docs I referenced explain them. The rules can generally be condensed to: If you have a variable that can't be reassigned to a different type, and there is a check for a narrower type via the is or as operator, the narrower type is available via implicit casts provided by the compiler.

In practice, this is very easy to read and understand:

func printCharCount(obj:Any) {
  if obj is String {
    print("Chars: \(obj.count)")
  }
}

printCharCount(obj:"Hello")

Note: This is a proposed Swift feature. It won't compile.

Relying on when the compiler can proof it is not great when things can get arbitrarily complex.

True, but you could make the same argument against Swift's type inferencing of, for example, array and dictionary literals. We still have type inferencing because it is easily understood in most cases, and even in complex cases the rules are clearly defined. I would argue this is no more complex.

Finally, this is a battle tested feature being used by millions of developers. It's not experimental. Would it work in Swift? There is nothing in the grammar or compiler that would prevent it.

15

I wish I could link you there. It was a very extensive discussion, part of which we're reiterating.

I did read the doc. It is still pretty vague. I see that Kotlin also try to dig into disjunction clauses (||), which means that it should also try to figure out:

if (x is Int || condition1 || condition2),
  (x is Int || condition3 || condition4) {
  // is x Int here?
}

and I just turn our compiler into a 3SAT solver. If we'd restrict it to a top-level condition, then it's not that big of a win against existing syntaxes. I'm not arguing against the feature per se, but false negative can be just as confusing as false positive.

We do have specifications about ordering (which overload is preferred over which), albeit not official. I'd prefer it if we end up officializing those specifications (or ones the supersede them) at some point.

Also, AFAICT, Kotlin's smart casts is the only way you can (safely) downcast types, which is not the case in Swift. So while it is invaluable in Kotlin, maybe not so much in Swift.

2 Likes
16

I'll see if I can hunt this discussion down. Thank you for making me aware of it.

Interesting. I haven't explored their use in disjunction clauses because I normally use smart casts via is in simple when and switch cases. I'll take another look at this section of the docs.

I appreciate your detailed reply.

17

Well, (obviously) Kotlin won't really figure that out, but I just demonstrate my point that if the specification is not very concise, users will expect some interesting scenario to just work.

3 Likes
18

Sorry for being too combative.

non-local var doesn't work either (rule 4)

Yep, I agree. They make sense. They are just complicated.

Huh? I don't remember type inference rules being different in swift for local variables. (unless you meant in repl/debugger/main.swift mode which is broken)

Kotlin smart casts fail silently. For example:

var obj: Any = "Hello"
fun <T>f(arg: T) { println("generic") }
fun f(arg: String) { println("string") }
fun main() {
    if (obj is String) {
        f(obj) // prints "generic" because there was no smart cast
    }
}

This feature is so confusing, that even people writing documentation get it wrong. I'm not saying that swift doesn't have confusing features. It does. I just don't want to make the current situation worse. Let's take for example this existing swift code:

func g(_ arg: Int) throws -> String { ... }
func f(arr: [Int]) throws -> String? {
    return try arr.lazy.map(g).first
}

It looks like it uses lazy to make sure that g is executed only on the first element. It doesn't do that. The whole array is mapped, before returning the first element. That is a bug with method dispatch being too complicated. Compiler gave me no warnings, no errors. All the unit tests will be successful. No matter how experienced you are, this is an easy mistake to make. With smart casts, it would be even easier to make - even moving a variable to a different scope would be able to break your code.

2 Likes
19

@Chris_Lattner3 (who, as I’m sure you’re aware, first created Swift) had this to say in 2016:

6 Likes
20

I think you found the thread to which @Lantua was referring. Reviewing the previous discussion was very helpful.

It appears Lysenko and I went through the same journey of working with Kotlin's type narrowing, and wanting something like it in Swift. We also came to the same conclusions.

Exactly. It appears that this was never really resolved, or perhaps @Chris_Lattner3's post, quoted above, ended it.

The difference is that we now have a large body of code in another popular language that uses what was proposed then and now. You can always create examples where a feature like this is less obvious, as I did for type inferencing of type structure literals, and @Lantua did for type narrowing with disjunction clauses, but in the wild, it is used extensively in areas like simple switch cases and (in Kotlin), when. In these far more common cases, it makes code more readable.

I've had the same experience. In practice, Kotlin's type narrowing makes code easier to read and is not deleterious to maintainability.