Can I universally quantify a type in Python?

Question

Say that I want to encode cons as:

def cons(a, b):
    return lambda f : f(a, b)

I would like to add typing to the cons above. The obvious typing would be:

T = TypeVar('T')
U = TypeVar('U')
V = TypeVar('V')

def cons(a: T, b: U) -> Callable[[Callable[[T, U], V]], V]:
    return lambda f : f(a, b)

However, the above doesn't type check in pyre which gives:

cons.py:7:24 Invalid type variable [34]: The type variable `Variable[V]` isn't present in the function's parameters.

I assume that what I need is a universal quantification of the return type of the function.

Is there a way to express this in the Python type-system?

Answer 1

Turns out that you can get enough type-safety for this on Pyre by creating a protocol to describe the type of the continuation produced by cons:

class ConsCallable(Protocol, Generic[T, U]):
    def __call__(self, f: Callable[[T, U], V]) -> V: ...

This hides the V from the type signature and allows us to use it as the return type of cons:

def cons(a: T, b: U) -> ConsProtocol[T, U]:
    return lambda f : f(a, b)

We can then type car and cdr as well (or anything that passes a lambda to the returned ConsProtocol):

def car(cons: ConsProtocol[T, U]) -> T:
    cont: Callable[[T, U], T] = lambda x, _: x
    return cons(cont)

def cdr(cons: ConsProtocol[T, U]) -> U:
    cont: Callable[[T, U], U] = lambda _, y: y
    return cons(cont)

Note that we still need to explicitly add a type annotation to the cont as it cannot be inferred correctly by Pyre. Revealing the type gives:

Revealed type for `cont` is `typing.Callable[[Named(x, typing.Any), Named(_, typing.Any)], typing.Any]`. 

Issue where this was explained on GitHub: https://github.com/facebook/pyre-check/issues/771

Answer 2

This works fine with the mypy type-checker. We can use reveal_type to verify the return type of the function returned by cons:

from typing import Callable, TypeVar

T = TypeVar('T')
U = TypeVar('U')
V = TypeVar('V')

def cons(a: T, b: U) -> Callable[[Callable[[T, U], V]], V]:
    return lambda f: f(a, b)

def func(x: int, y: float) -> str:
    return f"{x} + {y} = {x + y}"

reveal_type(cons(10, 32)(func))  # Revealed type is "builtins.str"