Search code examples
pythontypes

Is Any is the same as Forall a.a?


Python has the Any type which is 'is-consistent' with any type. Isn't it possible to express Any using the type represented in Haskell as forall a.a instead of adding a new type?


Solution

  • No, they are different.

    forall a. a is an uninhabited type. (A universal type would be a union of all other types; this is more like an intersection of all other types.) The only thing you can assign to a variable with that type is bottom:

    -- With the ExplicitForAll option set in GHC
    x, y :: forall a.a
    x = undefined  -- OK
    y = 'c' -- Not OK
    

    As such, it's the type most commonly used to indicate that a function never returns, either because it diverges (goes into an infinite loop)

    > :t let f = f in f
    let f = f in f :: t  -- forall t. t
    

    or because it raises an exception.

    > :t error
    error :: [Char] -> t  -- forall t. [Char] -> t
    

    Any is a pseudotype that is consistent with all other types, without being a sub- or supertype of any other type.

    x: Any = 1  # OK
    y: Any = 'c' # OK
    

    Neither 1 nor 'c' is an instance of Any, but the assignments are allowed according to the definition of consistency.

    In some sense, Python has two equivalents of forall a. a, at least for type-checking, typing.NoReturn and typing.Never. The latter was introduce in Python 3.11 as a clearer alternative to the former, but they are otherwise equivalent. (NoReturn was meant exclusively as a return-type annotation, while Never is explicitly intended to represent an empty type, which has uses other than as the return type of a non-returning function. NoReturn seems to be unofficially deprecated.)


    Consistency is the extension of subtyping to a "universe" in which Any has been added as a special type. As stated in PEP 483 (in the Summary of gradual typing),

    • A type t1 is consistent with a type t2 if t1 is a subtype of t2. (But not the other way around.)
    • Any is consistent with every type. (But Any is not a subtype of every type.)
    • Every type is consistent with Any. (But every type is not a subtype of Any.)