[simiones]

Not really, the problem described in the article could be rewritten to think of Next as a function World->World.

[contravariant]

Though in that case requiring that Next blinks both 'x' and 'y' should obviously mean they are required to blink synchronously. Depending on how you model World you can either compose the two Next functions that blink x and y or you can multiply their respective worlds and use the product map.

None of these feel unnatural.

[simiones]

Sure, that's a natural way of reading this requirement, but is it the right way? How would you specify the system such that it can produce:

[(x, y), (!x, y), (!x, !y), (x, !y), (!x, y), ...]

(that is, any interleaving of the two blinks that preserves the constraint that there is at least one blink in each "step")

[contravariant]

If you ask me requiring at least one blink in each step is a bit awkward as it is a global requirement as opposed to a local one.

But you can add the requirement Next(World) <> World if you really want to. Then you just get two sets:

- Next(World) <> World

- Next(World).x in (World.x, !World.x)

and

- Next(World) <> World

- Next(World).y in (World.y, !World.y)

and if you combine them you get

- Next(World) <> World

- Next(World).x in (World.x, !World.x)

- Next(World).y in (World.y, !World.y)

which seems to do what you want.

Adding global constraints seems like an easy way to shoot yourself in the foot though.