Subtyping

[shelby3]

Union types express a subtyping relationship, but I am unclear as to whether typeclasses (i.e. Rust's traits) do?

If a trait B extends another trait A and B reuses the implementations of A, can we assign a trait object that has a bound B to a trait object that has a bound A?

Seems the answer based on prior discussion is yes. But that is a subtyping relationship, which means we would need to deal with covariance on type parameters both when they are trait objects and when they are unions. Correct?

Prior discussion: https://github.com/keean/zenscript/issues/6#issuecomment-248711828 https://github.com/keean/zenscript/issues/1#issuecomment-248113585 https://github.com/keean/traitscript/issues/2#issuecomment-248021713 https://github.com/keean/zenscript/issues/1#issuecomment-248754649

[shelby3]

No offense intended, but to be curt... you are thinking about it wrong. Because your mind is apparently still stuck on the way Haskell infers types.

Haskell never subsumes (it doesn't even have subtyping at all). With inferred subsumption, then what I wrote is correct.

[shelby3]

Please see the new Higher-kinded Issue #10. I think it best summarizes the issue at hand.

Also please note that implementation of sort you attempted had no typeclass List. Please explain what this type families concept is and why you would ever want a List typeclass? Feel free to make a new Issue for that topic if it is not related to Subtyping.

[shelby3]

@keean wrote:

data List<a> = Nil() + Cons(head: a, tail: List<a>)

because the a is a type parameter it has to be exactly the same on both sides. If you want subsumption it has to be expressed as a type constraint.

Sorry you are incorrect. The inference algorithm can choose an value for a which satisfies the constraints. Since unions are available, it can subsume to the GLB which is the disjoint union.

You've apparently not been around Scala to know that is the way it is done with subtyping (even if subclassing is removed). And you've apparently tried to shoehorn the Haskell way of doing things when you do C++ or Rust. Well I don't know that, but seems maybe to be the case. I don't mean that as a criticism, because you are very strong in Haskell and I am weak in Haskell. But we can't use Haskell to solve the Expression Problem, because its type system won't allow it.

I already noted that you admitted having a myopia or resistance to any concepts related to subtyping. You even claimed that a programming language shouldn't have a Top and Bottom type. This comes from your exposure to Haskell's coinductive type system which places Bottom at the top and Top at the bottom of the type system, which disallows subtyping and moves non-termination (i.e. Bottom type) from an effect to a value.

Please try to understand. We've been talking about this for weeks during April/May and now again about 2 weeks. I hope we can finally understand each other on this issue?

Edit: please don't conflate all the bad of subclassing with subtyping. Subtyping is another dimension in the multi-dimensional space of type systems. If we discard it, we lose power¹.

1. 10

   2

[shelby3]

In this comment, I will write 'type parameter' where I mean the "type parameter on a type constructor" and not type parametrization of a function (where examples of type constructors include collections Array or List).

Type parameter variance

For those readers who don't know how subclassing (note I did not write 'subtyping') interacts with typing the variance of the type parameter of a type constructor, note that all programming languages which have subclassing have to manage the variance of the type parameter.

Default variance

Some languages by default make all such type parameters invariant, meaning that it is never possible to assign a subtype or supertype to any instance of the said type parameter. So an invariant Array<T> would mean you can never assign any supertype or subtype of T (what ever T is for the constructed instance of Array<T>).

TypeScript has by default something they refer to as bivariance which is incorrect, unsound, and allegedly unsoundness more often than they claim.

Variance annotations

Most languages offer some form of variance of said type parameters. For those languages that allow declaration of the variance, there are two variants: use-site and declaration-site variance annotations. Java has use-site and N4JS has both use-site and declaration-site. Afaik, Scala and Ceylon (and perhaps Kotlin and others) have declaration-site variance annotations.

Declaration-site variance

I will describe declaration-site variance. We define SUB to be a subtype of SUP (i.e. SUP is a supertype of SUB). A type parameter declared covariant, means that an instance of Array<SUB> can be assigned to a reference of type Array<SUP>, but not vice versa. And conversely for a type parameter declared contravariant, means that an instance of Array<SUP> can be assigned to a reference of type Array<SUB>, but not vice versa.

In order to enforce that the above allowed assignments won't cause the type of reference to an Array to become invalid, the compiler checks all instances of the type parameter are congruent with the declared variance. For covariant, this means the type parameter can never be used for method arguments but can be used for result values, which is why Ceylon chose out for this annotation. And conversely, for contravariant this means the type parameter can never be used for result values but can be used for method arguments, which is why Ceylon chose in for this annotation. As you probably expected, Scala uses some arbitrary symbol soup ASCII art which is impossible to intuitively describe and remember.

Typeclass objects

If Rust's typeclass objects (which I think will also be in ZenScript?) allow subsumption to their supertypes (i.e. when a trait extends another trait), then it is also subject to variance of type parameters. Except afaik Rust's type parameters are always invariant, because subsuming the trait object doesn't usually make sense, since a trait bound is always open to extension for new data types, unlike subclassing. And there is no subtyping in Haskell.

ZenScript

I don't think we've made decision yet whether ZenScript's type parameters will be invariant for typeclass bounds of typeclass objects? For our union types, invariant is sufficient except we must make them covariant (and/or contravariant) when we want to offer extension of variants (as a solution to the Expression Problem) in for example preexisting instances of List.

I hope this helped everyone understand what is going on with subtyping, variance of type parameters on constructors, and the differences thereof w.r.t. to subclassing, typeclass objects, and our new proposed unions.

[keean]

@shelby3

Scala is not a good example of a well designed type system. Personally I don't think the original type system was designed by someone who understood type systems, although they are now trying to fix their mistakes.

I don't have miopia when it comes to types, I understand what you are saying, but type systems are a logic, and you cannot just make the semantics up. They have to confirm to the behaviours of the underlying mathematical logic. Consider a type system a pure Prolog program (Horn clause logic effectively).

You do not want inferred subsumption. That is like inferred casting if number types in C, it introduces a magic black box into the type system that you can never get rid of. You are stuck forever with the language doing weird things you don't want it to. It is much better to have a sound type system and implement whatever weird functionality you want in a library that the user can optionally import if they want whatever flavour of weird behaviour it implements.

[keean]

@shelby3 this is important:

Subtype polymorphism is replaced in type class languages by type classes.

Consider an Array <T> in a language with subtyping you can put any function that is a subtype of T into the array. But what is a subtype? It is a type that implements at least the functions of the interface of T. So any type you insert must implement a certain set of functions (Liskov substitution principle). If we instead of giving an object type that defined the set of functions we must define, we instead give an interface (type-class), then we no longer need the mess that is variance.

[keean]

Further from the previous comment, what would the interface to a union type look like. You want to be able to inject a type, and project the type, using type indexed lookup. Let's ignore the implementation, what you get is something like:

trait Union T
   inj<A>(u : T, x : A) // inject value of type `A` into the union
   prj<A>(u : T) : Maybe<A> // project value of type `A` from the union

Now we can have Array<Union> and we can insert a value of any type, and read it back (providing we know the type we are looking for, a bit like a type-safe and sound cast).

[keean]

Perhaps I should add a little explanation of my type system methodology. If you make a bunch of stuff up (see Scala) you then have to go through a huge process of proving soundness, which is hard, and easy to get wrong (hence the unsoundness that occurs in other languages).

Fortunately there is a better way. If we consider types as atoms in a pure sound subset of Prolog, we can write programs in this Prolog to give the desired behaviours of the type system. Then we only have to prove the Prolog sound (which had been done for Prolog variants used in proofs, see "Prolog PTTP".

It happens that type-classes are the same thing, effectively a pure Prolog program (if we assume backtracking instance matching with no overlapping instances). So taking a language of atoms which represent types, and invariant variables (so we have a logic) we can write type system extensions that are definitely sound.

Now we can always have some syntax sugar to make things usable for the programmer, but if you cannot implement the features you want in this 'meta language' it is probably not sound.

[shelby3]

@keean wrote:

You do not want inferred subsumption.

This is getting tiring. You are contradicting yourself. You already agreed in the Union issue discussion which you marked as "Accepted" that we would infer if(x) "string" else 1 to be a Number|String.

I think we better move our discussion to private messages for a while and see if we can understand each other. I will message you in LinkedIn after I sleep when I wake up.

I want to speak with you frankly off the public record.

So many languages infer the union subsumption now including Ceylon, TypeScript, etc..

If you make a bunch of stuff up (see Scala) you then have to go through a huge process of proving soundness, which is hard, and easy to get wrong (hence the unsoundness that occurs in other languages).

Making a great language is hard. That isn't an excuse for making a crappy boilerplate (thus unpopular) language. Without implicit, information preserving, lossless subsumption to the union, I am gone. Simple as that. And I will take the name with me and my ideas with me. (Of course, you can continue to use the name regardless, I just mean I can also use it)

I invested a lot of effort here. :toilet:

[shelby3]

@keean wrote:

You do not want inferred subsumption. That is like inferred casting if number types in C, it introduces a magic black box into the type system that you can never get rid of. You are stuck forever with the language doing weird things you don't want it to.

I am reasonably sure you are incorrect, because the subsumption is disjoint and information preserving in our case, i.e. we are not discarding any information, which the other forms of casting and subsumption do.

Thus, I am nearly sure you are wrong. Of course it needs to be formalized to check.

[shelby3]

Sorry I need to be more blunt, because losing too much precious time. I need to know if we are creating a language I can use or not.

@keean wrote:

Subtype polymorphism is replaced in type class languages by type classes.

Incorrect. Subclassing polymorphism is replaced by type classes in Haskell. Subtyping wasn't replaced by anything, rather it doesn't exist in Haskell's coinductive, upside-down type system.

You continue to make egregious errors because you Can Only Think One Way™ (the way of Haskell's limitations).

If we instead of giving an object type that defined the set of functions we must define, we instead give an interface (type-class), then we no longer need the mess that is variance.

Incorrect.

As I explained already, this is only true because we choose to after subsuming data types to trait bounds, not further subsuming typeclass objects (aka Rust trait objects) to GLB of a set of trait bounds that extend from a common trait bound. That is named invariant. Otherwise, subtyping and variance comes into play same as for subclassing because the trait object is constructed instance's type parameter.

Analogously when we choose not to subsume further the constructed instance's type parameter when employing subclassing, then variance also does not come into play. That is named invariant.

[keean]

So what is wrong with the Array<Union> solution i gave? As I said, if you cannot formally define the typing feature you want, it is probably unsound. Just because the definition looks like boilderplate does not mean the user would ever see it. It may be in a library, or it may be inside the compiler (like a lot of type system weirdness like subsumption rules in other languages). I prefer to have it in a library, because then if I am interested, and I understand the formalism, I can read the exact rules that will be used by the type system.

Don't confuse formally defining type system rules, with programs the users would write, just because we can define these rules using type-classes.

[keean]

@shelby3 wrote:

Incorrect.

As I explained already, this is only true because we choose to after subsuming data types to trait bounds, not further subsuming typeclass objects (aka Rust trait objects) to GLB of a set of trait bounds that extend from a common trait bound. That is named invariant. Otherwise, subtyping and variance comes into play same as for subclassing because the trait object is constructed instance's type parameter.

Analogously when we choose not to subsume further the constructed instance's type parameter when employing subclassing, then variance also does not come into play. That is named invariant.

I think you are forgetting about existential types (like Rust trait objects). You can have (I don't know what our syntax for an existential type would be)

data AnyUnion = forall A . (Union<A>) => AnyUnion A

Now an Array<AnyUnion> can have a different implementation of 'Union' in each element.

[shelby3]

@keean wrote:

So what is wrong with the Array<Union> solution i gave?

There is no Maybe involved at all. All types in the union have a type-case boilerplate injected by the compiler to implement any trait bound at the call-site where the union is passed as an input. Every where else the compiler is tracking the type of union only.

[shelby3]

@keean wrote:

I think you are forgetting about existential types (like Rust trait objects).

I mentioned trait objects in what you quoted.

Now an Array<AnyUnion> can have a different implementation of 'Union' in each element.

Per this and my prior comment, you are back to premature virtualization (dynamic dispatch) which was the problem I was fixing. You are going backwards. This is getting very tiring.

You can't seem to wrap your mind around my solution to the Expression Problem, even I have explained every possible way I can think of to explain it. In #10, I provided another good explanation.

[keean]

@shelby3 I don't understand what you are saying here:

There is no Maybe involved at all. All types in the union have a type-case boilerplate injected by the compiler to implement any trait bound at the call-site where the union is passed as an input. Every where else the compiler is tracking the type of union only.

You are back to premature virtualization which was the problem I was fixing. You are going backwards. This is getting very tiring

What do you mean by 'premature virtualization?'

[shelby3]

@keean wrote:

I don't understand what you are saying here:

I am too sleepy to try to explain my solution to the Expression Problem for the umpteenth time. Could you perhaps read what is linked?

Maybe when I wakeup, I will be re-energized.

What do you mean by 'premature virtualization?'

Ditto above.

[keean]

Lets change tack (but still on subtyping). If I have a list of the type you describe, and we assume set based subtyping:

let x1 = Nil() // inferred type List<A> where 'A' is an unknown type
let x2 = Cons(123, x1) // List<Int>
let x3 = Cons("A", x2) // List<Int|String>
let x4 = Cons(0.1, x3) // List<Int|String|Float>

now if I want to swap the values in position 1 and 3, I can put 123 into slot 1, but I cannot put 0.1 into slot 3. I can of course build a new list (so this is no good for in-place sorting, and worse only works on a single container type, not on my arrays, maps, sets, queues, dequeues etc.)

But what happens with this:

let x1 = Nil()
let x2 = if random_bool then Cons("ABC", x1) else Cons(123, x1)
let x3 = if random_bool then Cons("ABC", x2) else Cons(123, x2)

what is the type of x2? If we infer the union we would get List<String> | List<Int> which I don't think is what we would want.

What is the type of x3? List<Int> | List<String> | List<Int|String> which again I don't think is what we want.

[shelby3]

@keean wrote:

Lets change tack (but still on subtyping).

You need to understand my solution to the Expression Problem. I provided you the link.

I can of course build a new list (so this is no good for in-place sorting, and worse only works on a single container type, not on my arrays, maps, sets, queues, dequeues etc.)

It might be possible to build those other container types in a way that is compatible.

Map would probably be easy, because you simply check the counter before you return it. I won't go into detail now... Ditto Set.

If you want to use an Array or any standard data structure, then serialize the List into it. Again we need higher-kinds #10.

what is the type of x2? ... If we infer the union we would get List<String> | List<Int> which I don't think is what we would want.

Since these are data types and not trait bounds, then List<String> | List<Int> is a subtype of (and can be subsumed to) List<String|Int> but they are not equivalent, i.e. an instance of List<String|Int> can't be assigned to a reference with type List<String> | List<Int>.

This is just math of sets.

What is the type of x3? List<Int> | List<String> | List<Int|String> which again I don't think is what we want.

Ditto what I wrote for x2

[keean]

Ah, but that's not true in general, because it depends on the properties of a List. With an arbitrary generic there is no rule for how the type-parameter is used.

So those rules would have to be defined per type. So somewhere where we define List we would also have to add a bunch of typing rules to make that happen in the right way for lists.

[keean]

@shelby3 I don't think any of the functionality for the List contradicts what I wrote above, I was just trying to make it work for an Array.

As I said elsewhere I am happy with subtyping based on sets, I am just thinking out-loud on how to combine sets based subtyping with otherwise invariant types, type classes etc.

[shelby3]

@keean wrote:

Ah, but that's not true in general, because it depends on the properties of a List. With an arbitrary generic there is no rule for how the type-parameter is used.

So those rules would have to be defined per type. So somewhere where we define List we would also have to add a bunch of typing rules to make that happen in the right way for lists.

Only the variance of the type parameter need be defined. What I wrote assumed covariant. Contravariant types are weird thus less frequent, basically coinductive such as a stream.

[keean]

@shelby3 wrote:

Only the variance of the type parameter need be defined. What I wrote assumed covariant. Contravariant types are weird thus less frequent, basically coinductive such as a stream.

I think its more complicated than that, because the type class may not be a container/collection at all.

For example what would you do with the type-equality class (trying on some of the new syntax for size):

pluggable TypeEq<A, B>

impl<A> TypeEq<A, A>

So type-eq constrains two types to be the same. What would happen with TypeEq<A, B> | TypeEq<B, C>

In fact I don't think what you suggest can work with multi-parameter type classes at all?

[shelby3]

@keean wrote:

I think its more complicated than that, because the type class may not be a container/collection at all.

We aren't subsuming typeclass bounds into unions (we haven't yet decided whether to implicitly subsume them to their GLB common supertype typeclass¹).

Only data types go into unions. Remember we agreed very early that unions of typeclasses don't make any sense, which you wrote here, you reiterated, and then I agreed. And where I explained why we need unions for data types, I agreed again not for trait (typeclass) bounds.

---

1. @shelby3 wrote:

   Typeclass objects

   If Rust's typeclass objects (which I think will also be in ZenScript?) allow subsumption to their supertypes (i.e. when a trait extends another trait), then it is also subject to variance of type parameters. Except afaik Rust's type parameters are always invariant, because subsuming the trait object doesn't usually make sense, since a trait bound is always open to extension for new data types, unlike subclassing. And there is no subtyping in Haskell.

   ZenScript

   I don't think we've made decision yet whether ZenScript's type parameters will be invariant for typeclass bounds of typeclass objects?

[keean]

Okay so what about multi parameter datatypes like a pair:

data Pair<A, B> = Pair(A, B)

what would happen to Pair(Int, Float) | Pair(String, Char) ?

[keean]

My vote is to only allow set based subtyping, so that Int <: Int | String and that is it.

I think we need to have per-datatype rules if we want to have any type isomorphisms for unions.

[shelby3]

Please note upthread edit:

1. Since an eager, CBV language makes Bottom an effect, I have argued the name of the Bottom type should be Never and not Nothing (which appears to be the choice TypeScript made). Bottom is for example the type of functions that never return (terminate). Whereas, in a lazy, CBN language such as Haskell, Bottom becomes a value, so I argue it should be named Nothing and not Never.

[keean]

I don't think we need a bottom type. Failure to type check will be failure. Where do you see a bottom being necessary?

Isn't that the billion dollar mistake?

I would argue that when you want a type that is Nothing, you have to use Maybe (Haskell) or Option (Rust). I am not sure which is better but I am used to Maybe:

data Maybe<A> = Nothing() | Just(A)

[shelby3]

@keean wrote:

I don't think we need a bottom type. Failure to type check will be failure. Where do you see a bottom being necessary?

All ZenScript functions will always return? What type will you give to functions that never terminate?

@shelby3 wrote:

Bottom is for example the type of functions that never return (terminate).

We can't properly model Nil in the type system without the concept of Bottom. Also Bottom is necessary for modeling LUB (least upper bounds) which is for example necessary in the contravariant case.

You need to understand that the type inference engine has to think in terms of GLB and LUB else it won't be correct. This is not Haskell. I don't know how many times I need to repeat that.

---

@keean wrote:

Isn't that the billion dollar mistake?

No that was Hoare's opinion about null values. Remember I just wrote that in an eager, CBV language (such as ZenScript), then Bottom is never a value, rather only an effect. This is why Scala has a separate type for Null which is not the Bottom type Nothing. But Scala made a mistake by naming Bottom Nothing instead of Never because Scala is eager, CBV, so Bottom can never be instantiated.

[keean]

You don't need bottom, you type Nil polymorphically as: List<A>

No bottom, no variance!

I want a sound type system, and that means following the rules :-)

Edit: Not returning has nothing to do with it consider:

fn() =>
    while true:
    return 1

This never terminates, but has a return type of Int.

[shelby3]

@keean wrote:

You don't need bottom...

Please answer:

@shelby3 wrote:

All ZenScript functions will always return? What type will you give to functions that never terminate?

[keean]

I answered in the edit above. Definitely nothing like that Scala subtype tree! Only subtyping for union (set) types.

The fact that someone had to draw that diagram to understand it shows what a bad idea it is :-)

[shelby3]

@keean wrote:

I answered in the edit above.

You have not answered regarding the type of non-termination. You answered w.r.t. to the Nil value. You keep repeating the same mistake in your thought process. Non-termination is an effect in a eager, CBV language such as ZenScript (and most other programming languages on the planet other than Haskell), not a value like in Haskell.

[keean]

@shelby3 wrote:

All ZenScript functions will always return? What type will you give to functions that never terminate?

That does not make sense. Function return types have nothing to do with termination? I don't understand where you got such a strange idea from?

The function return type is determined statically from the code at compile time. This is the same in C, C++, Pascal, Ada, Rust ... in fact every statically typed language I know of.

[shelby3]

@keean wrote:

That does not make sense. Function return types have nothing to do with termination? I don't understand where you got such a strange idea from?

What is the type of a function that throws always throws an exception? What is the type of exit() function? (such as if we want to allow ZenScript to be used in scenarios where PHP is currently employed)

You've been fooled by your familiarity with Haskell. In Haskell, non-termination is a value and inhabits every type, thus it never has to be declared as a value.

[keean]

Hold on, I see what you are talking about. You mean functions that do not return anything, rather than functions that never return? like "print".

PHP is not a programming language :-)

The answer is they return '()' or void. Its a type which has no values, thats all, it does not necessarily have a subtyping relation with other type...

[shelby3]

@keean wrote:

Hold on, I see what you are talking about. You mean functions that do not return anything, rather than functions that never return? like print.

The answer is they return () or void. Its a type which has no values, thats all, it does not necessarily have a subtyping relation with other type...

No the singleton Unit type is not the Bottom type.

Bottom can't be instantiated in an eager, CBV typing system, thus it can't be a singleton. How many times do I need to repeat this (the bolded). Your mind is locked into Haskell's type system.

[keean]

See my example from above again:

fn() =>
    while true:
    return 1

The return type is Int, this function never returns.

[keean]

Example from C:

int fn() {
    while true;
    return 1;
}

[shelby3]

@keean if your function never terminates, and you don't type it as Bottom, then you will have unsoundness.

TypeScript's documentation explains several use cases, including:

Because never is assignable to every type, a function returning never can be used when a callback returning a more specific type is required:

function test(cb: () => string) {
    let s = cb();
    return s;
}

test(() => "hello");
test(() => fail());
test(() => { throw new Error(); })

[keean]

So the compiler does termination analysis on the code? This is known as the halting problem, so any type system that includes never is by definition unsound.

For example consider the Mandelbrot recursion? How can you tell if the loop ever terminates? The border between termination and non-termination is an infinite detail fractal.

[shelby3]

@keean wrote:

So the compiler does termination analysis on the code? This is known as the halting problem, so any type system that includes never is by definition unsound.

You are conflating orthogonal concepts.

Turing-completeness is due to unbounded recursion (of the tape). The type system is only modeling the body of the function. The typing system can't model run-time behavior such as infinite recursion.

[keean]

So what do you mean by 'non-termination' ?

[shelby3]

@keean wrote:

So what do you mean by 'non-termination' ?

The body of the function has in every code path which doesn't return, e.g. throw but note a Bottom is subsumable so a single throw (non-termination path) combined with a concrete return could be subsumed to that concrete return value (but in the case of unions we can't subsume to a union | Never because Bottom is never a value). This excludes dependent typing, i.e. analysis of run-time values and run-time behavior.

[keean]

Consider this:

mandel(x0, y0, x, y) : never =>
    while (x*x + y*y < 2*2) {
        let xtemp = x*x - y*y + x0
        y = 2*x*y + y0
        x = xtemp
    }
}

Is this type correct?

[keean]

refresh, as i edited above.

[keean]

Basically if you cannot prove non-termination, then never is by definition unsound. The definition of soundness is that a program that passes type-checking cannot go wrong at runtime. A function that I type as never that actually returns is going-wrong.

[shelby3]

@keean wrote:

Is this type correct?

No. Should be the Unit type, because it doesn't return a value.

Although it doesn't return in some scenarios but not all, thus:

@shelby3 wrote:

but note a Bottom is subsumable so a single throw (non-termination path) combined with a concrete return could be subsumed to that concrete return value

[keean]

@shelby3 what is the difference between this example:

// Function returning never must have unreachable end point
function infiniteLoop(): never {
    while (true) {
    }
}

And this:

mandel(x0, y0, x, y) : never =>
    while (x*x + y*y < 2*2) {
        let xtemp = x*x - y*y + x0
        y = 2*x*y + y0
        x = xtemp
    }
}

How does the compiler know the first terminates and the second sometimes does terminate? The only way is to evaluate the loop. This is exactly the halting problem.

The point is the type checker has to decide if the type is correct, and that triggers the halting problem

[shelby3]

@keean wrote:

Basically if you cannot prove non-termination, then never is by definition unsound.

Incorrect, because it can be subsumed to any instantiable type.

A function that I type as never that actually returns is going-wrong.

Correct. But we are not doing that.

The main utility of Bottom in an eager, CBV language is so we can assign a type that is nothing to something that expects a type, e.g. Nil and the example provided by TypeScript. Which is why Scala chose Nothing name but Never is more consistent.