Version française
Home     About     Download     Resources     Contact us    
Browse thread
Stdlib regularity
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: skaller <skaller@m...>
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