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

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

[Manuel Fahndrich]

I did not word what I meant correctly. In the case of initial values, errors
can occur anywhere in the code, namely, whenever I access an uninitialized
value. Since these values can live in records, and the records can be passed
around, the error can occur anywhere.

Now, with a well-defined and encapsulated use of Obj.magic, such errors can
be avoided. E.g. in the extensible array case, I can write the module in
such a way that no matter what code I write outside of that module (not
using Obj.magic), it cannot result in an error.

-Manuel


-----Original Message-----
From: skaller [mailto:skaller@maxtal.com.au]
Sent: Thursday, October 14, 1999 3:44 PM
To: Manuel Fahndrich
Cc: caml-list@inria.fr
Subject: Re: Proposal for study: Add a categorical Initial type to ocaml


Manuel Fahndrich wrote:
> 
> skaller wrote:
> 
>         [...]
> 
>         > Like I've been saying, with option you can turn it off, with
> Obj.magic, the implementor ought to be damned sure he's doing things
right.  
> But with these special "uninitialized value" sorts of things, people like
> me who've gotten used to good type systems keep looking over their
> shoulders because they're afraid it might turn around and bite
> them in the butt.
> 
>>                 How is this different from Obj.magic? Can't that bite you
>>         in the ass too?
> 
>>> The difference is that in the first case of uninitialized values, they
can
>>> crop up anywhere in your program, since they get propagated. Using
Obj.magic
>>> within a special module such as resizable arrays confines the danger to
that
>>> module. The programmer can make sure (through extensive code reviews of
a
>>> finite piece of code) that outside the module, things cannot go awry.

	No. It is the other way around. Obj.magic values can get
propagated, and so cause a problem. The special initial can NOT
be propagated. Any attempt to copy such a value raises an exception.
Ensuing this does not happen is also a matter of hiding within
a modular abstraction, but at least an exception will help
detect such localised errors.

-- 
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

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

[skaller]

Manuel Fahndrich wrote:
> 
> I did not word what I meant correctly. 

	i thought you did OK ..

>In the case of initial values, errors
> can occur anywhere in the code, namely, whenever I access an uninitialized
> value. Since these values can live in records, and the records can be passed
> around, the error can occur anywhere.
> 
> Now, with a well-defined and encapsulated use of Obj.magic, such errors can
> be avoided. E.g. in the extensible array case, I can write the module in
> such a way that no matter what code I write outside of that module (not
> using Obj.magic), it cannot result in an error.

	I'm sorry. I do do not follow. You argument is comparative,
and appears unsound because it fails to make a distinction.
The magical encapsulation of Obj.magic within a module
or class, can be applied to initials just the same: maintaining
the invariant 'uninitialised values are initialised before use'
is the same in both cases, only the value representing it differs.
Where 'initial' might be used, obj.magic could be used too.
References to both may be propagated without error
(and indeed that is the whole point): the only difference
is that using an initial value is guarranteed to cause
an exception to be raised, whereas using a magical
value offers no guarrantees, and could core dump.

	The initial value is therefore easier
to debug. The other difference seems to be that it
is polymorphic whereas obj.magic needs explicit
casting.
 
-- 
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

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

[Manuel Fahndrich]

I was comparing using Obj.magic in the particular case of writing an
extensible array module vs. adding uninitialized values to the language.

In the second case, having uninitialized values as a language feature will
make code more brittle since the uninitialized exception may be raised
anywhere in the code where a field access is made.

In the first case, the module can be constructed such that the use of
Obj.Magic can be deemed safe, namely by requiring all accesses of extensible
arrays to go through the module and that appropriate checks are in place
there.

-Manuel


-----Original Message-----
From: skaller [mailto:skaller@maxtal.com.au]
Sent: Sunday, October 17, 1999 2:19 AM
To: Manuel Fahndrich
Cc: caml-list@inria.fr
Subject: Re: Proposal for study: Add a categorical Initial type to ocaml


Manuel Fahndrich wrote:
> 
> I did not word what I meant correctly. 

	i thought you did OK ..

>In the case of initial values, errors
> can occur anywhere in the code, namely, whenever I access an uninitialized
> value. Since these values can live in records, and the records can be
passed
> around, the error can occur anywhere.
> 
> Now, with a well-defined and encapsulated use of Obj.magic, such errors
can
> be avoided. E.g. in the extensible array case, I can write the module in
> such a way that no matter what code I write outside of that module (not
> using Obj.magic), it cannot result in an error.

	I'm sorry. I do do not follow. You argument is comparative,
and appears unsound because it fails to make a distinction.
The magical encapsulation of Obj.magic within a module
or class, can be applied to initials just the same: maintaining
the invariant 'uninitialised values are initialised before use'
is the same in both cases, only the value representing it differs.
Where 'initial' might be used, obj.magic could be used too.
References to both may be propagated without error
(and indeed that is the whole point): the only difference
is that using an initial value is guarranteed to cause
an exception to be raised, whereas using a magical
value offers no guarrantees, and could core dump.

	The initial value is therefore easier
to debug. The other difference seems to be that it
is polymorphic whereas obj.magic needs explicit
casting.
 
-- 
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

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

[skaller]

Manuel Fahndrich wrote:
> 
> skaller wrote:
> 
>         [...]
> 
>         > Like I've been saying, with option you can turn it off, with
> Obj.magic, the implementor ought to be damned sure he's doing things right.  
> But with these special "uninitialized value" sorts of things, people like
> me who've gotten used to good type systems keep looking over their
> shoulders because they're afraid it might turn around and bite
> them in the butt.
> 
>>                 How is this different from Obj.magic? Can't that bite you
>>         in the ass too?
> 
>>> The difference is that in the first case of uninitialized values, they can
>>> crop up anywhere in your program, since they get propagated. Using Obj.magic
>>> within a special module such as resizable arrays confines the danger to that
>>> module. The programmer can make sure (through extensive code reviews of a
>>> finite piece of code) that outside the module, things cannot go awry.

	No. It is the other way around. Obj.magic values can get
propagated, and so cause a problem. The special initial can NOT
be propagated. Any attempt to copy such a value raises an exception.
Ensuing this does not happen is also a matter of hiding within
a modular abstraction, but at least an exception will help
detect such localised errors.

-- 
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

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

[Manuel Fahndrich]

skaller wrote:

	[...]

	> Like I've been saying, with option you can turn it off, with
Obj.magic, the
	> implementor ought to be damned sure he's doing things right.  But
with
	> these special "uninitialized value" sorts of things, people like
me
	> who've gotten used to good type systems keep looking over their
	> shoulders because they're afraid it might turn around and bite
them in
	> the butt.

		How is this different from Obj.magic? Can't that bite you
	in the ass too?

The difference is that in the first case of uninitialized values, they can
crop up anywhere in your program, since they get propagated. Using Obj.magic
within a special module such as resizable arrays confines the danger to that
module. The programmer can make sure (through extensive code reviews of a
finite piece of code) that outside the module, things cannot go awry.

-Manuel

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

[skaller]

John Prevost wrote:
> Something like that.  We can probably define unsafe_create like this:
> 
> let unsafe_create i = (Obj.magic (Array.make i 0) : 'a array)

	Thanks for the example, using Obj.magic. Since this
is not really documented, I wasn't sure how it worked.
This makes the code much cleaner. 

> (The above works, I've tested it.  

	Thanks!

> Now.  What can we gather from this?  First: by abusing Obj.magic, we
> can do what we want.  Obviously, it's not strictly a nice thing to do,
> but if we can prove to ourselves that the code works right, then from
> the point of view of the API's client, everything's great.

	Yes. You've used Obj.magic much as I'd envision I'd
have used an 'initial' value.

> What else can we gather?  Well, what would be different if this were
> implemented with options?  There'd be the boxing inefficiency, of
> course.  Anything else? Not really. 

	Yes: the implementation would be much messier.

> So, is there a problem with my solution of working around the type
> system under the API level?

	Obj.magic isn't documented;  it isn't really part of the 
language. [But I think your solution is fine, provided it works]
 
> > The initial is not 'strange',
> > rather it is fundamental, the dual of the 'unit' type.
> 
> No--it's strange.  The reason it's strange is that it's something that
> can happen to a user that they don't expect.  Like null in Java.

	Which is better: initialising something with 'null',
leaving it uninitialised, or initialising it with a dummy value,
GIVEN that it must be declared before the first value is
available?

	It would not be entirely unreasonable to argue
that the dummy value is the _worst_ option, since failing
to subsequently initialise it with the proper value is
guarranteed NOT to be detected by the system (and will be
reflected only in unexpected program semantics). Null seems
better; even a core dump indicates there is an error.
 
> Why is it [null] a pain in the ass?  There's no way to turn it off. 

	It's a built in 'a option, for every pointer.

> Like I've been saying, with option you can turn it off, with Obj.magic, the
> implementor ought to be damned sure he's doing things right.  But with
> these special "uninitialized value" sorts of things, people like me
> who've gotten used to good type systems keep looking over their
> shoulders because they're afraid it might turn around and bite them in
> the butt.

	How is this different from Obj.magic? Can't that bite you
in the ass too?

> It's appropriate for exceptions to be thrown when out of bounds array
> accesses happen--although I'd rather it weren't.  

	It's better if the compiler checks. In Pascal, array bounds
cannot be exceeded. [The index must be of the type for which the
array is declared, which guarrantees it is in bounds]. Of course,
an automatic conversion for int to a subrange can fail :-)

>It's reasonable for
> the programmer to check and make sure this doesn't happen.  It's not
> reasonable for the programmer to check that index i of an array that
> was passed in has actually been assigned before now.  Much like it's
> not reasonable for the programmer to have to check that the argument
> is not null on a function that doesn't claim to accept null as an
> argument (my Java pet peeve).

	The way I understand 'initial', the programmer not only
doesn't have to check, the programmer _cannot_ check for it.
The check must be done by the system. 
 
> I really think adding anything that can cause more runtime errors is
> likely to be a wart, and no language needs more warts.

	As I said above: I do not see that this argument holds water.
The problem is that sometimes storage must be allocated before
initial values are available (in a procedural language).
It is possible then, to forget to initialise the storage properly.

	Forgetting is the problem, and it causes a run time error,
no matter whether a special 'initial' value is used, Obj.magic is used,
a dummy value is used, or the store is just left uninitialised.
There is no getting around this: the only difference is the _kind_
of run time error.

-- 
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

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

[Damien Doligez]

>From: John Prevost <prevost@maya.com>

>val Array.make_with_option (or something) : unit -> 'a option array
>
>which in some sort of "unsafe" mode doesn't actually initialize the
>array and guarantee that all values are well-formed.

That would break the invariants of the memory manager.

-- Damien

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

[Damien Doligez]

>From: skaller <skaller@maxtal.com.au>

>There proposal is for a syntactic designator (say '$') for the
>non-existant value of the initial type, which can
>be bound to a variable of any type.
>[You could say it has type 'a, as does 'raise SomeException']
>
>The effect of attempting to read this value from any type
>should be to raise the exception Uninitialised_value.

You could try to use "lazy (raise Uninitialised_value)", of type
'a lazy, with the advantage that the notion of "reading this value"
becomes clearly defined (it is using "force" on the value).


>A better name than $ is probably 'none'.
>Boxed values can use a null pointer for none.

OK.


>Integers and floats can be treated as follows:
>do not initialise them at all, if -unsafe is 
>specified. Otherwise, use the spare value of integers

What spare value ?


>and some NaN for floats,

This may or may not be possible, depending on the details of the IEEE
specification.


>Chars can be handled too, but it is probably not worth the
>effort until they are lifted to ISO10646, which has
>suitable code points available. [We could use 0xFF for
>8 bit chars]

No.  0xFF is already used, as well as the other 255 values.


-- Damien

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

[Jean-Francois Monin]

I'm not sure that category theory helps so much here. 
My own background in cat. th. is weak, here is my understanding:
 - unit is final because there is one & only one function from any type
   to unit, namely fun _ -> ()
 - an initial type, say ini, is a type s.t. we have one & only one function
   from ini to any type;
   this should be the empty sum with no contructor:
   type emp = ;;
   The initial function would be 
   let ini (x: emp) = match x with ;;

Note that this is syntactically not allowed in ocaml. I don't think
there is a theoretical problem to add it (at least there are
extensions of caml type system allowing this) , however such a type would be
intrinsically useless (without real use). In particular your '$' seems
inconsistent to me. The only way to "get" such a value is to
introduce it locally in the context, e.g. fun x -> x, or in your case

let f dollar = let x = { data = ini dollar }

which will never help !

[John Prevost <prevost@maya.com> wrote:]
> I would like to propose adding a new special type to ocaml,
> a categorical initial type. This type is the categorical dual
> of the categorical terminal type, unit. 
> 
> There proposal is for a syntactic designator (say '$') for the
> non-existant value of the initial type, which can
> be bound to a variable of any type.
> [You could say it has type 'a, as does 'raise SomeException']
> 
> The effect of attempting to read this value from any type
> should be to raise the exception Uninitialised_value.
> 
> Example:
> 
> type A = { data: t }
> let x = { data = $ }
> in x.data (* raises exception *)

  Jean-Francois Monin

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

[John Prevost]

chet@watson.ibm.com writes:

> Of course, it is problematic that "None" and "Some None" are
> indistinguishable.  But is it a reason to not have such a facility (as
> a storage-cost-free "option" type constructor)?
> 
> I'd like to believe that the answer is "no" -- that the efficiency
> values of such a type-constructor outweigh the semantic difficulties.
> 
> Of course, there's only one way to prove that -- by implementing both
> and trying it out on large programs.

One might presume that the definition that "'a nullOption === 'a
nullOption nullOption" isn't too hard to understand (although it might
muck up the inference engine.)  (Some (Some x)) would be the same as
(Some x) in this model, just as None would be the same as Some None.
Probably not suitable for a replacement of the option type, but a
useful additional type?

John.

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

[John Prevost]

skaller <skaller@maxtal.com.au> writes:

> > I have a question--how is this different (except for the efficiency of
> > using null) from using a 'a option array?  The array still must be
> > initialized--in this case to all null, or in the unsafe case, well,
> > it's unsafe.
> 
> 	It isn't, in theory, it is exactly the same (and therefore sound).
> The difference lies in the way it is represented: using the initial
> the 'a option wrapping is done by the system, not the client programmer
> (sort of like a Haskell monad) and therefore is more robust, more
> efficient, and leaves the client code cleaner. This is much the
> same argument as for exceptions. 

Hiding implementation details from the programmer does not always make
code cleaner.  You can have the monad comparison, though.  I'll use it
in a second.

> > If anything, I would argue that this points at representing 'a option
> > specially for already boxed values by using a null pointer for None,
> > rather than having a special strange value that comes out of arrays
> > and magically creates exceptions.
>
> 	That would make 'a option faster to use, but still require the
> overhead of writing code that needless does matches where it is
> known (dynamically) that only one of the cases can be used (such as
> in a variable length array).

Okay--so here's what I would do:

"Inefficient" safe array implementation:

type 'a exparray = { mutable ea_size   : int;
                     mutable ea_length : int;
                     mutable ea_array  : 'a array }

let length a = a.ea_length

let get a i =
  if i < a.ea_length
    then a.ea_array.(i)
    else raise (Invalid_argument "Earray.get")

let set a i v =
  if i < a.ea_length
    then a.ea_array.(i) <- v
    else raise (Invalid_argument "Earray.set")

let expand a n v =
  begin
    (if a.ea_length + n >= a.ea_size then
       let new_size =
         if n > a.ea_size then a.ea_size + n else a.ea_size * 2 in
       let new_arr = unsafe_create new_size in
       begin
         Array.blit a.ea_array 0 new_arr 0 a.ea_length;
         a.ea_array <- new_arr;
         a.ea_size <- new_size;
       end);
    Array.fill a.ea_array a.ea_length n v;
    a.ea_length <- a.ea_length + n
  end

let create i =
  { ea_size = i;
    ea_length = 0;
    ea_array = unsafe_create i }

let make i v =
  { ea_size = i;
    ea_length = i;
    ea_array = Array.make i v }

Something like that.  We can probably define unsafe_create like this:

let unsafe_create i = (Obj.magic (Array.make i 0) : 'a array)

(The above works, I've tested it.  I highly recommend not trying to
print out values of type 'a earray from the toplevel, though.)

So this is the pretty unsafe version.  There can't be a really unsafe
version because not initializing the memory at all would play havoc
with the GC.

Now.  What can we gather from this?  First: by abusing Obj.magic, we
can do what we want.  Obviously, it's not strictly a nice thing to do,
but if we can prove to ourselves that the code works right, then from
the point of view of the API's client, everything's great.

What else can we gather?  Well, what would be different if this were
implemented with options?  There'd be the boxing inefficiency, of
course.  Anything else?  Not really.  We'd be guaranteeing something
we can show to be true anyway, since that's why we were okay with
using Obj.magic up there.

So, is there a problem with my solution of working around the type
system under the API level?

> > Again, rather than introduce new features into the language, add a new
> > unsafe optimization and make the option type more efficient for boxed
> > values.
> 
> The initial is not 'strange',
> rather it is fundamental, the dual of the 'unit' type.

No--it's strange.  The reason it's strange is that it's something that
can happen to a user that they don't expect.  Like null in Java.

There's nothing unsound about null (well, unless you consider that
trying to call a method on null fails to be unsound, which I guess I
probably do), but that doesn't mean it's not a pain in the ass.

Why is it a pain in the ass?  There's no way to turn it off.  Like
I've been saying, with option you can turn it off, with Obj.magic, the
implementor ought to be damned sure he's doing things right.  But with
these special "uninitialized value" sorts of things, people like me
who've gotten used to good type systems keep looking over their
shoulders because they're afraid it might turn around and bite them in
the butt.

It's appropriate for exceptions to be thrown when out of bounds array
accesses happen--although I'd rather it weren't.  It's reasonable for
the programmer to check and make sure this doesn't happen.  It's not
reasonable for the programmer to check that index i of an array that
was passed in has actually been assigned before now.  Much like it's
not reasonable for the programmer to have to check that the argument
is not null on a function that doesn't claim to accept null as an
argument (my Java pet peeve).

I really think adding anything that can cause more runtime errors is
likely to be a wart, and no language needs more warts.


Hrm.  That last bit is too rambly, but I'll send this anyway.


John.

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

[skaller]

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

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

[chet]

Of course, it is problematic that "None" and "Some None" are
indistinguishable.  But is it a reason to not have such a facility (as
a storage-cost-free "option" type constructor)?

I'd like to believe that the answer is "no" -- that the efficiency
values of such a type-constructor outweigh the semantic difficulties.

Of course, there's only one way to prove that -- by implementing both
and trying it out on large programs.

--chet--

>>>>> "WC" == William Chesters <williamc@dai.ed.ac.uk> writes:

    WC> The problem is that if you have a value of the type `int
    WC> option option', you have to be able to distinguish between
    WC> `None' and `Some None'!  If both the enumeration-indirections
    WC> are elided, you can't; if only one of them is, you have
    WC> inconsistency which would presumably have to be resolved using
    WC> whole-program optimisation or something.

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

[chet]

I read the referenced note

[http://caml.inria.fr/caml-list/0967.html]

and while I agree with most of what's said there, I think that putting
the "option" attribute onto a field would reduce its value.

Specifically, it is a highly common (albeit problematic) idiom in C,
C++, Java, and other languages, to program with a pointer to X, which
is perhaps null, and is only checked late, at the point when it is
destructured somehow.

That sort of idiom would not be possible to capture -- when we fetch
the value of an "option" field, we are implicitly asking for the field
to be checked for non-null-ness.

In other words, I think that "nullability" is a useful property of
types in general, and not merely of types of fields.

--chet--

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

[William Chesters]

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.

For the lowdown and an interesting proposal for a fix, see

	http://caml.inria.fr/caml-list/0967.html

The same idea would obviously apply to arrays.

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

[Vyskocil Vladimir]

>I would like to propose adding a new special type to ocaml,
>a categorical initial type. This type is the categorical dual
>of the categorical terminal type, unit. 


I ask for this some time ago, but it was said that "it's not a good thing"...

Vladimir.

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

[chet]

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--

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

[skaller]

John Prevost wrote:
> 
> skaller <skaller@maxtal.com.au> writes:
> 
> > A better name than $ is probably 'none'.
> > Boxed values can use a null pointer for none.
> > Integers and floats can be treated as follows:
> > do not initialise them at all, if -unsafe is
> > specified. Otherwise, use the spare value of integers
> > and some NaN for floats, and insert tests
> > for all read accesses.
> 
> I have a question--how is this different (except for the efficiency of
> using null) from using a 'a option array?  The array still must be
> initialized--in this case to all null, or in the unsafe case, well,
> it's unsafe.

	It isn't, in theory, it is exactly the same (and therefore sound).
The difference lies in the way it is represented: using the initial
the 'a option wrapping is done by the system, not the client programmer
(sort of like a Haskell monad) and therefore is more robust, more
efficient, and leaves the client code cleaner. This is much the
same argument as for exceptions. 

> If anything, I would argue that this points at representing 'a option
> specially for already boxed values by using a null pointer for None,
> rather than having a special strange value that comes out of arrays
> and magically creates exceptions.

	That would make 'a option faster to use, but still require
the overhead of writing code that needless does matches where
it is known (dynamically) that only one of the cases can be used (such
as in
a variable length array).
 
> Again, rather than introduce new features into the language, add a new
> unsafe optimization and make the option type more efficient for boxed
> values.

The initial is not 'strange',
rather it is fundamental, the dual of the 'unit' type.

-- 
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

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

[chet]

I second John's point.  In order to capture Java's semantics "on the
nose", you need to be able to model a slot of the T, which can contain
a "null".

Doing that by transforming Java's "T" to Caml's "T option", while
using a more-efficient representation under-the-covers, preserves the
possibility of disabling that efficiency-hack and debugging in a
cleaner environment.

Moreover, Java's semantics for variable-access is that fetching a null
value doesn't raise an exception -- only invoking a method on it
raises an exception.

So one can't use this "initial value" to model Java's "null".

Now, nobody claimed that Java's "null" was the target here, but, hey,
that's my $0.02.

--chet--

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

[John Prevost]

skaller <skaller@maxtal.com.au> writes:

> A better name than $ is probably 'none'.
> Boxed values can use a null pointer for none.
> Integers and floats can be treated as follows:
> do not initialise them at all, if -unsafe is 
> specified. Otherwise, use the spare value of integers
> and some NaN for floats, and insert tests
> for all read accesses.

I have a question--how is this different (except for the efficiency of
using null) from using a 'a option array?  The array still must be
initialized--in this case to all null, or in the unsafe case, well,
it's unsafe.

If anything, I would argue that this points at representing 'a option
specially for already boxed values by using a null pointer for None,
rather than having a special strange value that comes out of arrays
and magically creates exceptions.

One of the frustrations I have with things like Java is that it's not
possible to type references in a way which guarantees a value is not
null.

With my proposal, your special thing turns into an 'a option array,
lookup is the same (but is not guaranteed to provide a Some value),
and there's a new array function:

val Array.make_with_option (or something) : unit -> 'a option array

which in some sort of "unsafe" mode doesn't actually initialize the
array and guarantee that all values are well-formed.  This provides a
failure mechanism similar to unsafe array bounds, without adding
strange null values into the language.

Again, rather than introduce new features into the language, add a new
unsafe optimization and make the option type more efficient for boxed
values.

John.

Proposal for study: Add a categorical Initial type to ocaml

[skaller]

I would like to propose adding a new special type to ocaml,
a categorical initial type. This type is the categorical dual
of the categorical terminal type, unit. 

There proposal is for a syntactic designator (say '$') for the
non-existant value of the initial type, which can
be bound to a variable of any type.
[You could say it has type 'a, as does 'raise SomeException']

The effect of attempting to read this value from any type
should be to raise the exception Uninitialised_value.

Example:

	type A = { data: t }
	let x = { data = $ }
	in x.data (* raises exception *)

	type B = {mutable data: t }
	let y = { data = $ }
	in if something x.data <- t_value; 
	x.data (* raise exception if not something *)

The use of initial is something like a Haskell monad
with all types T changed to T option, and all 
read acesses changed to 

	match t with
	| Some t' -> t'
	| None -> raise Uninitialised_value

A better name than $ is probably 'none'.
Boxed values can use a null pointer for none.
Integers and floats can be treated as follows:
do not initialise them at all, if -unsafe is 
specified. Otherwise, use the spare value of integers
and some NaN for floats, and insert tests
for all read accesses.

Chars can be handled too, but it is probably not worth the
effort until they are lifted to ISO10646, which has
suitable code points available. [We could use 0xFF for
8 bit chars]

-- 
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