Split Never-type into 2 types

Is the sole distinction between the two types you proposed that one is in the argument position and the other is in the return type position?

If so, then I think they should be the same type.

A function with argument position ! can never be called, because you can't pass a value of ! to it (thus it "never starts calculating").

A function with return position ! may never return, because it can't return a value of !. It is not necessarily something that never ends, it just doesn't return to its caller.

But this distinction comes from the duality of the function argument vs return position, not from the type. The arguments provide a requirement to the caller and a guarantee to the function, while the return type is a requirement to the function and a guarantee to the caller.

12 Likes

Mostly. And !never could be a return-type, but implicitly ! at return-type is !any

Yes, !never can never be called, but such function could be written!

fn foo(p: !never) -> !never { p }

Maybe you are right!

1 Like

Ok, I sad that Rust macro panic!() -> !any and Haskell error :: HasCallStack => String -> a has similar return type.

You said "no it is impossible", but I still don't understand: why "no"?

I don't know what you are referring to, I never actually said "no it is impossible" in this thread.

Then, what is the difference between using !never in the return type and using !any in the return type?

Of course! In fact, that also works if we only have one never type:

fn foo(p: !) -> ! { p }

Even this would work:

fn foo<T>(p: !) -> T { p }

Exactly - now rust allow to write Nonsense, just compare with:

fn foo(p: u64) -> i16 { p }

I wish to repair this situation

The reason you can't implicitly convert from u64 to i16 is that it's ill-defined in some cases.

It's just fine to be able to implicitly convert from ! to anything else, because it is well-defined and unambiguous in all cases (because there are no cases).

3 Likes

You could still write this function with !never if it is truly equivalent to enum !never {} (playground)

fn foo<T>(p: !never) -> T { match p {} }

even if it weren't, it'd still also be valid to write

fn foo<T>(p: !never) -> T { unreachable!() }

since you have a type-checked guarantee that this code is unreachable.

These functions aren't useless, they are very useful when you need to map types, e.g. if you need to take a Result<(), !> and make a Result<(), Error> you can just result.map_err(absurd) (absurd is the name I've seen given to this function before, I don't recall where it comes from).

2 Likes

It's a good name. My logician brain also suggests "exfalso"

2 Likes

Your example is nonsense, the other example is reasonable because if I'm given a value that cannot exist then I have an absurd and I'm allowed to produce anything.

I don't understand what you mean with "repair this situation". This code is valid today and must remain valid tomorrow, you cannot change that.

3 Likes

Sure, you could write even

fn foo(p: !never) -> u16 { 42 }

But this not a point of nonsense.

In Haskell we could write

id_int :: Int -> Int
id_int x = x

id_str :: String -> String
id_str x = x

id :: a -> a
id x = x

-- ERROR: type mismatch
id_a_b :: a -> b
id_a_b x = x

-- ERROR: type mismatch
id_void :: Void -> a
id_void x = x

which corresponds to rust

fn id_int(x: i32) -> i32 { x }

fn id_str(x: &str) -> &str { x }

fn id<T>(x: T) -> T { x }

// Nonsense is here:
fn id_nonsense<T>(x: !) -> T { x }

That nonsense I wish to repair

Your Haskell example is not equivalent. The Rust equivalent of id_a_b is:

fn id_a_b<A,B>(x: A) -> B { x }

which is indeed an error.

The Haskell equivalent of "id_nonsense" is the function "absurd", which exists, and is defined as follows:

absurd :: Void -> a
absurd a = case a of {}
2 Likes

First, it is equivalent for "any"!. And for "never"! we still have an error

-- ERROR: type mismatch
id_void :: Void -> a
id_void x = x

Again: id_void is not equivalent to absurd!!!

I never said that absurd is wrong in rust! It is right.

If your concept of "any"! makes those equivalent, it follows that your concept of "any"! is not equivalent to any way that Rust uses !.

The only reason your id_void doesn't work in Haskell is that Haskell doesn't allow an implicit conversion between those types. But as I said above, it's entirely reasonable for Rust to perform this implicit conversion, because there is no ambiguity about how to convert ! to another type.

1 Like

Any proofs?

What is a type of panic!() in expression if cond { 42i32 } else { panic!() } if RUST have a RULE "An if expression evaluates to the same value as the executed block, or () if no block is evaluated. An if expression must have the same type in all situations."

I'm not 100% sure how rust/std currently implements it, but there are at least 2 reasonable possibilities:

  1. panic!()'s type is !. The ! gets implicitly converted into i32, so that the block has the type i32. I think this is what actually happens, at least in nightly.
  2. panic!() behaves like fn panic<T>() -> T, so after type inference, the type of panic!() in that context is i32.

I think case 2 aligns with your concept of "any"!, but it does not actually involve any types other than i32 – only functions with type parameters, and it would be a conceptual mistake to confuse type parameters with types.

1 Like

Note that if cond { 42i32 } else { panic!(); } is also well typed, even though the block with panic doesn't have a trailing expression and so should have type (). The panic!(); also doesn't have to be the last statement.

2 Likes

You say, 2 + 3 is not equivalent to 3 + 2 and absolutely not near to 5

But I say, (2 + 3) == (3 + 2) == (5).

We do not care if ! is implicitly converted to any type OR ! is a generalized type OR it is magical !any type.

In Rust type ! plays 2 roles now: as !never and as !any, which corresponds to Hakell types Void and a

Haskell has no concept equivalent to Rust's ! influencing control flow (in part because control flow is an inpure construct)

1 Like