Hard-play model

See section 15.

The type of the process I described previously is similar to hard-play model by Giorgi Japaridze.
In terms of game semantics, the environment can make as many moves as it wants (and as is possible in the current state) by filling the holes and only then to give an opportunity to make a move to the process (by forcing it).

Hard-play and easy-play models intersect on a practical class of problems, so it might be enough to support only one of them. However, human factors might require suppporting both (or a more general model).

E.g. (piohiho process):

class Process p i o hi ho where
 schedule :: (p, Map hi i, Set ho) -> (p, Map ho o, Set hi)

The environment passes to a process some of the previously requested inputs, and requests some outputs. The process responds by some outputs, and requests some inputs.
Note that while values of both ho and hi must be used linearly, it is allowed to postpone their fullfilment by several steps.

PS: alterrnatively, to make justification structure more obvious:

class Process p i o hi ho where
 schedule :: (p, Map hi (i, Set ho)) -> (p, Map ho (o, Set hi))