Function "bind" on Result adt doesn't typecheck

[ianliu]

The following adt with an extra method bind is failing to typecheck. Mypy is returning

main.py:15: error: Argument "ok" to "match" of "Result" has incompatible type "Callable[[A], Result[C, B]]"; expected "Callable[[Result[C, B]], Result[C, B]]"

from adt import adt, Case
from typing import Generic, TypeVar, Callable

A = TypeVar("A")
B = TypeVar("B")
C = TypeVar("C")

@adt
class Result(Generic[A, B]):
    OK:  Case[A]
    ERR: Case[B]

    # bind :: Result a b -> (a -> Result c b) -> Result c b
    def bind(self, fun : Callable[[A], Result[C, B]]) -> Result[C, B]:
        return self.match(ok=fun, err=Result.ERR)

If I reveal the type of the match function, mypy says:

main.py:15: note: Revealed type is 'def [_MatchResult] (*, ok: def [_MatchResult] (A`1) -> _MatchResult`1, err: def [_MatchResult] (B`2) -> _MatchResult`1) -> _MatchResult`1'

and revealing the ok value:

main.py:15: note: Revealed type is 'def (A`1) -> main.Result[C`-1, B`2]'

So, the revealed types seems to be correct, but mypy still reports an error.

[jspahrsummers]

I haven't had a chance to try this sample out myself, but my guess is that the typechecker is failing to unify the types of ok and err. If you try the same code, but with lambdas wrapping fun and Result.ERR, does it work?

[ianliu]

I revealed the type for the err argument and indeed it was wrong, so I enforced the types for the arguments. Now mypy complains about the err function, saying it should be Callable[[Result[E, B]], Result[E, B]]

from adt import adt, Case
from typing import Callable, Generic, TypeVar

A = TypeVar("A")
B = TypeVar("B")
E = TypeVar("E")

@adt
class Result(Generic[E, A]):
    OK: Case[A]
    ERR: Case[E]

    def bind(self, f: Callable[[A], Result[E, B]]) -> Result[E, B]:
        ok: Callable[[A], Result[E, B]] = f
        err: Callable[[E], Result[E, B]] = Result.ERR
        return self.match(ok=f, err=err)

[jspahrsummers]

Does it work if you try to write something like this without the @adt sugar? The only thing that I can think of at this point is that there is a genuine mypy bug or limitation.

[ianliu]

The following program type-checks with mypy 0.782 and python 3.8.5:

from dataclasses import dataclass
from typing import Generic, TypeVar, Callable, cast, Union, Mapping

E = TypeVar("E")
A = TypeVar("A")
B = TypeVar("B")
Fun = Callable[[A], B]

class Result(Generic[E, A]):
    @staticmethod
    def OK(value: A) -> 'Result[E, A]':
        return Result(True, value)

    @staticmethod
    def ERR(value: E) -> 'Result[E, A]':
        return Result(False, value)

    def __init__(self, ok: bool, value: Union[E, A]):
        self.ok = ok
        self.value = value

    def __repr__(self):
        return f"OK {repr(self.value)}" if self.ok else f"ERR {repr(self.value)}"

    def __str__(self):
        return repr(self)

    def match(self, ok: Fun[A, B], err: Fun[E, B]) -> B:
        return ok(cast(A, self.value)) if self.ok else err(cast(E, self.value))

    def bind(self, f: Fun[A, 'Result[E, B]']) -> 'Result[E, B]':
        return self.match(ok=f, err=Result.ERR)

@dataclass
class User:
    id: int
    name: str

USERS: Mapping[int, User] = {
    0: User(id=0, name="root")
}

def parse_user_id(s: str) -> Result[str, int]:
    try:
        return Result.OK(int(s))
    except ValueError as e:
        return Result.ERR(e.args[0])

def get_user(id: int) -> Result[str, User]:
    if id not in USERS:
        return Result.ERR('User not found')
    else:
        return Result.OK(USERS[id])

def get_user_from_str(s: str) -> Result[str, User]:
    return parse_user_id(s).bind(get_user)

print(get_user_from_str("foo")) # ERR "invalid literal for int() with base 10: 'foo'"
print(get_user_from_str("10"))  # ERR 'User not found'
print(get_user_from_str("0"))   # OK User(id=0, name='root')