Version française
Home     About     Download     Resources     Contact us    
Browse thread
Re: Proposal for study: Add a categorical Initial type to ocaml
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: John Prevost <prevost@m...>
Subject: Re: Proposal for study: Add a categorical Initial type to ocaml
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.