Re: Proposal for study: Add a categorical Initial type to ocaml

From: skaller (skaller@maxtal.com.au)
Date: Mon Oct 11 1999 - 02:51:38 MET DST


Date: Mon, 11 Oct 1999 10:51:38 +1000
From: skaller <skaller@maxtal.com.au>
To: William Chesters <williamc@dai.ed.ac.uk>
Subject: Re: Proposal for study: Add a categorical Initial type to ocaml

William Chesters wrote:
>
> skaller writes:
> > > > Boxed values can use a null pointer for none.
> > >
> > > I have a question--how is this different (except for the efficiency of
> > > using null) from using a 'a option array?
> >
> > It isn't, in theory, it is exactly the same (and therefore sound).
>
> I think (correct me if I'm wrong, sorry) that this is a return to an
> issue which seems to be a bit of an FAQ.
>
> The problem is that if you have a value of the type `int option
> option', you have to be able to distinguish between `None' and `Some
> None'! If both the enumeration-indirections are elided, you can't; if
> only one of them is, you have inconsistency which would presumably
> have to be resolved using whole-program optimisation or something.

You are right. Note, however, that the 'initial' value would
never be available to the client, since any attempt to get it
would throw an exception, and in that case there is no need to
distinguish the cases.

To put it another way: programming languages generally
distinguish isomorphic objects, for example

        ((), x) (* type is unit * int *)

is isomorphic to

        x (* type is int *)

but they are distinguished in _client_ code.
The compiler may be able to use the isomorphism to achieve
an optimisation in the representation.

However, this is not the way initial works, since the client
can never sensibly test for this value, since every attempt to do so
would either fail or raise an exception. That is,
while in the case of 'a option:

        match x with
        | Some x' -> do_something x'
        | None -> do_nothing

it makes sense for do_nothing to do some kind of work, in the
case of initial, it always signifies a programming error.
So there is no need to distinguish the isomorphic cases here:
unlike client code 'Initial' means 'forbidden', the action
on the 'None' case is built in (raise an exception).

-- 
John Skaller, mailto:skaller@maxtal.com.au
1/10 Toxteth Rd Glebe NSW 2037 Australia
homepage: http://www.maxtal.com.au/~skaller
downloads: http://www.triode.net.au/~skaller



This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:26 MET