It seems unwise to me to try to capture the notion of side-effects via a
type like "0" or "1". Skaller is talking as if the type

  int -> 0

means "a command with side-effects". But "int -> int" can have plenty
side effects, too. A better solution would be to refine types so that
they keep track of which things have side-effects (monads!).

A discussion along the lines "do commands return void or unit?" is
flawed. The type void, in any reasonable semantics (assuming eager
language here), will be inhabited exactly by non-terminating
expressions, whereas "unit" will be inhabited by non-terminating and
terminating ones. Neither of these say anything about side-effects.

I understand ocaml's solution to be as follows: it is understood that
expressions of _all_ types may involve side effects (as well as
exceptions). While the result of a command may be ignored, as it is
uninteresting, the cruical bit is that a command may terminate or not.
This means that its type must posses terminating as well as
non-terminating values, i.e., _unit_ is the right choice. Void would be
the right choice only if all commands were non-terminating, or if all
were terminating.

Andrej Bauer