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

# language-proposalss

spand

04/23/2021, 7:54 AMI 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.
Copy code

```
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 ?t

Tomasz Krakowiak

04/23/2021, 8:27 AMWouldn't it be better:

Copy code

```
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.s

spand

04/23/2021, 9:22 AMNo, if the

`LoadingCache`

is serves values from a total function then it does not make sense for `get`

to have a nullable type.r

Ruckus

04/23/2021, 3:31 PMWhy would the user have the option to specify nullability on one method but not the other? That doesn't seem to be particularly applicable.

f

Fleshgrinder

04/23/2021, 7:48 PM Copy code

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

r

Ruckus

04/23/2021, 8:01 PMThose 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.

f

Fleshgrinder

04/23/2021, 8:24 PMThe 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

04/23/2021, 8:26 PMNot 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.

r

Ruckus

04/23/2021, 8:28 PMThey aren't equivalent. The first only allows:

Copy code

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

The second would allow either
Copy code

```
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:
Copy code

`val x = f("asdf")`

Is `x`

a `String`

or a `String?`

? There's no way to know.f

Fleshgrinder

04/23/2021, 8:30 PMThey 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.

r

Ruckus

04/23/2021, 8:31 PMThose aren't the same thing at all.

f

Fleshgrinder

04/23/2021, 8:31 PMThe example wasn't meant to be useful, it was meant to illustrate the request of **@spand**. ๐

Fleshgrinder

04/23/2021, 8:31 PMThey aren't, never said they are. Again, just wanted to explain. ๐

r

Ruckus

04/23/2021, 8:34 PMI 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.

f

Fleshgrinder

04/23/2021, 8:36 PMIt'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.โ

r

Ruckus

04/23/2021, 8:37 PM"Some implementations of X can serve as an alternative to Y" is clearly not the same as "X is a special case of Y"

f

Fleshgrinder

04/23/2021, 8:43 PMThe 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

04/23/2021, 8:43 PMThey are related, same same but different. ๐

r

Ruckus

04/23/2021, 8:44 PMAlso, 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.

f

Fleshgrinder

04/23/2021, 8:46 PMtype theory is just set theoryWhich was an oversimplification to

r

Ruckus

04/23/2021, 8:52 PMI'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?

f

Fleshgrinder

04/23/2021, 8:58 PMMost 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

04/23/2021, 9:06 PMIs it useful? Yes, see OPs example. Can we solve it maybe already with some Kotlin magic. Actually, we can:

Fleshgrinder

04/23/2021, 9:08 PMBut 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.s

spand

04/26/2021, 5:29 AMThanks 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`:
Copy code

```
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.e

elizarov

05/13/2021, 3:32 PMIn 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.โค๏ธ 2

s

spand

05/17/2021, 7:22 AMGreat news. Do you have any idea when ? 1.6, 1.7, 1.8.. ?

e

elizarov

05/17/2021, 8:26 AM๐ 1

9 Views