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?

You are right what the issue and what you need. You could probably just create a wrapper class to encapsulate the function. Then you could just pass the types into `__call__` as a generic ‍♂️. — PCDSandwichMan, Aug 01 '23 at 22:11
@Samwise doesn't `V` have to be in the input types for it to be in the return type? — PCDSandwichMan, Aug 01 '23 at 22:14
@Samwise, `mypy` indeed type checks this but it doesn't understand type check for `car` and `cdr` — namesis, Aug 01 '23 at 22:15
I am looking [here](https://docs.python.org/3/library/typing.html#typing.TypeVar) if it helps at all. — PCDSandwichMan, Aug 01 '23 at 22:16
@namesis You might want to post a new question with the definitions of `car` and `cdr`. I'm familiar with those function names from Lisp but I'm not quite clear on what it is you're doing here. — Samwise, Aug 01 '23 at 22:17
@PCDSandwichMan no. Loads of functions return a different type to their arguments. — OrangeDog, Aug 01 '23 at 22:33
@Samwise mypy playground link for car and cdr: https://mypy-play.net/?mypy=latest&python=3.11&gist=30773cfcb7f4bf19fb6a1602d10a4549 — namesis, Aug 01 '23 at 22:50
If it's supposed to work, and works in one type checker but not another, that's a bug to file against the latter, not a programming problem. Keep in mind that annotations have *no effect at runtime and no effect on compilation* aside from setting some metadata in hidden `__annotations__` attributes; these checks are *only* implemented by third party tools and *cannot actually invalidate* the code as far as Python's bytecode compiler is concerned. — Karl Knechtel, Aug 03 '23 at 09:12
@KarlKnechtel, indeed. I've added one bug-report to mypy about this already. I will add a separate bug report as it fails to type-check the code on my answer below. — namesis, Aug 03 '23 at 09:16

score 0 · Answer 1 · answered Aug 01 '23 at 22:15

0

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"

answered Aug 01 '23 at 22:15

Samwise

68,105
3
30
44

Interesting that `mypy` works for this. However, it seems to fail for `car` and `cdr`: ``` def car(cons: Callable[[Callable[[T, U], V]], V]) -> T: return cons(lambda x, _: x) ``` – namesis Aug 01 '23 at 22:18
Your type annotation for `cons` in that example doesn't match the actual type of `cons`, though... did you mean to shadow it with an entirely different function like that? – Samwise Aug 01 '23 at 22:20
What's the actual type for `cons`? – namesis Aug 01 '23 at 22:21
1

`cons` as defined above is a `Callable[[T, U], Callable[[Callable[[T, U], V]], V]]`. But regardless, it's weird that you would shadow it in the definition of `car` the way you did, which suggests that there might be some other confusion. The functions you're defining don't look like the `cons`, `car`, and `cdr` operations that I'm familiar with. – Samwise Aug 01 '23 at 22:22
The thing I pass in `car` and `cdr` is the return value of `cons`. These seem to encode traditional Lisp `cons`, `car`, and `cdr` to me: ```assert car(cons('a', 4)) == 'a'; assert cdr(cons(3, 4)) == 4; assert car(cdr(cons(5, cons(4, 6)))) == 4``` – namesis Aug 01 '23 at 22:30
Here's a mypy playground link: https://mypy-play.net/?mypy=latest&python=3.11&gist=30773cfcb7f4bf19fb6a1602d10a4549 – namesis Aug 01 '23 at 22:50
Again: I suggest posting a new question that includes the definitions of `car`, `cdr`, and `cons`. Comments aren't a good format to ask a whole new question. – Samwise Aug 01 '23 at 23:05
1

I will note, now that I understand a bit more what you're trying to do, that trying to implement this via functions with strong typing is very awkward. Python already has a native data type for this (tuples) and if you just use that the typing is extremely straightforward; it's probably more runtime-efficient as well. – Samwise Aug 01 '23 at 23:18
Irrespective of car and cdr, I think that the fact that mypy type checks this at all is a bug. Also, mypy fails to type check if you replace the `func` in your example with a generic function. – namesis Aug 04 '23 at 11:51

score 0 · Accepted Answer · answered Aug 03 '23 at 08:50

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

Can I universally quantify a type in Python?

2 Answers2