Sunday 9 June 2024

Kotlin (vs Python) Type System

I recently read this amazing article about the Kotlin type system. Though focused on Kotlin, it's useful to get a better understanding of Type Systems at a general level. In the past I would have thought of types just as classes, interfaces and functions, but particularly with advanced type systems like those in Kotlin, Python typing and TypeScript, we have to understand types in a broader sense (with nullable types, union and interception types where supported, Callables-Function Types, Nothing-Never...). I think we should think of Types as contracts of what an object can do, descriptions of what an object is. As the article says:

A class is a template for creating objects. A type defines expectations and functionalities.

I wrote in the past about Top and Bottom types in TypeScript and Python typing. I've realised that what I say in both articles about Any as a bottom type is not fully correct (at least "academically"). In both languages Any behaves as if it were at the bottom of the Type Hierarchy because it disables the type-checker, not because of allegedly sitting at the bottom of that Type Hierarchy. In TypeScript and Python the Any type allows us to combine the full dynamism of both languages and the convenience, safety and error preventing powers of types, cause by disabling the type-checker it's as if it were derived from any other type, and accessing to any method or attribute in it is valid. Casting an object to Any will allow us to add or access any attibute in that object without any complain from the type-checker.

This said, in Kotlin there's not that "as if", in Kotlin Any? (and Any) is just a Top type, it's not a "sort of" bottom type, and in Kotlin there's no way to disable the type-checker. The bottom type in Kotlin is Nothing. We can not cast an object to Nothing, and Nothing is mainly used to express cases where a function will never return (infinite loop, exception). As Nothing derives from any other type, if we mark a function as returning a string, but in some conditions it returns the string but in others it throws an exception, the compiler will be happy with it. Notice that we can not create an instance of Nothing or cast an object to Nothing. We can not create instances of Nothing, indeed, I think type-theory says that bottom types can not be instantiated, but I'm not 100% sure.


// can not create instances of Nothing (private constructor)
//var n = Nothing()

println("null is Nothing: ${null is Nothing}") //False

In Kotlin for the JVM the relation between Any and Object is a bit particular. While in Java all objects inherit from Object, as we've seen in Kotlin all objects inherit from Any? and Object does not show up in the type hierarchy diagrams. We can create instances using the Any and Object constructors, and at a Kotlin level both constructors will return an instance of Any (if we check its Kclass with instance::class). But in reality, at the JVM level, both instances are instances of Object (as we can see with instance::class::java). We can cast an Object instance to Any and viceversa, but the compiler will warn us each time we use Object with a: "This class shouldn't be used in Kotlin. Use kotlin.Any instead" message.


class Animal {}

var any1 = Any()
println("any1::class: ${any1::class}") //kotlin.Any
println("any1::class.java: ${any1::class.java}") //java.lang.Object
println("any1 is Any: ${any1 is Any}") // true
println("any1 is Object: ${any1 is Object}") // true
var ob: Object = any1 as Object


var o1 = Object()
println("o1::class: ${o1::class}") //kotlin.Any
println("o1::class.java: ${o1::class.java}") //java.lang.Object
println("o1 is Object: ${o1 is Object}") // true   
println("o1 is Any: ${o1 is Any}") // true       
any1 = o1 as Any //warning: no cast needed
any1 = o1

var a2: Animal = Animal()

// this does not compile: error: incompatible types: Object and Animal
println("a2 is instance of [Object]?: ${a2 is Object}")
    
// warning: this class shouldn't be used in Kotlin. Use kotlin.Any instead.
o1 = a1 as Object


As I've said, in Python, Any is a top type, and a sort of bottom type. We have to notice that Any only exists at the type-checking level, at runtime we can not check if an object is an instance of Any, and indeed we can not create an instance of Any. Python has a real bottom type, Never (that is equivalent to NoReturn)

A special kind of type is Any. A static type checker will treat every type as being compatible with Any and Any as being compatible with every type.[1]
The Any type is both a top type (so you can assign anything to Any) and a bottom type (so you can assign Any to anything). In effect it turns off the type system whenever you use Any.[2]

The behaviour of Any with regards to nullability is a bit strange. While for other type declarations, e.g. a1: Animal that declaration is a not nullable one (in Python it's common to say Optional rather nullable), and to get its nullable equivalent we have to use any of this forms: a1: Optional[Animal] or a1: Animal | None, for Any this is different. Any means any value, including None, so you can assign None to a variable declared as Any (None is compatible with Any), so Python's Any is different from Kotlin's Any. Though an Any varible could point to None, the type-checker will not apply on it the restrictions that it applies on nullables (Optional's), and we can access any attribute on it freely, cause indeed as I aforementioned, "Any disables the type checker". I we want something equivalent to Kotlin's Any? we should use Any | None. There's some discussion about this Any vs Optional[Any] here

We used to simplify any union containing Any to Any, but @ddfisher found out this is incorrect. E.g.if something is either an int or Any, when it is an int, it definitely doesn't have an append() method.

No comments:

Post a Comment