It expresses intuitively, "Something which is exactly a nothing", so naturally, I would categorize that as a nothing directly of course. And you've just done precisely that with your code; foo = Some None => set that field to NULL could only represent saying that field is just exactly nothing directly. So, it's just like I said-you have to deal with the instance because it comes up in practice, and pragmatically we have to represent such cases in machine code as has been discussed. But in practicality almost never would an author sensibly keep the expanded form of Some None directly, it shows up due to code combinations only to be reduced. 

On Thu, Aug 20, 2015 at 10:05 AM, David Allsopp <dra-news@metastack.com> wrote:

Kenneth Adam Miller wrote:
> In the case of 2), that's interesting because such a type of
> Some None is sort of antithetical to describing anything
> sensical. Not that it's not pragmatic or doesn't occur-I'm sure
> some functions get combined in ways that stuff like this crops
> up. But I think of the typing system as being badly exercised
> if something like this arises-

One example that springs immediately to mind: NULLable field in a database, so 'a option is a sensible type to represent it. Now consider a function intended to generate SQL UPDATE statements for that field:

val update_record : ?foo:int option -> ?bar:int option -> id:int -> baz:string -> bool

where omitting ~foo or ~bar means "don't change foo/bar in the UPDATE statement". Within the code for update_record:

foo = None => don't update that field
foo = Some None => set that field to NULL
foo = Some (Some i) => set that field's value to i

and all three cases will need different code.

See also https://github.com/ocaml/ocaml/blob/trunk/typing/env.ml#L391

What's (to you) badly exercised or nonsensical in either of those representations?


David