What's the correct way to type hint an empty list as a literal in python?

I have a function that always returns an empty list (it's a long story why), I could type hint as usual with just "list", but it would be useful to indicate that the list is always going to be the same.

My first thought was to use literal like this:

from typing import Literal

def get_empty_list() -> Literal[[]]:
    return []

Mypy flags this as an invalid type, is there a correct way to type hint an always empty list? (obviously, I could type hint just a list, but this is less helpful)

To be explicit, this is a list that is always empty and doesn't expect to have any elements. (As seperate for example, from a list that is currently empty, but might have elements of some type added later on).

If you want a type that expresses "list that doesn't have elements now, but might have elements added later", then that's fundamentally not a static type. Appending elements to such a list would be valid, but would cause the list to stop being an element of that type, which should not happen with static types in a program that respects static typing.

If you want something that expresses "list that has no elements, and will never have elements", you can kind of do it:

from typing import Never

def get_empty_list() -> list[Never]:
    return []

Here, we've annotated the element type as typing.Never, a type with no values. This is actually the type mypy infers for an empty list literal if there's no context to suggest another type, as you can see with reveal_type:

from typing import Never

x: list[Never]
reveal_type(x)
reveal_type([])

mypy output:

main.py:4: note: Revealed type is "builtins.list[<nothing>]"
main.py:5: note: Revealed type is "builtins.list[<nothing>]"
Success: no issues found in 1 source file

Here are the implications of using a list[Never] type:

• Static type checkers will not allow operations that add elements to a list annotated as list[Never].

• They will allow operations like get_empty_list().append(sys.exit()), where the argument to append is an expression that cannot evaluate to a value.

• They will recognize that get_empty_list()[0] cannot evaluate to a value... but this is very different from considering it a prohibited operation. In fact, rather than prohibiting the operation, they will allow it, in almost any context.

  After all, if an expression cannot produce a value, then it cannot produce a value of the wrong type, no matter what the right type is. So you can do stuff like

  x: int = get_empty_list()[0]
  

  and from a static typing perspective, that's perfectly valid. ([][0] is considered valid too.)

• They will not recognize that len(get_empty_list()) must be 0.

from typing import List

def get_empty_list() -> List:
    return []

result = get_empty_list()
print(result)  # Output: []

The List annotation without any type parameters is used to indicate that the function returns a list, but it doesn't specify the type of elements in the list.