From: chet@watson.ibm.com
Message-Id: <199910101610.MAA16130@bismarck.chet.org>
To: John Prevost <prevost@maya.com>
Subject: Re: Proposal for study: Add a categorical Initial type to ocaml
Date: Sun, 10 Oct 1999 12:10:18 -0400
After some thought, it occurred to me that, given ZINC's
representation of objects, it should be possible to add a new
type-constructor,
type 'a unboxed_option =
ubSome of 'a
| ubNone
wherein ubSome is represented by the identitty function in the code,
and ubNone by NULL -- zero.
If I remember right, there is currently no use for NULL pointers in
CAML. So all we need to do is to write down the proper low-level
lambda-language expressions for each of the constructor and destructor
operations, as well as for equality-checking, and we're done (I
think?).
[[ubSome]] == [lam v]v
[This is really equal to "if v == NULL then NULL else v", as explained
below.]
[[ubNone]] == 0
[[match e with
ubSome x -> B1
| ubNone -> B2]]
==
let v1 = [[e]]
in if v1 == NULL then [[B2]]
else let x = v1
in [[B1]]
Equality is taken care of by just doing what we do today, but making
sure that NULL == NULL.
I haven't thought this thru enough to believe that I could *prove*
that well-typed programs don't go wrong, but I do *believe* it. We
can think of the GC maintenance bit as being an implicit discriminator
used to distinguish between the two cases -- ubSome or ubNone -- for
*unboxed* values. Likewise, for *boxed* values, since no boxed value
can be *null* (all boxed values are really represented in the heap,
even -- especially -- nullary constructors) the null-ness of the
ubNone value is used to discriminate.
It is a happy coincidence that you don't have to strip off that
discriminator "tag" when you destructure, and that you don't have to
add the "tag" when you construct.
Going further, things like ('a unboxed_option) unboxed_option are
somewhat flawed, but they do work, (as they must, if this is going to
work) -- of three possibilities,
(a) ubSome(ubNone)
(b) ubSome(ubSome x)
(c) ubNone
at construction time, (a) and (c) collapse, together, but everything
is still well-typed.
So there is a behavioural difference in programs -- they can detect
that unboxed_option is actually unboxed, by using the fact that these
two cases collapse. But seems like a small price to pay for something
which gives you a rather useful feature of systems-programming
languages.
Comments,
--chet--
This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:26 MET