Skip to content
This repository has been archived by the owner on Oct 4, 2024. It is now read-only.

Function "bind" on Result adt doesn't typecheck #40

Open
ianliu opened this issue Jul 30, 2020 · 4 comments
Open

Function "bind" on Result adt doesn't typecheck #40

ianliu opened this issue Jul 30, 2020 · 4 comments
Labels
mypy Relating to the ADT mypy plugin question Further information is requested

Comments

@ianliu
Copy link

ianliu commented Jul 30, 2020

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
Copy link
Owner

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?

@jspahrsummers jspahrsummers added mypy Relating to the ADT mypy plugin question Further information is requested labels Aug 2, 2020
@ianliu
Copy link
Author

ianliu commented Aug 2, 2020

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
Copy link
Owner

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
Copy link
Author

ianliu commented Aug 11, 2020

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')

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
mypy Relating to the ADT mypy plugin question Further information is requested
Projects
None yet
Development

No branches or pull requests

2 participants