I posted in general with no response so I assume i...

# language-proposals

[spand]

I posted in general with no response so I assume its missing. I think it could be useful to be able to remove the nullability of a generic type. Sort of the opposite of T? . Here I invented the T!! type operator for it. Should be clear from the example here why it could be useful.

interface LoadingCache<K : Any, V> {
    fun get(key: K): V // <-- If it can return null then it must be specified by type V

    // If load returns null then entries are missing hence it doesnt make sense to have here : Map<K,V?>
    fun getAll(keys: Iterable<K>): Map<K, V!!> {
        return keys.mapNotNull { k -> get(k)?.let { k to it } }.toMap()
    }
}

Thoughts ?

[Tomasz Krakowiak]

Wouldn't it be better:

interface LoadingCache<K : Any, V : Any> {
    fun get(key: K): V?
    fun getAll(keys: Iterable<K>): Map<K, V> {
        return keys.map { k -> get(k)?.let { k to it } }.toMap()
    }
}

Seems semantically more correct to me.

[spand]

No, if the LoadingCache is serves values from a total function then it does not make sense for get to have a nullable type.

[Ruckus]

Why would the user have the option to specify nullability on one method but not the other? That doesn't seem to be particularly applicable.

[Fleshgrinder]

@Ruckus it's already possible, but only one-way. @spand is asking for symmetry here.

fun <T : Any> f(input: T): T? { /* awesome stuff */ }

fun <T> f(input: T!!): T { /* awesome stuff */ }

[Ruckus]

Those aren't symmetric. In the first, the the API is specifying the nullability. In the second, the user gets to choose the nullability (but with the API patially overriding it?)

Still, it doesn't seem like a generally useful feature, more of a code smell. I could be missing something, but I don't get it.

[Fleshgrinder]

The two signatures given above are 1:1 equivalent in choice, just different locations. It's basically asking for a more expressive type system (unions, intersections, ...), and type theory is just set theory, so it's basically 𝑃 ↛ 𝑄 where 𝑃 is our generic and 𝑄 is null.

[Fleshgrinder]

Not sure if I could come up with an example that is exactly 1:1 the same. But, at the end this is proof that this would provide a functionality not covered today.

Rust has the ability to remove types from types. So it seems that they think it's useful.

[Ruckus]

They aren't equivalent. The first only allows:

val x: String? = f<String>("asdf")

The second would allow either

val x: String? = f<String?>("asdf")
val y: String = f<String>("asdf")

And I don't see a practical way for the function to distinguish them:

val x = f("asdf")

Is x a String or a String?? There's no way to know.

[Fleshgrinder]

They are equivalent in choice, but different in location. In the first I can choose the nullability of the parameter, but not of the return value. In the second I can choose the nullability of the return value, but not the parameter.

[Ruckus]

Those aren't the same thing at all.

[Fleshgrinder]

The example wasn't meant to be useful, it was meant to illustrate the request of @spand. 😉

[Fleshgrinder]

They aren't, never said they are. Again, just wanted to explain. 😛

[Ruckus]

I don't get what you were trying to explain. Also, I'm no expert, but I'm pretty sure "type theory is just set theory" is wrong, and the idea that all type systems can/should cover all of any given type theory seems like a bad idea.

[Fleshgrinder]

It's a special field of it: “Some type theories serve as alternatives to set theory as a foundation of mathematics. Two well-known such theories are Alonzo Church's typed λ-calculus and Per Martin-Löf's intuitionistic type theory.”

[Ruckus]

"Some implementations of X can serve as an alternative to Y" is clearly not the same as "X is a special case of Y"

[Fleshgrinder]

The type theory was initially created to avoid paradoxes in a variety of formal logics and rewrite systems. Later, type theory referred to a class of formal systems, some of which can serve as alternatives to naive set theory as a foundation for all mathematics. — https://en.wikipedia.org/wiki/History_of_type_theory

[Fleshgrinder]

They are related, same same but different. 😄

[Ruckus]

Also, that same article says:

Type theory is closely related to, and in some cases overlaps with, computational type systems, which are a programming language feature used to reduce bugs.

So even if they (type theory and set theory) were "the same" it still doesn't necesarily apply to type systems at all.

[Fleshgrinder]

type theory is just set theory

Which was an oversimplification to explain, draw an analogy, trying to explain with different concepts to arrive at something that is comprehensible. Sorry for that. I'll go and do something else. Really sorry.

[Ruckus]

I'm not trying to dismiss you, I'm trying to understand your claim. I'm just pointing out what appears to be a flaw in your logic. In this case, you say you're using the phrase "type theory is just set theory" as an oversimplification to help explain an idea, but you were actually using it as evidence to prove the equivalence of the two statements:

type theory is just set theory, so it's basically 𝑃 ↛ 𝑄...

If the root claim that "type theory is just set theory" doesn't hold, then the claim that "The two signatures given above are 1:1 equivalent in choice, just different locations." fundamentally isn't true. Does that make sense? Am I missing something important?

[Fleshgrinder]

Most certainly feels like it. Let me try again. If T? means T or null then T!! means T not null. So, if T is <T : Any?> then T!! is <T : Any>. This is like the referenced 𝑃 ↛ 𝑄 where 𝑃 is T and everything except 𝑄 which is null.

[Fleshgrinder]

Is it useful? Yes, see OPs example. Can we solve it maybe already with some Kotlin magic. Actually, we can:

Untitled

[Fleshgrinder]

But I'd argue that a cache should really use Optional to model this. Then the whole problem goes away and we can distinguish any Map.get returned value between key doesn't exist and value is not present.

[spand]

Thanks for participating and yes.. I really expect some kind of symmetry here. If I can add nullability then I ought to be able to remove it also.

Richard provided an example that shows that you can solve this in current Kotlin if the task can be reformulated in terms of extension methods. My use case here cannot since getAll() is a real native function that must be overridable and as I said earlier I would like to express the potential totallity of get() without getting an ugly return type on getAll() : Map<K, V?> in the non total case.

Current workarounds in Kotlin is using the extension method overloads as Richard shows. This workarounds is only really useable on functions. For interfaces we cannot just use the same workaround. Kotlin also "almost" has T!! in the form of `T : Any`:

interface LoadingCache<K : Any, V> {
    fun get(key: K): V // <-- If it can return null then it must be specified by type V
    // If load returns null then entries are missing hence it doesnt make sense to have here : Map<K,V?>
    fun <MV> getAll(keys: Iterable<K>): Map<K, MV> where MV : V, MV : Any {
        return keys.mapNotNull { k -> get(k)?.let { k to it } }.toMap()
    }
}

This is however prohibited by the Kotlin compiler. Not sure if this is a fundamental problem.

[elizarov]

In fact, T!! is internally supported by Kotlin's type system in the form of intersection type T & Any , and you may enounter this type from time to time, for example, as a result of a smartcast in if (t != null) expression. However this type is not directly denotable in the source code, but we do plan to make it denotable via this specific T!! syntax in the future.

[spand]

Great news. Do you have any idea when ? 1.6, 1.7, 1.8.. ?

[elizarov]

1.6 -> https://youtrack.jetbrains.com/issue/KT-26245