Re: [Caml-list] Re: Void type?

["Markus Mottl" <markus.mottl@gmail.com>]

On 7/30/07, Brian Hurt <bhurt@janestcapital.com> wrote:
> I'm not sure I agree with this- especially the proposition that unit ==
> truth.  That would make a function of the type:
>     unit -> 'a
> equivelent to the proposition "If true then for all a, a", which is
> obviously bogus.

Indeed, this proposition is impossibly true.

> The assumption of the Ocaml type system is that you
> can not form "false" theorems within the type system (these correspond
> to invalid types).  So either this assumption is false, or unit is the
> void type in the Ocaml type system.

I guess you mean that one cannot form proofs of propositions that
don't have a model (i.e. an interpretation that makes the proposition
true).  There is a false dichotomy here.  It rests on the assumption
that a pure program that has such a type is a proof of the proposition
whereas in fact it isn't.  The assumption that programs are proofs
only makes sense if every program is strongly normalizing, i.e.
requires only a finite amount of evaluation (= "proof") steps.  This
is always the case with e.g. the pure, simply typed lambda calculus
without fixed-point operator, which is strongly normalizing.
Something that requires an infinite number of derivation steps cannot
be considered a proof.

If we constrained ourselves to programs that are proofs only, and if
we required soundness, too, then there would be satisfiable
propositions for which, indeed, you wouldn't be able to write down a
program of corresponding type: some solvable problems would become
unsolvable to us.

OCaml is not unsound.  It is also not incomplete in the sense that you
cannot write down a terminating program for a proposition that has a
model.  But this unfortunately necessarily implies that you can write
down programs that are not proofs, i.e. never terminate.

Note that you can also write down the type "unit -> unit", which is a
tautology and therefore trivially true in any interpretation.  But you
can still write down a program of this type that doesn't constitute a
proof of the corresponding proposition irrespective of how trivial it
may be:

  let rec f () = f (f ())

Provability and truth are two distinct concepts, you cannot conflate
the two in the general case.  This is a direct consequence of Goedel's
incompleteness theorem.

Some program may constitute a proof or not, and a type may correspond
to a satisfiable proposition or not.  We definitely don't want a
system that allows us to write down something that is a proof of a
false proposition (= unsound).  We want to be able to write down a
proof for every proposition that has a model (= completeness).  But
then we'll have to live with the presumably less awful fact that we
will be able to write down non-proofs of non-truths (and truths
alike)...

> More pragmatically, I don't see any situation in which void can be used
> where unit couldn't be used just as well, if not better.

You'll laugh, but I just actually made use of Chung-chieh Shan's trick
to use polymorphic record fields in our code base.  Here is a rough
idea of where this may be useful:

Assume you have a functor argument that defines several types and
functions operating on these types.  Now assume that I know that I
will never want to use the module resulting from the functor
application in a way that requires the use of some of these types and
associated functions in the functor argument.  How can I make sure
that nobody will ever do something with the resulting module that
violates these assumptions?  E.g.:

---------------------------------------------
module type ARG = sig
  type t
  type u

  val use_t : t -> unit
  val use_u : u -> t
end

module Func (Arg : ARG) = struct
  let propagate_t arg_t = Arg.use_t arg_t
  let propagate_u arg_u = Arg.use_u arg_u
end

type void = { void : 'a. 'a }

module Arg = struct
  type t = int
  type u = void

  let use_u u = u.void
  let use_t t = print_int t
end
---------------------------------------------

If I had specified "u" as "unit" in the above example, I would need to
e.g. raise an exception in "use_u" to indicate that my assumption was
violated, or return a dummy value (integer) which may screw up
something in the functor body, etc.  But having specified the value as
"void", I essentially get a proof at compile time that nobody will
ever be able to misuse the module resulting from the functor
application.

Of course, I could restrict the signature of the resulting module, but
this may be a non-trivial effort, e.g. if type "u" is used in sum
types of the resulting module, etc., in which case I'd have to wrap
the result in an intermediate module that translates function calls
accordingly.  The "void" solution on the other hand is just plain
awesome and solves this problem safely and conveniently.

Best regards,
Markus

-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com