"skaller" <skaller@users.sourceforge.net> wrote:

> Felix allows
>
> f: int -> 0
>
> but not
>
> g: 0 -> int

Then your "0" is not a proper type in the usual formal sense. Even less is
it the type-theoretic 0.

As Andrej Bauer points out, void vs unit has nothing to do with side
effects. If you want to capture side effects properly in a type system the
known approaches are effect systems or monads. In fact, your 0 looks
somewhat like a monad type with implicit injection and semicolon as a kind
of forgetting bind operator. But it seems sufficiently adhoc to make any
type-theoretic interpretation difficult.

  - Andreas