Tychecking control.solve

[jorgefandinno]

The current type definition of control.solve():

clingo/libpyclingo/clingo/control.py

Lines 687 to 697 in ec2c706

	def solve(
	self,
	assumptions: Sequence[Union[Tuple[Symbol, bool], int]] = [],
	on_model: Optional[Callable[[Model], Optional[bool]]] = None,
	on_unsat: Optional[Callable[[Sequence[int]], None]] = None,
	on_statistics: Optional[Callable[[StatisticsMap, StatisticsMap], None]] = None,
	on_finish: Optional[Callable[[SolveResult], None]] = None,
	on_core: Optional[Callable[[Sequence[int]], None]] = None,
	yield_: bool = False,
	async_: bool = False,
	) -> Union[SolveHandle, SolveResult]:

force us to use cast() with each call because of the Union type of its return value.

with cast(
    SolveHandle,
    self.control.solve(yield_=True),
) as handle:
    for model in handle:
    ...

It should be possible to improve this by using the @overload decorator on the type definition of control.solve() as follows:

   @overload
   def solve(
        self,
        assumptions: Sequence[Union[Tuple[Symbol, bool], int]] = [],
        on_model: Optional[Callable[[Model], Optional[bool]]] = None,
        on_unsat: Optional[Callable[[Sequence[int]], None]] = None,
        on_statistics: Optional[Callable[[StatisticsMap, StatisticsMap], None]] = None,
        on_finish: Optional[Callable[[SolveResult], None]] = None,
        on_core: Optional[Callable[[Sequence[int]], None]] = None,
        yield_: Literal[True] = False,
        async_: bool = False,
    ) -> SolveHandle:

    @overload
    def solve(
        self,
        assumptions: Sequence[Union[Tuple[Symbol, bool], int]] = [],
        on_model: Optional[Callable[[Model], Optional[bool]]] = None,
        on_unsat: Optional[Callable[[Sequence[int]], None]] = None,
        on_statistics: Optional[Callable[[StatisticsMap, StatisticsMap], None]] = None,
        on_finish: Optional[Callable[[SolveResult], None]] = None,
        on_core: Optional[Callable[[Sequence[int]], None]] = None,
        yield_: Literal[False] = False,
        async_: bool = False,
    ) -> SolveResult:

    @overload
    def solve(
        self,
        assumptions: Sequence[Union[Tuple[Symbol, bool], int]] = [],
        on_model: Optional[Callable[[Model], Optional[bool]]] = None,
        on_unsat: Optional[Callable[[Sequence[int]], None]] = None,
        on_statistics: Optional[Callable[[StatisticsMap, StatisticsMap], None]] = None,
        on_finish: Optional[Callable[[SolveResult], None]] = None,
        on_core: Optional[Callable[[Sequence[int]], None]] = None,
        yield_: bool = False,
        async_: bool = False,
    ) -> Union[SolveHandle, SolveResult]:

    def solve(
        self,
        assumptions: Sequence[Union[Tuple[Symbol, bool], int]] = [],
        on_model: Optional[Callable[[Model], Optional[bool]]] = None,
        on_unsat: Optional[Callable[[Sequence[int]], None]] = None,
        on_statistics: Optional[Callable[[StatisticsMap, StatisticsMap], None]] = None,
        on_finish: Optional[Callable[[SolveResult], None]] = None,
        on_core: Optional[Callable[[Sequence[int]], None]] = None,
        yield_: bool = False,
        async_: bool = False,
    ) -> Union[SolveHandle, SolveResult]:

with this, it should be possible to call solve.control() without cast when yield_ is used with a literal as in

with self.control.solve(yield_=True), as handle:
    for model in handle:
    ...

The first two instances of the overloaded declaration handle the use of literal booleans. The third handles the use of boolean expressions that still would need a cast because its type cannot be statically determined.

This requires python 3.8, which is the oldest version that did not reach its end of life. If older versions need to be supported, Literal[...] can be replaced by 'Literal[...]'.

[rkaminsk]

An example like this is given in PEP0586. So we could add these overloads. However, clingo still supports Python 3.6 and literal types are only available from Python 3.8 onward. The overloads would have to be added conditionally. (I know that Python 3.7 is EOL but there are still supported Linux distributions shipping with it.)

I think that it is worth adding this because with the current code one has to add this annoying cast/assertion. The conditional import could be done like this:

try:
    from typing import Literal
    HAS_LITERAL_TYPE = True
except ImportError:
    HAS_LITERAL_TYPE = False

...

# the first two overloads are subject to this condition
if HAS_LITERAL_TYPE:
    ...

Putting the type in quotes is for forward references. I did not find a pep that says we can do this for backward-compatibility. In any case, we would still have to do the conditional import (or import typing and then write 'typing.Literal[True]').

https://peps.python.org/pep-0586/#shortening-unions-of-literals